# Proof-Carrying Neuro-Symbolic Code

arXiv: https://arxiv.org/abs/2504.12031 · HTML: https://mlsanity.com/paper/2504.12031/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 27 of its 58 references that are in the map.
- First posted on arXiv 16 Apr 2025.

## Builds on (most cited first, 27 of 27)

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [Deep Learning with Logical Constraints](https://mlsanity.com/paper/2205.00523/) (2022)
- [Exploiting Verified Neural Networks via Floating Point Numerical Error](https://mlsanity.com/paper/2003.03021/) (2020)
- [Neural Network Robustness as a Verification Property: A Principled Case Study](https://mlsanity.com/paper/2104.01396/) (2021)
- [Neural Network Verification with Proof Production](https://mlsanity.com/paper/2206.00512/) (2022)
- [Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates](https://mlsanity.com/paper/2405.14058/) (2024)
- [Logic of Differentiable Logics: Towards a Uniform Semantics of DL](https://mlsanity.com/paper/2303.10650/) (2023)
- [Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs](https://mlsanity.com/paper/2401.06379/) (2024)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Stochastic Omega-Regular Verification and Control with Supermartingales](https://mlsanity.com/paper/2405.17304/) (2024)
- [CAISAR: A platform for Characterizing Artificial Intelligence Safety and Robustness](https://mlsanity.com/paper/2206.03044/) (2022)
- [Provably Safe Neural Network Controllers via Differential Dynamic Logic](https://mlsanity.com/paper/2402.10998/) (2024)
- [A Certified Proof Checker for Deep Neural Network Verification in Imandra](https://mlsanity.com/paper/2405.10611/) (2024)
- [Comparing differentiable logics for learning with logical constraints](https://mlsanity.com/paper/2407.03847/) (2024)
- [Neural Continuous-Time Supermartingale Certificates](https://mlsanity.com/paper/2412.17432/) (2024)
- [The Imandra Automated Reasoning System (system description)](https://mlsanity.com/paper/2004.10263/) (2020)
- [Proof-Pattern Recognition and Lemma Discovery in ACL2](https://mlsanity.com/paper/1308.1780/) (2013)
- [Propositional Logics for the Lawvere Quantale](https://mlsanity.com/paper/2302.01224/) (2023)
- [Compiling High-Level Neural Network Specifications into VNN-LIB Queries](https://mlsanity.com/paper/2402.01353/) (2024)
- [Taming Differentiable Logics with Coq Formalisation](https://mlsanity.com/paper/2403.13700/) (2024)
- [Measure Construction by Extension in Dependent Type Theory with Application to Integration](https://mlsanity.com/paper/2209.02345/) (2022)
- [On Quantifiers for Quantitative Reasoning](https://mlsanity.com/paper/2406.04936/) (2024)
- [Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification](https://mlsanity.com/paper/2102.01644/) (2021)
- [A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq](https://mlsanity.com/paper/2403.18229/) (2024)

## Built on by (most cited first, 1 of 1)

- [Proof-Carrying Materials: Falsifiable Safety Certificates for Machine-Learned Interatomic Potentials](https://mlsanity.com/paper/2603.12183/) (2026)

## Abstract (arXiv)

This invited paper introduces the concept of "proof-carrying neuro-symbolic code" and explains its meaning and value, from both the "neural" and the "symbolic" perspectives. The talk outlines the first successes and challenges that this new area of research faces.