mlsanityData to 14 Oct 2026

PICID: Proof-Driven Clause Learning in Neural Network Verification

arXiv 2503.12083 ↗First posted 15 Mar 2025cs.LO cs.LGcited by 3

Not on the map. Why?

Abstract (arXiv)

Current Deep Neural Network (DNN) verifiers are typically designed to prioritize scalability over reliability. Reliability can be reinforced through the generation of proofs that are checkable by trusted, external proof checkers. To date, only a handful of verifiers support proof production; and these rely on verifier-specific formats, and balance between scalability, proof detail, and the trustworthiness of their proof checker. In this tool paper, we introduce PICID, a DNN verifier that produces proofs in the standard Alethe format for SMT solving, checkable by an independent checker. PICID implements a parallel CDCL(T) architecture that integrates the state-of-the-art, proof-producing CaDiCaL SAT solver with the Marabou DNN verifier. Furthermore, PICID leverages UNSAT proofs to derive conflict clauses. Our evaluation shows that PICID generates valid proofs in the vast majority of cases and significantly outperforms existing tools that produce comparable proofs.

Key facts. Cited by 3 papers in the map (data through 14 Oct 2026). Builds on 47 of its 121 references that are in the map. First posted on arXiv 15 Mar 2025.

Builds on

47 of 121 references.

References · 47

  1. 2013Intriguing properties of neural networkscited by 5,155
  2. 2016End to End Learning for Self-Driving Carscited by 1,009
  3. 2018Threat of Adversarial Attacks on Deep Learning in Computer Vision: A Surveycited by 460
  4. 2016Safety Verification of Deep Neural Networkscited by 263
  5. 2017Formal Verification of Piece-Wise Linear Feed-Forward Neural Networkscited by 242
  6. 2021Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verificationcited by 228
  7. 2018Formal Security Analysis of Neural Networks using Symbolic Intervalscited by 185
  8. 2024Marabou 2.0: A Versatile Formal Analyzer of Neural Networkscited by 81
  9. 2021PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximationscited by 77
  10. 2020Verification of Deep Convolutional Neural Networks Using ImageStarscited by 75
  11. 2021The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Resultscited by 71
  12. 2019An Abstraction-Based Framework for Neural Network Verificationcited by 68
35 more
  1. 2018Deep Neural Network Compression for Aircraft Collision Avoidance Systemscited by 58
  2. 2023First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)cited by 58
  3. 2019Quantitative Verification of Neural Networks And its Security Applicationscited by 56
  4. 2024The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Resultscited by 43
  5. 2022Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networkscited by 42
  6. 2019Fastened CROWN: Tightened Neural Network Robustness Certificatescited by 39
  7. 2020Parallelization Techniques for Verifying Neural Networkscited by 36
  8. 2020Exploiting Verified Neural Networks via Floating Point Numerical Errorcited by 35
  9. 2021Towards Scalable Verification of Deep Reinforcement Learningcited by 33
  10. 2022Verifying Learning-Based Robotic Navigation Systemscited by 33
  11. 2024Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planescited by 33
  12. 2021Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopescited by 26
  13. 2022Efficient Neural Network Analysis with Sum-of-Infeasibilitiescited by 24
  14. 2023A DPLL(T) Framework for Verifying Deep Neural Networkscited by 24
  15. 2023Formally Explaining Neural Networks within Reactive Systemscited by 24
  16. 2022Neural Network Verification with Proof Productioncited by 22
  17. 2022Neuro-Symbolic Verification of Deep Neural Networkscited by 21
  18. 2021Pruning and Slicing Neural Networks using Formal Verificationcited by 20
  19. 2022Verification-Aided Deep Ensemble Selectioncited by 18
  20. 2022Neural Network Verification using Residual Reasoningcited by 18
  21. 2024NLP Verification: Towards a General Methodology for Certifying Robustnesscited by 16
  22. 2021Minimal Multi-Layer Modifications of Deep Neural Networkscited by 14
  23. 2016Efficient Certified RAT Verificationcited by 13
  24. 2022Towards Reliable Neural Specificationscited by 12
  25. 2022veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection Systemcited by 12
  26. 2023Verifying Generalization in Deep Learningcited by 11
  27. 2022Tighter Abstract Queries in Neural Network Verificationcited by 8
  28. 2023DNN Verification, Reachability, and the Exponential Function Problemcited by 8
  29. 2024Robustness Assessment of a Runway Object Classifier for Safe Aircraft Taxiingcited by 8
  30. 2024A Certified Proof Checker for Deep Neural Network Verification in Imandracited by 7
  31. 2024Scalable Synthesis of Formally Verified Neural Value Function for Hamilton-Jacobi Reachability Analysiscited by 7
  32. 2023ANTONIO: Towards a Systematic Method of Generating NLP Benchmarks for Verificationcited by 6
  33. 2023Towards a Certified Proof Checker for Deep Neural Network Verificationcited by 6
  34. 2024DeepCDCL: An CDCL-based Neural Network Verification Frameworkcited by 6
  35. 2021Alethe: Towards a Generic SMT Proof Format (extended abstract)cited by 2

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2025: 2; 2026: 1.

3 papers.

  1. 2025Abstraction-Based Proof Production in Formal Verification of Neural Networkscited by 5
  2. 2025Tighter Truncated Rectangular Prism Approximation for RNN Robustness Verificationcited by 0
  3. 2026Learning Lookahead Lemmas for Neural Network Verificationcited by 0