We study orbit-finite systems of linear equations, in the setting of sets
with atoms. Our principal contribution is a decision procedure for solvability
of such systems. The procedure works for every field (and even commutative
ring) under mild effectiveness assumptions, and reduces a given orbit-finite
system to a number of finite ones: exponentially many in general, but
polynomially many when atom dimension of input systems is fixed. Towards
obtaining the procedure we push further the theory of vector spaces generated
by orbit-finite sets, and show that each such vector space admits an
orbit-finite basis. This fundamental property is a key tool in our development,
but should be also of wider interest.

本文研究了带有原子的集合中的有限轨系统的线性方程组，提出了一个适用于任何域（甚至可交换环）的可解决性决策过程，并将给定的有限轨系统约减为若干个有限系统；当输入系统的原子维度固定时，约减数量通常是指数级的，但是多项式数量。为了得到此过程，我们进一步推进了轨道有限集生成的向量空间理论，并展示了每个向量空间都拥有一个轨道有限基础，这个基础性质是我们开发中的关键工具，但也应该具有更广泛的兴趣。

轨道有限线性方程组的可解性

Solvability of orbit-finite systems of linear equations

In recent years, the notion of local robustness (or robustness for short) has
emerged as a desirable property of deep neural networks. Intuitively,
robustness means that small perturbations to an input do not cause the network
to perform misclassifications. In this paper, we present a novel algorithm for
verifying robustness properties of neural networks. Our method synergistically
combines gradient-based optimization methods for counterexample search with
abstraction-based proof search to obtain a sound and ({\delta}-)complete
decision procedure. Our method also employs a data-driven approach to learn a
verification policy that guides abstract interpretation during proof search. We
have implemented the proposed approach in a tool called Charon and
experimentally evaluated it on hundreds of benchmarks. Our experiments show
that the proposed approach significantly outperforms three state-of-the-art
tools, namely AI^2 , Reluplex, and Reluval.

本文提出了一种用于验证神经网络鲁棒性的新算法 Charon，并通过实验评估其在数百个基准测试中显著优于 AI^2，Reluplex 和 Reluval 等三种最先进的工具。