Page 35 - 《软件学报》2025年第8期

3458 软件学报 2025 年第 36 卷第 8 期

的指标度量这种相似性也是一个有意义的问题.
差异验证 [58−60] 涉及比较两个不同的神经网络模型或同一模型的两个不同版本的行为, 其目标是检查模型是否
对相同的输入产生相似的输出. 而增量验证通过重用以前的结果和知识优化验证过程, 有可能将特定的增量验证
问题简化为差异验证问题.

5 总 结

在本文中, 我们提出神经网络验证的增量约束求解问题, 并基于 Reluplex 框架提出一个增量 SMT 求解算法.
我们将算法实现为增量 SMT 求解器 DeepInc. 实验结果表明 DeepInc 在大多数权重被修改验证问题中更高效, 并
且特定场景下与目前最先进的求解器 α, β-CROWN 性能相当. 未来我们将考虑神经网络的结构变化, 以适应基于
CEGAR 框架的验证方法. 另一个挑战性的工作是考虑将 CDCL 框架与增量 SMT 求解结合. 此外, 结合 IVAN 和
DeepInc 的算法法并探究这两种方法如何结合以及选择哪种底层求解器能够获得最佳性能也是一个有价值的研究
方向.

References:
[1] Szegedy C, Zaremba W, Sutskever I, Bruna J, Erhan D, Goodfellow IJ, Fergus R. Intriguing properties of neural networks. In: Proc. of the
2nd Int’l Conf. on Learning Representations. Banff: OpenReview.net, 2014.
[2] Katz G, Barrett C, Dill DL, Julian K, Kochenderfer MJ. Reluplex: An efficient SMT solver for verifying deep neural networks. In:
Majumdar R, Kunčak V, eds. Computer Aided Verification. Cham: Springer, 2017. 97–117. [doi: 10.1007/978-3-319-63387-9_5]
[3] Ehlers R. Formal verification of piece-wise linear feed-forward neural networks. In: D’Souza D, Narayan Kumar K, eds. Automated
Technology for Verification and Analysis. Cham: Springer, 2017. 269–286. [doi: 10.1007/978-3-319-68167-2_19]
[4] Katz G, Huang DA, Ibeling D, Julian K, Lazarus C, Lim R, Shah P, Thakoor S, Wu HZ, Zeljić A, Dill DL, Kochenderfer MJ, Barrett C.
The Marabou framework for verification and analysis of deep neural networks. In: Dillig I, Tasiran S, eds. Computer Aided Verification.
Cham: Springer, 2019. 443–452. [doi: 10.1007/978-3-030-25540-4_26]
2
[5] Gehr T, Mirman M, Drachsler-Cohen D, Tsankov P, Chaudhuri S, Vechev M. AI : Safety and robustness certification of neural networks
with abstract interpretation. In: Proc. of the 2018 IEEE Symp. on Security and Privacy (SP). San Francisco: IEEE, 2018. 3–18. [doi: 10.
1109/SP.2018.00058]
[6] Singh G, Gehr T, Püschel M, Vechev M. An abstract domain for certifying neural networks. Proc. of the ACM on Programming
Languages, 2019, 3(POPL): 41. [doi: 10.1145/3290354]
[7] Eén N, Sörensson N. Temporal induction by incremental SAT solving. Electronic Notes in Theoretical Computer Science, 2003, 89(4):
543–560. [doi: 10.1016/S1571-0661(05)82542-3]
[8] Shtrichman O. Pruning techniques for the sat-based bounded model checking problem. In: Proc. of the 11th IFIP WG 10.5 Advanced
Research Working Conf. Scotland: Springer, 2001. 58–70. [doi: 10.1007/3-540-44798-9_4]
[9] Schrammel P, Kroening D, Brain M, Martins R, Teige T, Bienmüller T. Successful use of incremental BMC in the automotive industry.
In: Núñez M, Güdemann M, eds. Formal Methods for Industrial Critical Systems. Cham: Springer, 2015. 62–77. [doi: 10.1007/978-3-319-
19458-5_5]
[10] Disch S, Scholl C. Combinational equivalence checking using incremental sat solving, output ordering, and resets. In: Proc. of the 2007
Asia and South Pacific Design Automation Conf. Yokohama: IEEE, 2007. 938–943. [doi: 10.1109/ASPDAC.2007.358110]
[11] Ravi N, Wendell RE. The tolerance approach to sensitivity analysis in network linear programming. Networks, 1988, 18(3): 159–171.
[doi: 10.1002/net.3230180303]
[12] Wondolowski Jr FR. A generalization of Wendell’s tolerance approach to sensitivity analysis in linear programming. Decision Sciences,
1991, 22(4): 792–811. [doi: 10.1111/j.1540-5915.1991.tb00365.x]
[13] Filippi C. A fresh view on the tolerance approach to sensitivity analysis in linear programming. European Journal of Operational
Research, 2005, 167(1): 1–19. [doi: 10.1016/j.ejor.2004.01.050]
[14] Borgonovo E, Buzzard GT, Wendell RE. A global tolerance approach to sensitivity analysis in linear programming. European Journal of
Operational Research, 2018, 267(1): 321–337. [doi: 10.1016/j.ejor.2017.11.034]
[15] Wagner HM. Global sensitivity analysis. Operations Research, 1995, 43(6): 948–969. [doi: 10.1287/opre.43.6.948]