# Safe Neurosymbolic Learning with Differentiable Symbolic Execution

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

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- Builds on 20 of its 42 references that are in the map.
- First posted on arXiv 15 Mar 2022.

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

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Certified Adversarial Robustness via Randomized Smoothing](https://mlsanity.com/paper/1902.02918/) (2019)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [A Reductions Approach to Fair Classification](https://mlsanity.com/paper/1803.02453/) (2018)
- [Batch Policy Learning under Constraints](https://mlsanity.com/paper/1903.08738/) (2019)
- [Towards Stable and Efficient Training of Verifiably Robust Neural Networks](https://mlsanity.com/paper/1906.06316/) (2019)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Verifiable Reinforcement Learning via Policy Extraction](https://mlsanity.com/paper/1805.08328/) (2018)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Gradient Estimation Using Stochastic Computation Graphs](https://mlsanity.com/paper/1506.05254/) (2015)
- [Neural Lander: Stable Drone Landing Control using Learned Dynamics](https://mlsanity.com/paper/1811.08027/) (2018)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [An Abstraction-Based Framework for Neural Network Verification](https://mlsanity.com/paper/1910.14574/) (2019)
- [Introduction to Neural Network Verification](https://mlsanity.com/paper/2109.10317/) (2021)
- [Formal Verification of Neural Network Controlled Autonomous Systems](https://mlsanity.com/paper/1810.13072/) (2018)
- [Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness](https://mlsanity.com/paper/1904.09959/) (2019)
- [A Survey of Symbolic Execution Techniques](https://mlsanity.com/paper/1610.00502/) (2016)
- [Symbolic Execution for Deep Neural Networks](https://mlsanity.com/paper/1807.10439/) (2018)

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

- [Neuro-Symbolic AI in 2024: A Systematic Review](https://mlsanity.com/paper/2501.05435/) (2025)
- [Smoothing Methods for Automatic Differentiation Across Conditional Branches](https://mlsanity.com/paper/2310.03585/) (2023)
- [Certifiably Robust Reinforcement Learning through Model-Based Abstract Interpretation](https://mlsanity.com/paper/2301.11374/) (2023)
- [On the Promise for Assurance of Differentiable Neurosymbolic Reasoning Paradigms](https://mlsanity.com/paper/2502.08932/) (2025)
- [A Synergistic Approach In Network Intrusion Detection By Neurosymbolic AI](https://mlsanity.com/paper/2406.00938/) (2024)
- [Canopy: Property-Driven Learning for Congestion Control](https://mlsanity.com/paper/2412.10915/) (2024)
- [Composing Linear Layers from Irreducibles](https://mlsanity.com/paper/2507.11688/) (2025)
- [SAIL: Sound Abstract Interpreters with LLMs](https://mlsanity.com/paper/2511.13663/) (2025)
- [Scaling Up without Fading Out: Goal-Aware Sparse GNN for RL-based Generalized Planning](https://mlsanity.com/paper/2508.10747/) (2025)

## Abstract (arXiv)

We study the problem of learning worst-case-safe parameters for programs that use neural networks as well as symbolic, human-written code. Such neurosymbolic programs arise in many safety-critical domains. However, because they can use nondifferentiable operations, it is hard to learn their parameters using existing gradient-based approaches to safe learning. Our approach to this problem, Differentiable Symbolic Execution (DSE), samples control flow paths in a program, symbolically constructs worst-case "safety losses" along these paths, and backpropagates the gradients of these losses through program operations using a generalization of the REINFORCE estimator. We evaluate the method on a mix of synthetic tasks and real-world benchmarks. Our experiments show that DSE significantly outperforms the state-of-the-art DiffAI method on these tasks.