Z3 / OCaml 绑定未考虑变量边界

如何解决Z3 / OCaml 绑定未考虑变量边界

下午好，

我正在尝试使用 Z3 OCaml 绑定构建一个包含一些有边界变量的公式。对于上下文，我试图证明编码为 SMT 公式的神经网络的安全属性。

我的一些输入变量的值有界限，我想要的界限 添加作为我的 SMT 公式的约束。然后我迭代地向我的求解器堆栈添加新约束并检查它们是否有效。

这里是求解器栈的初始内容，用Z3.Solver.get_assertions获得。它包含没有确定的神经网络控制流 节点、权重和偏差值以及输入边界约束。

(forall ((x Real)) (= (reluR x) (ite (> x 0.0) x 0.0)))
[...]
;bunch of variables definitions and constraints
[...]
;input variables definitions
(> |CELL_actual_input_0_0_0_1| (/ 1.0 2.0))
(< |CELL_actual_input_0_0_0_1| 2.0)
(> |CELL_actual_input_0_0_0_0| (/ 1.0 2.0))
(< |CELL_actual_input_0_0_0_0| 2.0)
;a bunch of contraints defining the control flow of the network,here is an example
(= |CELL_actual_output_0_0_0_0| (+ |CELL_22_0_0_0_0| |CELL_l_4.bias_0|))
(= |CELL_14_0_0_0_1|
   (+ (* |CELL_12_0_0_0_0| |CELL_25_0_1|)
      (* |CELL_12_0_0_0_1| |CELL_25_1_1|)
      (* |CELL_12_0_0_0_2| |CELL_25_2_1|)
      (* |CELL_12_0_0_0_3| |CELL_25_3_1|)))
[...] 

然后我添加了以下表达式，描述了 ReLU 节点的激活。

(= |CELL_20_0_0_0_0| |CELL_19_0_0_0_0|)
(> |CELL_19_0_0_0_0| 0.0)

求解器给出了肯定的回答，并且在相应的模型上有些问题：

[...]
(define-fun |CELL_actual_input_0_0_0_0| () Real
  0.0)
(define-fun |CELL_actual_input_0_0_0_1| () Real
  0.0)
[...]

它似乎违反了我的输入边界约束。

求解后的求解器堆栈内容如下，我不确定我是否理解forall中的行

(forall ((x Real)) (= (reluR x) (k!11 x)))
(not (<= |CELL_actual_input_0_0_0_1| (/ 1.0 2.0)))
(not (<= 2.0 |CELL_actual_input_0_0_0_1|))
(not (<= |CELL_actual_input_0_0_0_0| (/ 1.0 2.0)))
(not (<= 2.0 |CELL_actual_input_0_0_0_0|))
(forall ((x!1 Real))
  (! (or (not (<= x!1 0.0)) (= (k!11 x!1) 0.0)) :pattern ((k!11 x!1))))
(forall ((x!1 Real))
  (! (or (<= x!1 0.0) (= (k!11 x!1) x!1)) :pattern ((k!11 x!1))))

请注意，我声明了我的控制流，其中输入变量已经首先出现，然后我用 Arithmetic.Real.mk_const_s ctx name 重新声明了我的输入，其中 name 是一样的。会不会是变量在栈中被记录了两次？

提前感谢您的回答