Source-linked AI summary
An Abstraction-Based Framework for Neural Network Verification
Yizhak Yisrael Elboher, Justin Gottschlich, Guy Katz
TL;DR
Opaque DNNs are difficult to certify, and verification scalability is limited by network size. The paper uses sound over-approximation and counterexample-guided refinement to verify smaller networks, and its Marabou evaluation reports improved performance in most cases.
Problem
DNN opacity complicates certification, and verification becomes exponentially more difficult as network size increases.
Source: §1 · p. 2Method
The framework over-approximates a DNN with a smaller network, merging compatible neurons and refining the abstraction when a counterexample is spurious.
Source: §1 · p. 2Results
On ACAS Xu benchmarks, abstraction-enhanced Marabou significantly outperformed original Marabou in most cases, and small abstractions often sufficed to establish properties of the original networks.
Source: §1 · p. 3Takeaways & Limitations
The abstraction-based approach can reduce network size and boost the performance of existing verification technology.
Source: §7 · p. 20The described verification setting focuses on ReLU networks, conjunctive linear input constraints, and a single output condition y > c.
Source: §2.2 · p. 5
Abstract
from arXiv · showhide
Deep neural networks are increasingly being used as controllers for safety-critical systems. Because neural networks are opaque, certifying their correctness is a significant challenge. To address this issue, several neural network verification approaches have recently been proposed. However, these approaches afford limited scalability, and applying them to large networks can be challenging. In this paper, we propose a framework that can enhance neural network verification techniques by using over-approximation to reduce the size of the network - thus making it more amenable to verification. We perform the approximation such that if the property holds for the smaller (abstract) network, it holds for the original as well. The over-approximation may be too coarse, in which case the underlying verification tool might return a spurious counterexample. Under such conditions, we perform counterexample-guided refinement to adjust the approximation, and then repeat the process. Our approach is orthogonal to, and can be integrated with, many existing verification techniques. For evaluation purposes, we integrate it with the recently proposed Marabou framework, and observe a significant improvement in Marabou's performance. Our experiments demonstrate the great potential of our approach for verifying larger neural networks.
1 Introduction
The paper addresses the scalability limits of neural-network verification with an abstraction-and-refinement framework that verifies smaller networks while preserving soundness. Its Marabou evaluation shows improved performance in most cases.
1 Introduction
- DNN certification is difficult because networks are opaque and small input perturbations can cause severe errors, while verification becomes exponentially harder as networks grow.The verification problem is computationally difficult even for simple specifications and networks.Source: §1 · p. 2
- The framework verifies a smaller abstract network; if a counterexample is spurious, it guides refinement and the process repeats.A property proved for the abstract network also holds for the original network.Source: §1 · p. 2
- Abstraction merges compatible neurons, using neuron classes to preserve over-approximation, while refinement splits merged neurons and heuristics choose which neurons to merge or split.The paper transforms the original network into an equivalent network with four neuron classes before safe merges.Source: §1 · p. 2
- On ACAS Xu benchmarks, abstraction-enhanced Marabou significantly outperformed original Marabou in most cases, and small abstractions often sufficed to establish properties of the original networks.The reported outcomes include properties shown to hold or not hold for the original DNNs.Source: §1 · p. 3
- The contributions are a general DNN over-approximation and refinement framework, abstraction and refinement heuristics, and an implementation integrated with Marabou.The implementation is evaluated on the ACAS Xu benchmark set.Source: §1 · p. 3
2 Background
The background introduces feedforward neural networks and ReLU-based evaluation, then frames verification as checking whether an input satisfying a predicate can produce an output violating the desired property. It also specifies the simplified verification setting used in the paper.
2.1 Neural Networks
- The notation represents each layer's size and value vector, and a suffix network retains layers from a chosen layer onward while treating that layer as input.The illustrated fully connected network has 5 inputs, 5 outputs, and 36 hidden nodes across 4 hidden layers.Source: §2.1 · pp. 3–4, Figure 1 · p. 4
- A feedforward DNN computes hidden-layer values from weighted sums of the preceding layer followed by ReLU, while its output layer applies a linear transformation.The paper assumes zero biases for the rest of its discussion.Source: §2.1 · pp. 3–4
2.2 Neural Network Verification
- Verification asks whether some input satisfying P yields an output satisfying Q, where Q negates the desired property; UNSAT means the property holds, while SAT supplies a counterexample.The query is denoted ⟨N, P, Q⟩.Source: §2.2 · pp. 4–5
- For simplicity, the paper focuses on ReLU networks, conjunctions of linear input constraints, and a single output condition y > c; other properties can often be encoded in this setting.The paper notes that adding neurons for Boolean structure is typically negligible for ACAS Xu and L∞ or L1 adversarial-robustness queries.Source: §2.2 · p. 5
- The abstraction technique is designed to simplify the network while remaining compatible with most existing neural-network verification techniques.Source: §2.2 · p. 5
3 Network Abstraction and Refinement
The framework replaces a network with a smaller over-approximation whose verification can establish the original query, then refines coarse abstractions when they produce spurious counterexamples. It builds the abstraction by classifying and merging neurons, and refinement by splitting merged groups.
3 Network Abstraction and Refinement
- The framework verifies a smaller network with the same properties and ensures that if the abstract query is UNSAT, the original query is also UNSAT.For the single-output setting, it ensures N(x) ≤ N̄(x), so N̄(x) ≤ c implies N(x) ≤ c.Source: §3 · pp. 5–6
- A multi-output disjunction can be converted into an equivalent single-output y > 0 property by adding ReLU neurons and summing their outputs.For y2 > y1 ∨ y2 > y3, each ReLU neuron is positive exactly when its corresponding disjunct holds.Source: Figure 3 · p. 6
3.1 Abstraction
- An equivalent preprocessing transformation labels hidden neurons by outgoing-weight sign and output monotonicity, using at most four times as many neurons.The resulting labels are pos/neg and inc/dec.Source: §3.1 · pp. 6, 8
- Merges combine same-layer neurons with matching labels; for ⟨pos,inc⟩ neurons, incoming weights use a maximum and outgoing weights are summed, while dec cases use a minimum.Each abstraction preserves N̄(x) ≥ N(x).Source: §3.1 · p. 9
- Merging to saturation leaves at most four neurons in each hidden layer, potentially reducing network size substantially.Each merge reduces the network by one neuron.Source: §3.1 · p. 9
3.2 Refinement
- When a coarse abstraction yields a spurious counterexample, refinement splits one abstract group to produce a tighter over-approximation that remains above the original network.The refined network satisfies N(x) ≤ N̄′(x) ≤ N̄(x).Source: §3.2 · pp. 10–11
4 A CEGAR-Based Approach
The CEGAR procedure verifies an over-approximation, checks candidate counterexamples against the original network, and refines spurious ones. Heuristics determine how the initial abstraction is built and how refinement proceeds.
4 A CEGAR-Based Approach
- The procedure is sound and terminates if the underlying verifier terminates, because finitely many refinements can restore the abstract network to the original.It first abstracts, then verifies; a spurious counterexample triggers refinement and another verification round.Source: §4 · p. 12
4.1 Generating an Initial Abstraction
- Saturation merges every compatible same-attribute pair, leaving at most four neurons per hidden layer, but may require repeated refinement when the abstraction is too coarse.Source: §4.1 · p. 13
- Indicator-guided abstraction uses finite P-valid inputs to stop merging once any sampled input violates Q, aiming to reduce later refinement.Source: §4.1 · p. 13
- Among mergeable pairs, the heuristic chooses the pair with the smallest worst incoming-edge weight difference, favoring a closer weight-wise over-approximation.Source: §4.1 · pp. 13–14
4.2 Performing the Refinement Step
- For a spurious counterexample, refinement targets a neuron using both its activation mismatch and incoming-edge weight mismatch; the heuristic ranks candidates by their product.A single refinement may not eliminate the counterexample, so consecutive refinements can be needed.Source: §4.2 · pp. 14–15
5 Implementation and Evaluation
The evaluation integrates abstraction and refinement with Marabou and tests the framework on ACAS Xu properties. Abstraction-enhanced Marabou often improves runtime, including on adversarial-robustness queries, while abstract-network size and solver outcomes vary across experiments.
5 Implementation and Evaluation
- The Python framework reads NNet networks and properties, creates abstractions, invokes a black-box verification engine, and refines until UNSAT or a true counterexample.The implementation integrates with Marabou.Source: §5 · pp. 15–16
- The evaluation covered 45 ACAS Xu networks and properties concerning clear-of-conflict advisories for distant intruders and robustness to small input perturbations.Each network has 300 hidden nodes across six hidden layers before the described preprocessing transformation.Source: §5 · p. 16
- Abstraction to saturation almost always outperformed indicator-guided abstraction, despite potentially requiring more refinement rounds, because its coarse queries were easily solved by Marabou.The comparison plots total time spent solving queries during abstraction-refinement.Source: §5 · pp. 16–17, Figure 7 · p. 17
- 268.8 nodes was the average final network size for terminating abstraction-to-saturation experiments, versus 310 nodes originally, a 13% reduction despite preprocessing initially increasing size fourfold.The final abstract network was usually smaller than the original when the query could be solved.Source: §5 · p. 17
- 58 instances were solved by abstraction-enhanced Marabou versus 35 by vanilla; median runtime was 1045 seconds versus 63671 seconds among instances solved by both.These results compare the abstraction-to-saturation configuration on 90 ACAS Xu benchmarks with a 20-hour timeout.Source: §5 · pp. 17–18, Figure 8 · p. 18
- On 805 jointly solved robustness queries, median runtime was 0.026 seconds for abstraction-enhanced Marabou versus 15.07 seconds for vanilla, though vanilla solved more overall (893 versus 805).The experiment covered 900 queries with δ = 0.1.Source: §5 · pp. 18–19, Figure 9 · p. 19
6 Related Work
Related work spans several DNN verification methods and applications, including approaches that use abstraction. The proposed network-focused abstraction can be paired with sound and complete solvers, while combining it with input-focused abstraction is identified as future work.
6 Related Work
- DNN verification includes SMT, mixed-integer linear programming, symbolic interval propagation, and abstract-interpretation approaches, applied to tasks such as robustness, simplification, and modification.The paper states its approach can be integrated with any sound and complete solver for these tasks.Source: §6 · p. 20
- Prior work over-approximates sigmoid activations with rectangles and uses arbitrary refinement, reporting scalability only to networks with a few dozen neurons; AI2 abstracts inputs and reachable regions instead of the DNN.The paper distinguishes these approaches from its network-focused abstraction.Source: §6 · p. 20
- Combining input-focused abstraction with network-focused abstraction is proposed as an avenue for future work.Incomplete solvers might improve performance, but using them could make the overall approach incomplete.Source: §6 · p. 20
7 Conclusion
Abstraction-based techniques reduce network size to boost existing verification technology without compromising soundness. Future work will broaden the refinement heuristics, activation functions, and parallelization support.
7 Conclusion
- Abstraction-based techniques can reduce network size and boost existing verification technology without compromising verification soundness.The authors describe this as a way to mitigate the difficulty posed by network size.Source: §7 · p. 20
- Future work will investigate arbitrary-sized neuron splits and abstraction schemes for activation functions beyond ReLUs.Source: §7 · p. 20
- The authors also plan to parallelize abstraction and refinement so multiple workers can explore different step combinations, potentially speeding convergence.Source: §7 · p. 20