In recent years, Satisfiability Modulo Theory (SMT) solvers are becoming increasingly popular in the Com- puter Aided Verification and Reasoning community. Used natively or as back-engines, they are accumulat- ing a record of success stories and, as witnessed by the annual SMT competition, their performances and ca- pacity are also increasing steadily. Introduced in pre- vious 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 net- work. 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 veri- fication.
Challenging SMT solvers to verify neural networks
TACCHELLA, ARMANDO
2012-01-01
Abstract
In recent years, Satisfiability Modulo Theory (SMT) solvers are becoming increasingly popular in the Com- puter Aided Verification and Reasoning community. Used natively or as back-engines, they are accumulat- ing a record of success stories and, as witnessed by the annual SMT competition, their performances and ca- pacity are also increasing steadily. Introduced in pre- vious 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 net- work. 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 veri- fication.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
