The DOI matches its Crossref record; 44 of the 46 references it cites were found in a registry or an index.
Program synthesis using conflict-driven learning
Open accessAbstract
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.
Overview
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Integrity signals
Registry
Cites
Statistics
Verification
Claims the paper makes
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
The cited source says what the claim attributes to it.
In the citing paper
“Neo inherently requires SMT encoded properties for domain specific functions (i.e. its background knowledge).”
From Learning programs by learning from failures (2021) · cites this paper as Feng et al. 2018
The cited source says what the claim attributes to it.
In the citing paper
“Neo (Feng et al. 2018) synthesises non-recursive programs using SMT encoded properties and a three staged loop.”
From Learning programs by learning from failures (2021) · cites this paper as Feng et al. 2018
The cited source says what the claim attributes to it.
In the citing paper
“Neo cannot synthesise recursive programs, nor is it guaranteed to synthesise optimal (textually minimal) programs.”
From Learning programs by learning from failures (2021) · cites this paper as Feng et al. 2018
The cited source says what the claim attributes to it.
In the citing paper
“As it typically uses over-approximate properties, Neo can fail to detect inconsistency with the examples, in which case no programs get pruned.”
From Learning programs by learning from failures (2021) · cites this paper as Feng et al. 2018
The cited source says what the claim attributes to it.
In the citing paper
“Neo cannot synthesise recursive programs, nor is it guaranteed to synthesise optimal (textually minimal) programs.”
From Learning programs by learning from failures (2021) · cites this paper as Feng et al. 2018
Self-check
Percentages, sums and reported differences re-computed from the paper’s own numbers.
The self-check needs the paper’s full text.
Citations
Cites
Sequence to Sequence Learning with Neural Networks
Sutskever, I., Vinyals, O., & Le, Q. V. (2014) · arXiv · doi:10.48550/arxiv.1409.3215 · Cited by 17,766
de Moura, L., & Bjørner, N. (2008) · Lecture Notes in Computer Science · doi:10.1007/978-3-540-78800-3_24 · Cited by 6,595
GRASP: a search algorithm for propositional satisfiability
Marques-Silva, J. P., & Sakallah, K. A. (1999) · IEEE Transactions on Computers · doi:10.1109/12.769433 · Cited by 1,378
Automating string processing in spreadsheets using input-output examples
Gulwani, S. (2011) · ACM-SIGACT Symposium on Principles of Programming Languages · doi:10.1145/1926385.1926423 · Cited by 1,039
Combinatorial sketching for finite programs
Solar-Lezama, A., Tancau, L., Bodík, R., Seshia, S., & Saraswat, V. (2006) · ASPLOS XII · doi:10.1145/1168857.1168907 · Cited by 922
Frontiers in Artificial Intelligence and Applications
To, W., Tryfonas, T., & FARTHING, D. W. (2009) · IOS Press eBooks · Cited by 706
Efficient Conflict Driven Learning in a Boolean Satisfiability Solver
Zhang, L., Madigan, C. F., Moskewicz, M. H., & Malik, S. (2001) · Cited by 682
Alur, R., Bodik, R., Juniwal, G., Martin, M. M. K., Raghothaman, M., Seshia, S. A., Singh, R., Solar-Lezama, A., Torlak, E., & Udupa, A. (2013) · 2013 Formal Methods in Computer-Aided Design · doi:10.1109/fmcad.2013.6679385 · Cited by 656
DeepCoder: Learning to Write ProgramsPreprint
Balog, M., Gaunt, A. L., Brockschmidt, M., Nowozin, S., & Tarlow, D. (2016) · International Conference on Learning Representations · doi:10.48550/arxiv.1611.01989 · Cited by 641
Automating string processing in spreadsheets using input-output examples
Gulwani, S. (2011) · ACM SIGPLAN Notices · doi:10.1145/1925844.1926423 · Cited by 581
Research works printed but not linked: 2
- Arvind Neelakantan , Quoc V Le , Martin Abadi , Andrew McCallum , and Dario Amodei . 2017 . Learning a natural language interface with neural programmer . In Proc. International Conference on Learning Representations . OpenReview. Arvind Neelakantan, Quoc V Le, Martin Abadi, Andrew McCallum, and Dario Amodei. 2017. Learning a natural language interface with neural programmer. In Proc. International Conference on Learning Representations . OpenReview.
- Arvind Neelakantan , Quoc V Le , and Ilya Sutskever . 2016 . Neural programmer: Inducing latent programs with gradient descent . In Proc. International Conference on Learning Representations . OpenReview. Arvind Neelakantan, Quoc V Le, and Ilya Sutskever. 2016. Neural programmer: Inducing latent programs with gradient descent. In Proc. International Conference on Learning Representations . OpenReview.
Cited by
Sorted by citations
Items 101–110 of 110
A SQL Synthesis System with Operator Handler
Wang, H., Dou, Q., Tang, H., Zhang, S., & Pan, H. (2023) · doi:10.1145/3638584.3638654
Polygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approximation Search
Zhao, P., Wang, Y., & Wang, X. (2025) · Proceedings of the ACM on Programming Languages · doi:10.1145/3729303
Synthesizing Document Database Queries Using Collection Abstractions
Liu, Q., He, Y., Cai, Y., Kwak, B., & Wang, Y. (2025) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1109/icse55347.2025.00152
The Role of Interactive Program Synthesis in the Future of Software Development
Shaout, A., Ditty, J., & Carr, K. (2025) · Cureus Journal of Computer Science. · doi:10.7759/s44389-025-05516-x
Multi-modal Sketch-Based Behavior Tree Synthesis
Zhang, W., Chen, Z., & Hong, W. (2025) · Proceedings of the ACM on Programming Languages · doi:10.1145/3763178 · Cited by 1
Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Liu, J., Song, J., Chen, Y., Liu, H., Wen, H., Pearson, L., Chen, Y., & Feng, Y. (2025) · Proceedings of the ACM on Programming Languages · doi:10.1145/3763110
Self-citationHybrid Neuro-Symbolic AI Model for Automated Code Analysis in Software Engineering
Chen, D. L. (2025) · Darpan International Research Analysis · doi:10.36676/dira.v13.i4.186
Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling
Lee, D., Lee, W., & Yi, K. (2026) · Proceedings of the ACM on Programming Languages · doi:10.1145/3776694
SmartIFSyn: Automated Information Flow Security Policy Synthesis for Smart Contracts
Wu, Y., Zhang, M., Song, F., & Baugh, J. W. (2026) · Proceedings of the ACM on software engineering. · doi:10.1145/3797123
Mishra, A. K., & Jagannathan, S. (2026) · Lecture notes in computer science · doi:10.1007/978-3-032-32519-8_15
Metadata
- Authors
- Feng, Y., Martins, R., Bastani, O., & Dillig, I.
- Affiliations
- The University of Texas at Austin (US)
- Carnegie Mellon University (US)
- Massachusetts Institute of Technology (US)
- University of Texas at Austin, USA
- Venue
- Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation
- Publisher
- ACM
- Published
- 2018-06-11
- Pages
- 420-435
- ISSN
- 1531-7102 (ISSN-L)
- OpenAlex
- W2964240296
- Cited by
- 111
- References
- 46
- Citations by year
- 2026: 3 · 2025: 11 · 2024: 8 · 2023: 13 · 2022: 10 · 2021: 18 · 2020: 23 · 2019: 22 · 2018: 3
- FWCI
- 6.71
- Type
- conference paper
- Language
- en
- Open access
- bronze
- doi.org
- Locations
- ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (publishedVersion)
- Funders
- National Science Foundation (1453386)
- Defense Advanced Research Projects Agency (8750-14-2-0270)
- Topics
- Physical Sciences › Computer Science › Artificial Intelligence › Evolutionary Algorithms and Applications
- Physical Sciences › Computer Science › Software › Logic, programming, and type systems
- Physical Sciences › Computer Science › Computer Science Applications › Teaching and Learning Programming
- Keywords
- program synthesis, CDCL, learning from mistakes, search space pruning, data wrangling, functional programming
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
