Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Proof Minimization in Neural Network Verification

Omri Isac, Idan Refaeli, Haoze Wu, Clark Barrett, Guy Katz

TL;DR

This paper tackles the challenge of prohibitively large UNSAT proofs produced by DNN verifiers and proposes a two-stage proof minimization workflow: a proof-dependency analysis to drop unused lemmas, followed by two greedy/global minimization strategies to further prune dependencies. The authors implement these techniques on the Marabou proof-producing verifier and evaluate them across six benchmarks, achieving average proof-size reductions of 37%–82% and proof-checking-time reductions up to 88%, with a modest verifier overhead of 7%–20%. The approach leverages a Farkas-lemma-based UNSAT certificate and formalizes proof dependencies through $w^T A V = \sum c_i x_i$, enabling on-the-fly lemma deletion and memory savings. Overall, the method significantly improves the scalability and reliability of proof-producing DNN verifiers, facilitating safer deployment in safety-critical applications.

Abstract

The widespread adoption of deep neural networks (DNNs) requires efficient techniques for verifying their safety. DNN verifiers are complex tools, which might contain bugs that could compromise their soundness and undermine the reliability of the verification process. This concern can be mitigated using proofs: artifacts that are checkable by an external and reliable proof checker, and which attest to the correctness of the verification process. However, such proofs tend to be extremely large, limiting their use in many scenarios. In this work, we address this problem by minimizing proofs of unsatisfiability produced by DNN verifiers. We present algorithms that remove facts which were learned during the verification process, but which are unnecessary for the proof itself. Conceptually, our method analyzes the dependencies among facts used to deduce UNSAT, and removes facts that did not contribute. We then further minimize the proof by eliminating remaining unnecessary dependencies, using two alternative procedures. We implemented our algorithms on top of a proof producing DNN verifier, and evaluated them across several benchmarks. Our results show that our best-performing algorithm reduces proof size by 37%-82% and proof checking time by 30%-88%, while introducing a runtime overhead of 7%-20% to the verification process itself.

Proof Minimization in Neural Network Verification

TL;DR

This paper tackles the challenge of prohibitively large UNSAT proofs produced by DNN verifiers and proposes a two-stage proof minimization workflow: a proof-dependency analysis to drop unused lemmas, followed by two greedy/global minimization strategies to further prune dependencies. The authors implement these techniques on the Marabou proof-producing verifier and evaluate them across six benchmarks, achieving average proof-size reductions of 37%–82% and proof-checking-time reductions up to 88%, with a modest verifier overhead of 7%–20%. The approach leverages a Farkas-lemma-based UNSAT certificate and formalizes proof dependencies through , enabling on-the-fly lemma deletion and memory savings. Overall, the method significantly improves the scalability and reliability of proof-producing DNN verifiers, facilitating safer deployment in safety-critical applications.

Abstract

The widespread adoption of deep neural networks (DNNs) requires efficient techniques for verifying their safety. DNN verifiers are complex tools, which might contain bugs that could compromise their soundness and undermine the reliability of the verification process. This concern can be mitigated using proofs: artifacts that are checkable by an external and reliable proof checker, and which attest to the correctness of the verification process. However, such proofs tend to be extremely large, limiting their use in many scenarios. In this work, we address this problem by minimizing proofs of unsatisfiability produced by DNN verifiers. We present algorithms that remove facts which were learned during the verification process, but which are unnecessary for the proof itself. Conceptually, our method analyzes the dependencies among facts used to deduce UNSAT, and removes facts that did not contribute. We then further minimize the proof by eliminating remaining unnecessary dependencies, using two alternative procedures. We implemented our algorithms on top of a proof producing DNN verifier, and evaluated them across several benchmarks. Our results show that our best-performing algorithm reduces proof size by 37%-82% and proof checking time by 30%-88%, while introducing a runtime overhead of 7%-20% to the verification process itself.

Paper Structure

This paper contains 21 sections, 2 theorems, 9 equations, 5 figures, 5 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Background
  3. Deep Neural Networks and their Verification
  4. Proof Production for DNN Verification
  5. Proof Dependency Analysis and Minimization
  6. Analyzing Proof Dependencies
  7. Minimizing the Number of Proof Dependencies
  8. Proof Minimization.
  9. Global Heuristic for Proof Minimization.
  10. Additional Improvements and Lemma Deletion
  11. Implementation and Evaluation
  12. Experimental Setup and Implementation
  13. Evaluation
  14. Acas-Xu Benchmark.
  15. cersyve Benchmark.
  16. ...and 6 more sections

Key Result

theorem thmcountertheorem

Observe the constraints $A\cdot V = \bar{0}$ and $l \leq V \leq u$, where $A \in M_{m \times n} (\mathbb{R})$ and $l,V,u \in \mathbb{R}^{n}$. The constraints are UNSAT if and only if $\exists w \in \mathbb{R}^{m}$ such that for $w^\intercal \cdot A \cdot V \coloneq \underset{i=1}{\overset{n}{\sum}}c

Figures (5)

  • Figure 1: A toy DNN with ReLU activations.
  • Figure 2: A proof tree example with a single node (orange). Given the query $Q$, two lemmas (blue) are learned before deriving UNSAT (red).
  • Figure 3: Using \ref{['alg:lemmadeduction']} over the proof vector used to derive UNSAT (red) shows that a single lemma (blue) is used during the proof process, and the other (gray) is not. All proof vectors use information in the root query $Q$ (orange)
  • Figure 4: Using \ref{['alg:proofmin']} over the proof vector used to derive UNSAT (red) shows that both lemmas (gray) are unnecessary for proving UNSAT.
  • Figure 5: Proof size and runtime comparison across all benchmarks and methods.

Theorems & Definitions (11)

  • Example 1
  • Example 2
  • Example 3
  • theorem thmcountertheorem: Farkas Lemma Variant (From IsBaZhKa22)
  • Example 4
  • Example 5
  • Example 6
  • theorem thmcountertheorem
  • proof
  • Example 7
  • ...and 1 more