# Program Synthesis using Conflict-Driven Learning

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

## Key facts

- Cited by 26 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 21 Nov 2017.

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

- [Magicoder: Empowering Code Generation with OSS-Instruct](https://mlsanity.com/paper/2312.02120/) (2023)
- [PatchPilot: A Cost-Efficient Software Engineering Agent with Early Attempts on Formal Verification](https://mlsanity.com/paper/2502.02747/) (2025)
- [Frontier AI's Impact on the Cybersecurity Landscape](https://mlsanity.com/paper/2504.05408/) (2025)
- [HYSYNTH: Context-Free LLM Approximation for Guiding Program Synthesis](https://mlsanity.com/paper/2405.15880/) (2024)
- [API-guided Dataset Synthesis to Finetune Large Code Models](https://mlsanity.com/paper/2408.08343/) (2024)
- [Guiding Enumerative Program Synthesis with Large Language Models](https://mlsanity.com/paper/2403.03997/) (2024)
- [Program Synthesis Guided Reinforcement Learning for Partially Observed Environments](https://mlsanity.com/paper/2102.11137/) (2021)
- [Scaling Neural Program Synthesis with Distribution-based Search](https://mlsanity.com/paper/2110.12485/) (2021)
- [Generating Pragmatic Examples to Train Neural Program Synthesizers](https://mlsanity.com/paper/2311.05740/) (2023)
- [CodeEvo: Interaction-Driven Synthesis of Code-centric Data through Hybrid and Iterative Feedback](https://mlsanity.com/paper/2507.22080/) (2025)
- [ImageEye: Batch Image Processing Using Program Synthesis](https://mlsanity.com/paper/2304.03253/) (2023)
- [SapientML: Synthesizing Machine Learning Pipelines by Learning from Human-Written Solutions](https://mlsanity.com/paper/2202.10451/) (2022)
- [Reinforcement Learning and Data-Generation for Syntax-Guided Synthesis](https://mlsanity.com/paper/2307.09564/) (2023)
- [Learning programs with magic values](https://mlsanity.com/paper/2208.03238/) (2022)
- [Structured Q-learning For Antibody Design](https://mlsanity.com/paper/2209.04698/) (2022)
- [Synthesizing Programs with Continuous Optimization](https://mlsanity.com/paper/2211.00828/) (2022)
- [Satisfiability and Synthesis Modulo Oracles](https://mlsanity.com/paper/2107.13477/) (2021)
- [Modelling Program Spaces in Program Synthesis with Constraints](https://mlsanity.com/paper/2508.00005/) (2025)
- [Herb.jl: A Unifying Program Synthesis Library](https://mlsanity.com/paper/2510.09726/) (2025)
- [Learning logic programs by explaining their failures](https://mlsanity.com/paper/2102.12551/) (2021)
- [Iterative Genetic Improvement: Scaling Stochastic Program Synthesis](https://mlsanity.com/paper/2202.13040/) (2022)
- [Deterministic Graph-Walking Program Mining](https://mlsanity.com/paper/2208.10290/) (2022)
- [Learning-Based Automatic Synthesis of Software Code and Configuration](https://mlsanity.com/paper/2305.15642/) (2023)
- [Polygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approximation Search](https://mlsanity.com/paper/2504.06542/) (2025)
- [Narcissus: Program Synthesis Using Context-Aware LLM Approximations](https://mlsanity.com/paper/2608.25657/) (2026)
- [Towards Certificate-Driven Software Porting: A Self-Improving Agentic Harness for Scientific Program Optimization](https://mlsanity.com/paper/2609.34069/) (2026)

## Abstract (arXiv)

We propose a new conflict-driven program synthesis technique that is capable of learning from past mistakes. Given a spurious program that violates the desired specification, our synthesis algorithm identifies the root cause of the conflict and learns new lemmas that can prevent similar mistakes in the future. Specifically, we introduce the notion of equivalence modulo conflict and show how this idea can be used to learn useful lemmas that allow the synthesizer to prune large parts of the search space. We have implemented a general-purpose CDCL-style program synthesizer called Neo and evaluate it in two different application domains, namely data wrangling in R and functional programming over lists. Our experiments demonstrate the substantial benefits of conflict-driven learning and show that Neo outperforms two state-of-the-art synthesis tools, Morpheus and Deepcoder, that target these respective domains.