-
Optimized Symbolic Interval Propagation for Neural Network Verification
Authors:
Philipp Kern,
Marko Kleine Büning,
Carsten Sinz
Abstract:
Neural networks are increasingly applied in safety critical domains, their verification thus is gaining importance. A large class of recent algorithms for proving input-output relations of feed-forward neural networks are based on linear relaxations and symbolic interval propagation. However, due to variable dependencies, the approximations deteriorate with increasing depth of the network. In this…
▽ More
Neural networks are increasingly applied in safety critical domains, their verification thus is gaining importance. A large class of recent algorithms for proving input-output relations of feed-forward neural networks are based on linear relaxations and symbolic interval propagation. However, due to variable dependencies, the approximations deteriorate with increasing depth of the network. In this paper we present DPNeurifyFV, a novel branch-and-bound solver for ReLU networks with low dimensional input-space that is based on symbolic interval propagation with fresh variables and input-splitting. A new heuristic for choosing the fresh variables allows to ameliorate the dependency problem, while our novel splitting heuristic, in combination with several other improvements, speeds up the branch-and-bound procedure. We evaluate our approach on the airborne collision avoidance networks ACAS Xu and demonstrate runtime improvements compared to state-of-the-art tools.
△ Less
Submitted 15 December, 2022;
originally announced December 2022.
-
Geometric Path Enumeration for Equivalence Verification of Neural Networks
Authors:
Samuel Teuber,
Marko Kleine Büning,
Philipp Kern,
Carsten Sinz
Abstract:
As neural networks (NNs) are increasingly introduced into safety-critical domains, there is a growing need to formally verify NNs before deployment. In this work we focus on the formal verification problem of NN equivalence which aims to prove that two NNs (e.g. an original and a compressed version) show equivalent behavior. Two approaches have been proposed for this problem: Mixed integer linear…
▽ More
As neural networks (NNs) are increasingly introduced into safety-critical domains, there is a growing need to formally verify NNs before deployment. In this work we focus on the formal verification problem of NN equivalence which aims to prove that two NNs (e.g. an original and a compressed version) show equivalent behavior. Two approaches have been proposed for this problem: Mixed integer linear programming and interval propagation. While the first approach lacks scalability, the latter is only suitable for structurally similar NNs with small weight changes.
The contribution of our paper has four parts. First, we show a theoretical result by proving that the epsilon-equivalence problem is coNP-complete. Secondly, we extend Tran et al.'s single NN geometric path enumeration algorithm to a setting with multiple NNs. In a third step, we implement the extended algorithm for equivalence verification and evaluate optimizations necessary for its practical use. Finally, we perform a comparative evaluation showing use-cases where our approach outperforms the previous state of the art, both, for equivalence verification as well as for counter-example finding.
△ Less
Submitted 13 December, 2021;
originally announced December 2021.
-
An Incremental Abstraction Scheme for Solving Hard SMT-Instances over Bit-Vectors
Authors:
Samuel Teuber,
Marko Kleine Büning,
Carsten Sinz
Abstract:
Decision procedures for SMT problems based on the theory of bit-vectors are a fundamental component in state-of-the-art software and hardware verifiers. While very efficient in general, certain SMT instances are still challenging for state-of-the-art solvers (especially when such instances include computationally costly functions). In this work, we present an approach for the quantifier-free bit-v…
▽ More
Decision procedures for SMT problems based on the theory of bit-vectors are a fundamental component in state-of-the-art software and hardware verifiers. While very efficient in general, certain SMT instances are still challenging for state-of-the-art solvers (especially when such instances include computationally costly functions). In this work, we present an approach for the quantifier-free bit-vector theory (QF_BV in SMT-LIB) based on incremental SMT solving and abstraction refinement. We define four concrete approximation steps for the multiplication, division and remainder operators and combine them into an incremental abstraction scheme. We implement this scheme in a prototype extending the SMT solver Boolector and measure both the overall performance and the performance of the single approximation steps. The evaluation shows that our abstraction scheme contributes to solving more unsatisfiable benchmark instances, including seven instances with unknown status in SMT-LIB.
△ Less
Submitted 23 August, 2020;
originally announced August 2020.
-
Unbounded Software Model Checking with Incremental SAT-Solving
Authors:
Marko Kleine Büning,
Tomas Balyo,
Carsten Sinz
Abstract:
This paper describes a novel unbounded software model checking approach to find errors in programs written in the C language based on incremental SAT-solving. Instead of using the traditional assumption based API to incremental SAT solvers we use the DimSpec format that is used in SAT based automated planning. A DimSpec formula consists of four CNF formulas representing the initial, goal and inter…
▽ More
This paper describes a novel unbounded software model checking approach to find errors in programs written in the C language based on incremental SAT-solving. Instead of using the traditional assumption based API to incremental SAT solvers we use the DimSpec format that is used in SAT based automated planning. A DimSpec formula consists of four CNF formulas representing the initial, goal and intermediate states and the relations between each pair of neighboring states of a transition system. We present a new tool called LLUMC which encodes the presence of certain errors in a C program into a DimSpec formula, which can be solved by either an incremental SAT-based DimSpec solver or the IC3 algorithm for invariant checking. We evaluate the approach in the context of SAT-based model checking for both the incremental SAT-solving and the IC3 algorithm. We show that our encoding expands the functionality of bounded model checkers by also covering large and infinite loops, while still maintaining a feasible time performance. Furthermore, we demonstrate that our approach offers the opportunity to generate runtime-optimizations by utilizing parallel SAT-solving.
△ Less
Submitted 12 February, 2018;
originally announced February 2018.
