PICID: Proof-Driven Clause Learning in Neural Network Verification

arXiv:2503.12083 · cs.LO, cs.LG · Submitted 2025-03-15 · Read on arXiv

cs.LO, cs.LG

Submitted: 2025-03-15

Updated: 2026-09-21

Comments: This is a preprint version of the paper that appeared at FMCAD 2026

Code: https://github.com/VNNCOMP/vnncomp2025

License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/

Terminology

• Verification — 82× in this paper · explained in 2 episodes
• Verifier — 40× in this paper · explained in 2 episodes
• Benchmark — 13× in this paper · explained in 2 episodes
• Activation Function — 8× in this paper · explained in 1 episode
• SMT solver — 8× in this paper · explained in 2 episodes
• Formal Methods — 7× in this paper · explained in 3 episodes
• Abstraction — 5× in this paper · explained in 1 episode
• Robustness — 5× in this paper · explained in 5 episodes
• Computer Aided Verification — 4× in this paper
• Core — 4× in this paper · explained in 2 episodes
• Adaptation — 3× in this paper · explained in 1 episode
• Current Deep Neural Network — 2× in this paper
• Formal Verification — 2× in this paper · explained in 2 episodes
• Interactive Theorem Proving — 2× in this paper
• Analyzer — 1× in this paper · explained in 1 episode
• Conflict-Driven Clause Learning — 1× in this paper
• Consistency — 1× in this paper · explained in 3 episodes
• Formal Methods in Computer-Aided Design — 1× in this paper
• Modularity — 1× in this paper · explained in 9 episodes

Sources

• The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results
• A DPLL(T) Framework for Verifying Deep Neural Networks
• The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results
• Neural Network Verification with PyRAT

Related papers

• An Information-Flow Perspective on Explainability Requirements: Specification and Verification
• A programming language combining quantum and classical control
• Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows
• Encoder-Decoder Transformers: Logical Characterizations and Periodicity
• Ultraconstructive Model Theory via Bounded Adversarial Finite Structures