# A Theory of Formal Synthesis via Inductive Learning

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

## Key facts

- Cited by 17 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 15 May 2015.

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

- [Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems](https://mlsanity.com/paper/2405.06624/) (2024)
- [Interactive Code Generation via Test-Driven User-Intent Formalization](https://mlsanity.com/paper/2208.05950/) (2022)
- [ALGO: Synthesizing Algorithmic Programs with LLM-Generated Oracle Verifiers](https://mlsanity.com/paper/2305.14591/) (2023)
- [Machine Unlearning Doesn't Do What You Think: Lessons for Generative AI Policy and Research](https://mlsanity.com/paper/2412.06966/) (2024)
- [Guiding Enumerative Program Synthesis with Large Language Models](https://mlsanity.com/paper/2403.03997/) (2024)
- [NeuRI: Diversifying DNN Generation via Inductive Rule Inference](https://mlsanity.com/paper/2302.02261/) (2023)
- [Neuro Symbolic Reasoning for Planning: Counterexample Guided Inductive Synthesis using Large Language Models and Satisfiability Solving](https://mlsanity.com/paper/2309.16436/) (2023)
- [Data-driven Design of Context-aware Monitors for Hazard Prediction in Artificial Pancreas Systems](https://mlsanity.com/paper/2104.02545/) (2021)
- [Reinforcement Learning and Data-Generation for Syntax-Guided Synthesis](https://mlsanity.com/paper/2307.09564/) (2023)
- [CDRL: Certification-Driven Reinforcement Learning for Neutrino Flavor Model Discovery](https://mlsanity.com/paper/2608.20686/) (2026)
- [Supervised Bayesian Specification Inference from Demonstrations](https://mlsanity.com/paper/2107.02912/) (2021)
- [Satisfiability and Synthesis Modulo Oracles](https://mlsanity.com/paper/2107.13477/) (2021)
- [ExPairT-LLM: Exact Learning for LLM Code Selection by Pairwise Queries](https://mlsanity.com/paper/2511.10855/) (2025)
- [Formal Policy Learning from Demonstrations for Reachability Properties](https://mlsanity.com/paper/1903.00589/) (2019)
- [Metric-Guided Synthesis of Class Activation Mapping](https://mlsanity.com/paper/2504.09998/) (2025)
- [Hypothesis Frontier: Verifier Guided LLM and Symbolic Search for First-Order Induction](https://mlsanity.com/paper/2608.10843/) (2026)
- [Self-evolving network verifiers](https://mlsanity.com/paper/2608.11340/) (2026)

## Abstract (arXiv)

Formal synthesis is the process of generating a program satisfying a high-level formal specification. In recent times, effective formal synthesis methods have been proposed based on the use of inductive learning. We refer to this class of methods that learn programs from examples as formal inductive synthesis. In this paper, we present a theoretical framework for formal inductive synthesis. We discuss how formal inductive synthesis differs from traditional machine learning. We then describe oracle-guided inductive synthesis (OGIS), a framework that captures a family of synthesizers that operate by iteratively querying an oracle. An instance of OGIS that has had much practical impact is counterexample-guided inductive synthesis (CEGIS). We present a theoretical characterization of CEGIS for learning any program that computes a recursive language. In particular, we analyze the relative power of CEGIS variants where the types of counterexamples generated by the oracle varies. We also consider the impact of bounded versus unbounded memory available to the learning algorithm. In the special case where the universe of candidate programs is finite, we relate the speed of convergence to the notion of teaching dimension studied in machine learning theory. Altogether, the results of the paper take a first step towards a theoretical foundation for the emerging field of formal inductive synthesis.