如何验证简单的神经网络？我想将图层转换成数学方程式，然后使用例如求解器 SAT求解器

我看过许多论文，它们在其中验证了神经网络。他们要么尝试检查对抗性鲁棒性，要么找到模型错误预测的输入。他们尝试将层转换为数学表达式，例如布尔表达式。然后通过可用的求解器（Microsoft Z3，Gurobi）对其进行求解。但是我找不到任何教程或起始代码。

您能帮我开始这个过程吗？例如，共享一个代码，以通过ReLu激活转换一个完全连接的层以用于MNIST数据。然后，我可以在此基础上构建更复杂的层。

谢谢

我会尝试的。一种方法是将网络结构公式化为整数线性程序（ILP）。首先考虑线性激活的情况。输入为 x 的完全连接的层，然后输出为 y = W x + b ，其中W是矩阵层中每个神经元的权重，以及 b 偏差的向量。

假设该图层的输入尺寸为 n ，输出尺寸为 m 。在ILP公式中，我们需要为图层输入和输出定义一个连续变量：

我们将用

表示层的权重和偏差值

然后可以用线性方程对第 i 个神经元的输出进行编码

y_i = b_i + W_i0 * x_0 + W_i1 * x_1 + ... W_in * x_n。

这对任何ILP库（例如CPLEX或Gurobi）都应该很简单。对ReLU非线性进行编码会涉及更多的内容。一种方法如下：

当方程的右侧为负时，这会破坏y_i值的先前方程。为了解决这个问题，我们将添加新的变量

，还将每个s_i的值的下限设置为0。然后，将前面的线性方程式重新编写为

y_i-s_i = b_i + W_i0 * x_0 + W_i1 * x_1 + ... W_in * x_n。

此等式现在允许无意义的解决方案，我们仍然需要添加一个约束，该约束要求y_i或s_i中的一个等于零。这背后的直觉是，在y_i和s_i中，我们将右侧的值分为正分量y_i和负分量s_i。然后y_i将成为ReLU函数的值，而s_i可以忽略。

实现将取决于特定的库，但是在CPLEX中，可以使用指标约束。简而言之，我们添加 binary 变量

以及说明这一点的指标约束

前段时间，我在https://github.com/psaikko/explain-mnist/blob/master/twoclass/min_explanation.py中使用CPLEX为一个简单的神经网络实现了这一点。如上所述，第26-97行执行到ILP的编码。