Besides training, mathematical optimization is also used in deep learning to
model and solve formulations over trained neural networks for purposes such as
verification, compression, and optimization with learned constraints. However,
solving these formulations soon becomes difficult as the network size grows due
to the weak linear relaxation and dense constraint matrix. We have seen
improvements in recent years with cutting plane algorithms, reformulations, and
an heuristic based on Mixed-Integer Linear Programming (MILP). In this work, we
propose a more scalable heuristic based on exploring global and local linear
relaxations of the neural network model. Our heuristic is competitive with a
state-of-the-art MILP solver and the prior heuristic while producing better
solutions with increases in input, depth, and number of neurons.

此研究提出了一种基于全局和局部线性松弛的可扩展启发式方法，用于对训练后的神经网络模型进行建模和求解，具有与最先进的整数线性规划（MILP）求解器和之前的启发式方法相竞争，并且在输入、深度和神经元数量增加时能够产生更好的解。

基于训练过的神经网络的优化：放松行走

Optimization Over Trained Neural Networks: Taking a Relaxing Walk

Neural network verification mainly focuses on local robustness properties.
However, often it is important to know whether a given property holds globally
for the whole input domain, and if not then for what proportion of the input
the property is true. While exact preimage generation can construct an
equivalent representation of neural networks that can aid such (quantitative)
global robustness verification, it is intractable at scale. In this work, we
propose an efficient and practical anytime algorithm for generating symbolic
under-approximations of the preimage of neural networks based on linear
relaxation. Our algorithm iteratively minimizes the volume approximation error
by partitioning the input region into subregions, where the neural network
relaxation bounds become tighter. We further employ sampling and differentiable
approximations to the volume in order to prioritize regions to split and
optimize the parameters of the relaxation, leading to faster improvement and
more compact under-approximations. Evaluation results demonstrate that our
approach is able to generate preimage approximations significantly faster than
exact methods and scales to neural network controllers for which exact preimage
generation is intractable. We also demonstrate an application of our approach
to quantitative global verification.

研究了神经网络的全局鲁棒性问题，提出了一种在量化验证中高效的、基于线性松弛的生成符号下逼近的先验图像的算法。

神经网络中的原像逼近

On Preimage Approximation for Neural Networks

We study fully dynamic online selection problems in an adversarial/stochastic
setting that includes Bayesian online selection, prophet inequalities, posted
price mechanisms, and stochastic probing problems subject to combinatorial
constraints. In the classical ``incremental'' version of the problem, selected
elements remain active until the end of the input sequence. On the other hand,
in the fully dynamic version of the problem, elements stay active for a limited
time interval, and then leave. This models, for example, the online matching of
tasks to workers with task/worker-dependent working times, and sequential
posted pricing of perishable goods. A successful approach to online selection
problems in the adversarial setting is given by the notion of Online Contention
Resolution Scheme (OCRS), that uses a priori information to formulate a linear
relaxation of the underlying optimization problem, whose optimal fractional
solution is rounded online for any adversarial order of the input sequence. Our
main contribution is providing a general method for constructing an OCRS for
fully dynamic online selection problems. Then, we show how to employ such OCRS
to construct no-regret algorithms in a partial information model with
semi-bandit feedback and adversarial inputs.

本文提出了一种针对完全动态在线选择问题的在线争用解决方案方法，并展示了如何利用该方法在部分信息模型中构建无遗憾算法。

在线内容竞争决策的全动态在线选择方案

Fully Dynamic Online Selection through Online Contention Resolution Schemes

Tight and efficient neural network bounding is crucial to the scaling of
neural network verification systems. Many efficient bounding algorithms have
been presented recently, but they are often too loose to verify more
challenging properties. This is due to the weakness of the employed relaxation,
which is usually a linear program of size linear in the number of neurons.
While a tighter linear relaxation for piecewise-linear activations exists, it
comes at the cost of exponentially many constraints and currently lacks an
efficient customized solver. We alleviate this deficiency by presenting two
novel dual algorithms: one operates a subgradient method on a small active set
of dual variables, the other exploits the sparsity of Frank-Wolfe type
optimizers to incur only a linear memory cost. Both methods recover the
strengths of the new relaxation: tightness and a linear separation oracle. At
the same time, they share the benefits of previous dual approaches for weaker
relaxations: massive parallelism, GPU implementation, low cost per iteration
and valid bounds at any time. As a consequence, we can obtain better bounds
than off-the-shelf solvers in only a fraction of their running time, attaining
significant formal verification speed-ups.

论文提出了两种新的双重算法来解决神经网络边界问题，这些算法可以更紧密地边界和验证神经网络，同时具有之前方法的优点，可以更高效地获得更好的验证结果。