# Toward Neural-Network-Guided Program Synthesis and Verification

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 18 of its 34 references that are in the map.
- First posted on arXiv 17 Mar 2021.

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

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Explainable Artificial Intelligence (XAI): Concepts, Taxonomies, Opportunities and Challenges toward Responsible AI](https://mlsanity.com/paper/1910.10045/) (2019)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Deep symbolic regression: Recovering mathematical expressions from data via risk-seeking policy gradients](https://mlsanity.com/paper/1912.04871/) (2019)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Programmatically Interpretable Reinforcement Learning](https://mlsanity.com/paper/1804.02477/) (2018)
- [Learning Equations for Extrapolation and Control](https://mlsanity.com/paper/1806.07259/) (2018)
- [Extrapolation and learning equations](https://mlsanity.com/paper/1610.02995/) (2016)
- [Verifying Properties of Binarized Deep Neural Networks](https://mlsanity.com/paper/1709.06662/) (2017)
- [Neurosymbolic Reinforcement Learning with Formally Verified Exploration](https://mlsanity.com/paper/2009.12612/) (2020)
- [An Inductive Synthesis Framework for Verifiable Reinforcement Learning](https://mlsanity.com/paper/1907.07273/) (2019)
- [CLN2INV: Learning Loop Invariants with Continuous Logic Networks](https://mlsanity.com/paper/1909.11542/) (2019)
- [Learning Safe Neural Network Controllers with Barrier Certificates](https://mlsanity.com/paper/2009.09826/) (2020)
- [Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks (Extended Version)](https://mlsanity.com/paper/2003.07959/) (2020)
- [SMT-based Model Checking for Recursive Programs](https://mlsanity.com/paper/1405.4028/) (2014)
- [Horn-ICE Learning for Synthesizing Invariants and Contracts](https://mlsanity.com/paper/1712.09418/) (2017)
- [Overfitting in Synthesis: Theory and Practice (Extended Version)](https://mlsanity.com/paper/1905.07457/) (2019)
- [Data Flow Refinement Type Inference](https://mlsanity.com/paper/2011.04876/) (2020)

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

- [LLM4TDD: Best Practices for Test Driven Development Using Large Language Models](https://mlsanity.com/paper/2312.04687/) (2023)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)

## Abstract (arXiv)

We propose a novel framework of program and invariant synthesis called neural network-guided synthesis. We first show that, by suitably designing and training neural networks, we can extract logical formulas over integers from the weights and biases of the trained neural networks. Based on the idea, we have implemented a tool to synthesize formulas from positive/negative examples and implication constraints, and obtained promising experimental results. We also discuss two applications of our synthesis method. One is the use of our tool for qualifier discovery in the framework of ICE-learning-based CHC solving, which can in turn be applied to program verification and inductive invariant synthesis. Another application is to a new program development framework called oracle-based programming, which is a neural-network-guided variation of Solar-Lezama's program synthesis by sketching.