mlsanityData to 14 Oct 2026

Efficient Symbolic Reasoning for Neural-Network Verification

arXiv 2303.13588 ↗First posted 23 Mar 2023cs.AI cs.LG cs.SCcited by 1

On the map: LLM reasoning → Reasoning benchmarks and evaluation

Abstract (arXiv)

The neural network has become an integral part of modern software systems. However, they still suffer from various problems, in particular, vulnerability to adversarial attacks. In this work, we present a novel program reasoning framework for neural-network verification, which we refer to as symbolic reasoning. The key components of our framework are the use of the symbolic domain and the quadratic relation. The symbolic domain has very flexible semantics, and the quadratic relation is quite expressive. They allow us to encode many verification problems for neural networks as quadratic programs. Our scheme then relaxes the quadratic programs to semidefinite programs, which can be efficiently solved. This framework allows us to verify various neural-network properties under different scenarios, especially those that appear challenging for non-symbolic domains. Moreover, it introduces new representations and perspectives for the verification tasks. We believe that our framework can bring new theoretical insights and practical tools to verification problems for neural networks.

Key facts. Cited by 1 paper in the map (data through 14 Oct 2026). Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning. Builds on 35 of its 71 references that are in the map. First posted on arXiv 23 Mar 2023.

Builds on

35 of 71 references.

References · 35

  1. 2014Explaining and Harnessing Adversarial Examplescited by 7,364
  2. 2017Towards Deep Learning Models Resistant to Adversarial Attackscited by 6,415
  3. 2013Intriguing properties of neural networkscited by 5,155
  4. 2013Distributed Representations of Words and Phrases and their Compositionalitycited by 3,474
  5. 2016Towards Evaluating the Robustness of Neural Networkscited by 2,998
  6. 2015FaceNet: A Unified Embedding for Face Recognition and Clusteringcited by 2,849
  7. 2015The Limitations of Deep Learning in Adversarial Settingscited by 790
  8. 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 744
  9. 2017Provable defenses against adversarial examples via the convex outer adversarial polytopecited by 567
  10. 2018Certified Defenses against Adversarial Examplescited by 306
  11. 2019Efficient and Accurate Estimation of Lipschitz Constants for Deep Neural Networkscited by 293
  12. 2017Sampling Matters in Deep Embedding Learningcited by 285
23 more
  1. 2016Safety Verification of Deep Neural Networkscited by 263
  2. 2016Understanding Deep Neural Networks with Rectified Linear Unitscited by 257
  3. 2018Formal Security Analysis of Neural Networks using Symbolic Intervalscited by 185
  4. 2018Semidefinite relaxations for certifying robustness to adversarial examplescited by 179
  5. 2021On the Robustness of Vision Transformers to Adversarial Examplescited by 167
  6. 2020Multiscale Deep Equilibrium Modelscited by 151
  7. 2019A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networkscited by 125
  8. 2021Globally-Robust Neural Networkscited by 108
  9. 2016Crafting Adversarial Input Sequences for Recurrent Neural Networkscited by 103
  10. 2020Exactly Computing the Local Lipschitz Constant of ReLU Networkscited by 102
  11. 2020Lipschitz constant estimation of Neural Networks via sparse polynomial optimizationcited by 87
  12. 2020Enabling certification of verification-agnostic networks via memory-efficient semidefinite programmingcited by 66
  13. 2021Training Certifiably Robust Neural Networks with Efficient Local Lipschitz Boundscited by 65
  14. 2021Introduction to Neural Network Verificationcited by 63
  15. 2023A Unified Algebraic Perspective on Lipschitz Neural Networkscited by 60
  16. 2022A Quantitative Geometric Approach to Neural-Network Smoothnesscited by 16
  17. 2022Chordal Sparsity for Lipschitz Constant Estimation of Deep Neural Networkscited by 15
  18. 2020On the Tightness of Semidefinite Relaxations for Certifying Robustness to Adversarial Examplescited by 14
  19. 2020Interval Universal Approximation for Neural Networkscited by 14
  20. 2019Universal Approximation with Certified Networkscited by 9
  21. 2016Termination Analysis of Probabilistic Programs through Positivstellensatz'scited by 8
  22. 2021Exploring Adversarial Robustness of Deep Metric Learningcited by 4
  23. 2013Approximate Constraint Satisfaction Requires Large LP Relaxationscited by 1

Built on by

Cited by year

Citing papers per year: 2024: 1.

1 paper.

  1. 2024CTBENCH: A Library and Benchmark for Certified Trainingcited by 14

Similar, not cited

Close in wording, no citation either way

  1. 2021Verifying Quantized Neural Networks using SMT-Based Model Checking
  2. 2024Symbol Correctness in Deep Neural Networks Containing Symbolic Layers
  3. 2025Verification Learning: Make Unsupervised Neuro-Symbolic System Feasible
  4. 2026The Emergent Symbolic Structure of Artificial Neural Networks
  5. 2024Neuro-symbolic Learning Yielding Logical Constraints
  6. 2024Neural Model Checking
  7. 2025A Comparative Study of Neurosymbolic AI Approaches to Interpretable Logical Reasoning
  8. 2024Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization