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
In-IDE Code Generation from Natural Language: Promise and Challenges
Xu, F. F., Vasilescu, B., & Neubig, G. (2022) · ACM Transactions on Software Engineering and Methodology · doi:10.1145/3487569 · Cited by 154
“Besides visual no-code or low-code programming interfaces, there has also been much progress on program synthesis [12, 29, 31, 108], which uses input-output examples, logic sketches, etc.”
Background(2021) · doi:10.1145/3510003.3510203 · Cited by 139
Fuzz testing based data augmentation to improve robustness of deep neural networks
Gao, X. Y., Saha, R. K., Prasad, M. R., & Roychoudhury, A. (2020) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1145/3377811.3380415 · Cited by 129
Learning programs by learning from failures
Cropper, A., & Morel, R. (2021) · Machine Learning · doi:10.1007/s10994-020-05934-z · Cited by 86
“Indeed, PL approaches rarely evaluate the ability of their systems to synthesise solutions that generalise, i.e. they do not measure predictive accuracy (Feser et al. 2015; Polikarpova et al. 2016; Albarghouthi et al. 2017; Feng et al. 2018; Raghothaman et al. 2020).”
BackgroundMethodGenerative Code Modeling with GraphsPreprint
Brockschmidt, M., Allamanis, M., Gaunt, A. L., & Polozov, O. (2018) · arXiv (Cornell University) · doi:10.48550/arxiv.1805.08490 · Cited by 103
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
