Generating and Checking DNN Verification Proofs

Thank you for your encouraging comments. We provide our responses to your questions and concerns below.

1. Compare to Marabou checker

We were able to extract APTP proof trees from all 54 problems that Marabou could verify and check proofs.

• Marabou checker (min/median/max): 4/204/785 (seconds)
• APTP checker (min/median/max): 3/9/38 (seconds)

Note that compared to NeuralSAT/α-β-CROWN, Marabou fails to verify many problems. For those that it can solve, Marabou checker is a lot slower than APTP checker as shown.

2. APTP format limited to ReLU

We will clarify in the paper that the APTP format is not restricted to ReLU and can handle any piece-wise linear activations as hidden status can be expressed by logical formulae. For example, for Leaky_a(x) = { x if x ≥ 0 else ax }, it status are expressible by APTP, e.g., (>= Ni 0) for on and (< Ni 0) for off, which is essentially identical to ReLU, while MIP encoding will handle the Leaky operation.

Thank you for your encouraging feedback. We provide our responses to your questions and concerns below.

1. More complex networks

APTPchecker supports FNNs and CNNs but not ResNet. We mentioned in the paper (Sect.5) that this is an engineering limitation rather than a fundamental algorithmic one. For ResNet, the skip connections would require extending our MILP encoding, but the proof checking logic (validating that claimed infeasible branches are indeed infeasible) remains unchanged. The core APTP proof checking approach extends naturally to more complex architectures.

In the last several days we were able to do just that and support Resnet. However, we did not have enough time to run an experiment with it on Resnet benchmarks (we spent most time on extracting Marabou’s code as requested below by you and another reviewer). We'd be happy to add additional results during discussion time if allowed.

2. Compare to Marabou checker

We were able to extract APTP proof trees from all 54 problems that Marabou could verify and check proofs.

• Marabou checker (min/median/max): 4/204/785 (seconds)
• APTP checker (min/median/max): 3/9/38 (seconds)

Note that compared to NeuralSAT/α-β-CROWN, Marabou fails to verify many problems. For those that it can solve, Marabou checker is a lot slower than APTP checker as shown.

thanks! yes, we will include these results to the paper.

Thank you for your time and reviews. We provide our responses to your questions and concerns below.

1. Exponential Constraint Growth.

Yes! The number of constraints can indeed grow exponentially, but APTP already includes mechanisms to reduce them with neural stabilization, tree pruning, and parallelization. Our experiments show that the numbers of proofs (and constraints generated) are moderate, e.g., 601 sub-proofs to be checked on average for proofs generated by NeuralSAT.

2. Contributions of Proof checking over verification

APTP makes the following contributions:

• APTP validates that verifier-claimed infeasible branches are indeed infeasible, rather than searching for satisfying assignments as the verifier does.
• Verifiers like α-β-CROWN and NeuralSAT have many additional steps, optimizations, and heuristics beyond the minimal BnB algorithm presented. In contrast, APTP strictly follows BnB and is independent of all those additional complexities: it only needs to validate the final activation pattern claims, regardless of the sophisticated search strategies, bound tightening techniques, or pruning heuristics used by the verifier.
• Our key contribution is separating proof generation (done by existing verifiers) from proof checking (done by our minimal checker). This provides:
  • Reduced Trusted Computing Base: 800 SLOC checker vs 20K+ SLOC verifiers.
  • Verifier Independence: APTP format works with multiple verifiers (α-β-CROWN, NeuralSAT).
  • Independent Validation step of verification results
  • Checker validation: We attempt to prove the checker itself correct through symbolic execution (Section 6.3 and Appendix B).
  • Multiple solver support: Because we use the MILP solver as a black box, multiple solvers can be employed to increase confidence in results.
  • The APTP format captures activation pattern trees in a verifier-independent way that enables efficient checking while remaining compact and human-readable.
  • Our optimizations target proof checking efficiency (stabilization, pruning, parallelization) rather than verification search efficiency, leading to different algorithmic choices.

3. Runtime table for α-β-CROWN.

We'd be happy to. We have all the data to provide a complete table but they took too much space to include in the paper. We will include all data in the appendix. Here is a summary of the runtimes

• FNN (min/median/max):
  • Verify (4.0/9.0/481.1)
  • Proof check (3.4/19.0/869.7)
• CNN (min/median/max):
  • Verify (6.4/16.4/50.1)
  • Proof check (12.7/67.4/866.1)

In short, the results are similar for α-β-CROWN as expected: verification time is a lot shorter than checking verification results. While proof checking is more expensive than verification, we emphasize that generally speaking one would only check the proofs once. During development as properties and models are evolving one will rerun verification multiple times, but at the very last step when all the properties have proofs that is the time that you will check them. In this context the increased cost of proof checking is not as much of a concern.

Note that in our paper we show these results for NeuralSAT in figure 3, but figures are explicitly not allowed by NeurIPS rebuttal.

4. It would also be helpful to see a table reporting the size and complexity of the DNNs evaluated in your experiments.

We believe Tab.1 (page 7) provides these details of the DNNs. Let us know if you need additional info.

Thank you for your critical review. We’ve carefully considered your comments and provide detailed responses below to address raised concerns.

1. "Toy" models and not scale to networks that current verifiers can handle. Large models require lots of branchings.

We respectfully disagree that our evaluation benchmarks are “toy models”. Our benchmark consists of 400 problems across DNNs with up to 1.7M parameters, which are certainly not toys, even for SoTA DNN verifiers such as ABCrown (e.g., see VNN-COMP'24 results on how these tools struggle on similar or even smaller sizes). Moreover, the only existing proof checking work (Marabou's) evaluates on significantly smaller ACAS Xu networks with just 13K parameters.

The number of constraints created due to large branching indeed is theoretically exponential. However, in practice we do not observe that and more importantly APTP includes various techniques to improve scalability (e.g., neuron stabilization, proof tree pruning, and parallelization) that are shown to be effective in the paper (e.g., 601 proofs in average for proofs generated by NeuralSAT).

2. Overall runtime (of verifying and the validating proofs) is better than simply verifying the underlying models.

We are confused by this question. The purpose of this work is to provide support for verifying the verifier, i.e., we check that reasoning steps of existing DNN verifiers are sound. Thus our work does not aim to compete with verifiers but rather is used after verification to ensure the correctness of the steps performed by the verification implementation.

3. Correctness of MILP solver

We discussed this in the paper (4.1.2): APTP uses the Gurobi MILP solver as a blackbox, and as with all other verification work, we do not prove its correctness. However, our main goal with APTP is not to eliminate all trusted components, but rather to significantly reduce the size of the trusted code base (TCB) necessary to assure that the verification run was sound, so that users can have increased confidence in the result. APTP makes the following contributions toward improving confidence in ML verification: (i) it sets up an architecture to allow for proof checking that is separate from the complex algorithms for DNN verification, allowing their results to be checked independently; (ii) it implements an independent proof checker APTPChecker and goes further by verifying the implementation of the checker itself—this level of formalism and assurance is rarely seen in DNN verification work and reduces the TCB; (iii) the APTP architecture allows for targeting further reductions in the TCB, e.g., in the future the developers can plug in a different MILP solver, to provide increased confidence under the assumption that MILP solver implementations will not be strongly correlated, or replace LP solving with a trusted theorem prover.

We also note that the Marabou checker also relies on the correctness of the blackbox SMT solver used inside Imandra (and if we want to go further it relies on the correctness of its integration of Ocaml). This reliance on solvers (e.g., MILP solver in our case) is a common and accepted trade-off in the SoTA of verification checking.

In summary, while APTP does not eliminate all trust assumptions, it significantly reduces them compared to prior work, providing a framework for DNN verification proof checking. We believe it lays a path toward more trustworthy DNN verification that the community can build on and provides a level of verification of verification results that does not currently exist in the literature.

4. Floating-point (fp) errors due to abstraction/bound computations.

It's a good observation! Indeed, APTP can have fp errors due to the initial bound computation using interval abstraction. However, we do not rely on bound propagation but instead on neuron stability solved by MILP, which is more robust to fp errors compared to complex bound propagation schemes. We note that the initial interval abstraction can be completely replaced by the MILP formulation (Equation 2), e.g., encoding ReLU and solving bounds directly (in fact, the current implementation of APTP does just that and therefore resolves this concern). We also note that the Marabou checker work also relies on abstraction (DeepPoly) and has the same fp concern.

Interestingly, from what you said, verification tools could produce unsound results due to the mentioned fp error issue (due to abstraction and optimizations). If this happens then APTP checker can catch it because it does not have such optimizations and abstractions and instead just recheck their work using MILP solver.

5. Input splitting

We did not consider input splitting which helps deal with networks with low dimensional input spaces. We focus on the major BaB architecture for neuron splittings as challenging and interesting problems since those techniques are used by SoTA NN verifiers and are triggered when verifying networks with lots of neurons and high dimensional inputs.

That said, APTP proof format can be extended easily to handle the input splitting cases where each formula encoding hidden activation is converted to input intervals capturing the input subspace being checked. The core of APTPchecker would remain unchanged as would the level of trust one could place in verification results.

6. Concrete examples of unsound results from neural network verifiers which have been proven unsound by the proposed method.

While we acknowledge this would strengthen the empirical motivation, it does not diminish our contribution's significance. Our evaluation demonstrates that the two state-of-the-art verifiers we tested (α-β-CROWN and NeuralSAT) are sound for the problems we examined - APTPchecker successfully validated 363 out of 400 verification results with no cases where a verifier incorrectly claimed UNSAT.

The primary goal of APTPchecker is to provide independent validation that increases confidence in verification results. When APTPchecker cannot validate a proof, this would lead developers to further investigate whether unsoundness occurred.

Thanks for your questions. We provide our responses below.

1. MNISTFC_GDVB benchmark. Evaluation on diverse benchmarks.

MNISTFC_GDVB was introduced in [Harnessing neuron stability to improve DNN verification - Duong et. al.] in which they used the GDVB tool [Systematic Generation of Diverse Benchmarks for DNN Verification - Xu et. al.] to create diverse (i) networks, by varying network depth and layer width from a given seed network, and (ii) properties, by perturbing radii values (e.g., 0.01 to 0.09). In particular, we use MNISTFC_GDVB networks ranging from 2-6 layers, 16-512 neurons each layer, and 64-3072 ReLU counts (see Tab.1). We believe that these networks, along with the others, are sufficiently diverse.

2. Proof checking is faster than verification?

Proof checking is a lot slower than verification: This might appear counterintuitive and so we'll elaborate. Modern verification tools rely on abstraction for efficiency (e.g., abCrown, NeuralSAT, etc employ advanced abstractions for efficiency), in addition to other heuristics and optimizations --- and many of these are verifiers specific, e.g., tool X uses abstraction Y and heuristic Z. However, these are also what make DNN verification more complex and error-prone. In fact, in our comment to reviewer Pxf9, we mentioned NeuralSAT has soundness bugs due to its optimizations.

Thus, one major design of an independent checker like APTPChecker is that it eschews all these optimizations of verifiers and systematically traverses and checks the proof tree by MILP. Therefore checking these proofs becomes slower than generating them (which can be buggy and incorrect).

Moreover, the other work on DNN proof checking, Marabou checker, is also very slow -- in fact extremely slow as it spent days just to check the results of verifying tiny ACAS XU networks that could be verified by Marabou within seconds. In other words, Marabou checker spent days checking verification results that were obtained in seconds; this support our claim that proof checking is slower than verification.

3. Verification difficulty depends on non-linear components rather than tunable parameters.

We completely agree -- no argument here -- the difficulty of verification depends largely on non-linear components (ReLUs). However, we are unclear about the comment about tunable parameters as we never said that it would affect verification? Perhaps this was because we listed the parameters in Tab 1, and mentioned that our networks have millions of parameters to indicate that they are not toy models? We will clarify in our writing if that's where the confusion stems from, e.g., we can also include that these models have thousands of ReLUs, which imply high complexity.

4. The goal is not sound verification. Motivate other practical aims.

Indeed, our goal is not on sound verification of the model but instead to verify results of verification tools. As suggested by reviewer Pxf9, we agree that a concrete example of our tool detecting unsoundness bugs would be helpful. To address this concern during the rebuttal period, we have found a real problem causing unsoundness in NeuralSAT and we will use it to motivate our work.

5. APTPchecker handles big models. Comparison to verification work RefineZono.

After looking at that paper we believe the reason is because we perform bound optimizations (neuron stabilization) at each layer. Our evaluation in sect 5.1 (figs 4 and 5) shows that this significantly reduces the number of constraints and helps computation. In contrast, the ICLR19 paper relies on zonotopes to compute bounds and uses MILP to tighten bounds--but this is not performed at each layer and instead at some layer K, for some neurons P. Note that hardware advances can also make a difference (e.g., we use an AMD Threadripper 64-core vs. Intel Xeon 14-core/i9 10-core).

6. Input splitting for high-dimensional problems. APTP handles input splitting strategy.

We agree that high-dimensional problems might be beneficial from input splitting and will clarify how APTP handles input splitting strategy as mentioned in our rebuttal, i.e., converting each formula encoding hidden activation to input intervals (supported by APTP), to capture the subspace being checked.

7. Example of unsoundness detected by APTPchecker.

Thank you for the suggested paper, which presents both (i) real bugs and (ii) synthetic bugs. Looking closely at NeuralSAT issue #8 that we mentioned above and to reviewer Pxf9, looks like the reported bug belongs to the category (i) (and from the author of this paper). We will include this example to demonstrate APTPchecker.
In addition, we have looked at the synthetic bugs, and these injected bugs caused the verifiers to randomly miss branches, which APTPchecker will catch (raise errors as invalid proof) because that is the first thing to check that all branches are visited. Thanks for mentioning this work and we will include these to motivate our work.