Proof-Carrying Neuro-Symbolic Code

2025/04/16 by Ekaterina Komendantskaya, Komendantskaya, Ekaterina · 1 voice · 3 citations
Computer Science · #Artificial Intelligence (cs.AI) #F.3.1 #F.3.2 #F.3.3 #FOS: Computer and information sciences #I.2.0 #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL) #cs.AI #cs.LO #cs.PL

paper · pdf · doi:10.48550/arxiv.2504.12031

Abstract

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.

Citations

• Neural Network Verification is a Programming Language Challenge
• Neural Continuous-Time Supermartingale Certificates
• Formal Mathematical Reasoning: A New Frontier in AI
• On Quantifiers for Quantitative Reasoning
• Stochastic Omega-Regular Verification and Control with Supermartingales
• Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates
• A Certified Proof Checker for Deep Neural Network Verification in Imandra
• A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq
• Taming Differentiable Logics with Coq Formalisation
• Provably Safe Neural Network Controllers via Differential Dynamic Logic
• Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
• Compiling High-Level Neural Network Specifications into VNN-LIB Queries
• Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs
• Logic of Differentiable Logics: Towards a Uniform Semantics of DL
• Neural Network Verification with Proof Production
• Neural Network Robustness as a Verification Property: A Principled Case Study
• Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification
• Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification
• The Imandra Automated Reasoning System (system description)
• Exploiting Verified Neural Networks via Floating Point Numerical Error
• Intriguing properties of neural networks
• Proof-Pattern Recognition and Lemma Discovery in ACL2
• Machine Learning in Proof General: Interfacing Interfaces
• First-order Goedel logics
• A Scalable Approach to Probabilistic Neuro-Symbolic Robustness Verification

Discussions

• 📄 “Proof-Carrying Neuro-Symbolic Code” (2025) arxiv.org/abs/2504.12031 📄 “Proof-Carrying Code Completions” (2024) dl.acm.org/doi/pdf/10.1... After Necula (1996) “Proof-carrying code” dl.acm.org/doi/ [bsky, 0 points, 0 comments]

Related

• Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs
• A Semantic Framework for Neuro-Symbolic Computing
• Neuro-Symbolic Artificial Intelligence: Current Trends
• Neural-Symbolic Learning and Reasoning: Contributions and Challenges
• Neurons and Symbols: A Manifesto