Challenging SMT solvers to verify neural networks
Challenging SMT solvers to verify neural networks
复制标题
DOI：
10.3233/aic-2012-0525
复制
发表时间：
2012-01-01
影响因子：
0.8
通讯作者：
Tacchella, Armando
中科院分区：
文献类型：
--
作者：
Pulina, Luca;Tacchella, Armando
近年来，可满足性模理论(SMT)求解器在计算机辅助验证和推理界越来越流行。它们被本地使用或用作后备引擎，正在积累成功故事的记录，正如一年一度的SMT比赛所证明的那样，它们的性能和能力也在稳步增长。在我们以前的贡献中介绍了一个新的应用领域，它为SMT解算器提供了一个突出的挑战，这是一种广泛采用的人工神经网络-多层感知器(MLP)的验证。本文对目前最先进的SMT求解器进行了广泛的评价，并评估了它们在MLP验证领域的潜力。
In recent years, Satisfiability Modulo Theory (SMT) solvers are becoming increasingly popular in the Computer Aided Verification and Reasoning community. Used natively or as back-engines, they are accumulating a record of success stories and, as witnessed by the annual SMT competition, their performances and capacity are also increasing steadily. Introduced in previous contributions of ours, a new application domain providing an outstanding challenge for SMT solvers is represented by verification of Multi-Layer Perceptrons (MLPs) a widely-adopted kind of artificial neural network. In this paper we present an extensive evaluation of the current state-of-the-art SMT solvers and assess their potential in the promising domain of MLP verification.