Pith. sign in

REVIEW 3 major objections 5 minor 45 references

From Provable Correctness to Probabilistic Generation: A Comparative Review of Program Synthesis Paradigms

T0 review · 3 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Program synthesis's fifty-year arc runs from proof-checked code to probabilistic generation, with neuro-symbolic verifiers as the likely next step.

desk verdict A well-organized but unoriginal survey whose reliability is undermined by at least one checkable factual error and some sloppy editing. read the letter →

arxiv 2508.00013 v1 pith:HH5CIB5U submitted 2025-07-21 cs.PL

Zurabi Kobaladze , Anna Arnania , Tamar Sanikidze This is my paper
classification cs.PL
keywords programsynthesisdeductiveinductivesketch-basedlargelanguagemodelsneuro-symboliccorrectnessguaranteesspecificationburden
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This review maps fifty years of program synthesis as a single long trade-off between how much the user must specify and how strongly the generated code can be trusted. It distinguishes five paradigms — deductive, inductive, sketch-based, LLM-based, and neuro-symbolic — and argues that each sits at a different point on the same axes of specification burden, search complexity, expressive power, and correctness guarantees. The central claim is that the field's arc runs from provably correct code extracted from formal proofs (KIDS, Coq) to statistically likely code sampled from large language models (Codex, AlphaCode), and that the two extremes are now being reconciled in hybrid neuro-symbolic systems where a neural generator proposes code and a symbolic verifier checks it. If the narrative is right, it explains why mainstream synthesis shifted its target from correctness to usability, and why the current frontier is verification technology rather than generation technology alone.

What carries the argument

The comparative framework itself, organized around five paradigms, carries the argument; within each paradigm, the central mechanism is the pairing of a specification form with a search strategy and a correctness guarantee. The paper names the concrete instantiations: proof extraction via the Curry-Howard correspondence (propositions as types) for deductive synthesis (KIDS, Coq); a domain-specific language plus version-space search for inductive synthesis (FlashFill); holes filled by a counterexample-guided inductive synthesis (CEGIS) loop, a generate-and-check cycle against a verifier, for sketch synthesis (Sketch, Rosette); autoregressive token prediction over code corpora for LLM synthesis (Codex, AlphaCode); and a verifier-in-the-loop architecture — often a CEGIS loop with the LLM as generator — for neuro-symbolic synthesis. These mechanisms pin the paper's abstract trade-offs to concrete systems.

What would settle it

Reproduce the claimed empirical anchor: run a large code LLM on the HumanEval benchmark using the sampling-and-filtering protocol described in the paper and compare the pass@100 rate against the reported 70.2%; a large shortfall would show the review's central performance datum is not reproducible, and with it the credibility of its comparative narrative.

Watch

Extended reading notes

Core claim

On the paper's own terms, the discovery is that the history of program synthesis is coherently organized by a single tension: correctness guarantees are purchased with specification burden, and every paradigm is a different point on that curve. Deductive synthesis asks for complete formal specifications and returns programs correct by construction; inductive synthesis asks only for examples and returns hypotheses that generalize without logical guarantee; sketch synthesis asks for program structure and hands the correctness problem back to a solver; LLM-based synthesis asks for natural language and returns samples that must be filtered and tested; neuro-symbolic synthesis re-introduces symbolic checkers to make the probabilistic output trustworthy. The review treats these not as competing technologies but as successive answers to the same bottleneck, with the LLM era relaxing the input problem and the neuro-symbolic era attacking the output problem.

Load-bearing premise

The review assumes its secondary sources are accurate, so if key reported performance figures — such as Codex's 70.2% pass@100 or AlphaCode's Elo 1238 — are misquoted or invented, the narrative's empirical grounding fails without an internal check to catch it.

Editorial extensions

If this is right

  • If the review's narrative is correct, users of LLM code generation should expect no formal guarantee and should treat generated programs as hypotheses that need tests or a verifier.
  • The next generation of synthesis tools will likely couple a neural generator with a symbolic checker, because the review says pure neural generation hits a correctness impasse and pure symbolic synthesis hits a specification bottleneck.
  • Example-based specification tools will keep expanding for non-experts, since the review identifies that as the pragmatic path that succeeded commercially with FlashFill.
  • Formal-method synthesis will remain confined to safety-critical domains, where the review judges the specification burden acceptable.
  • Evaluation in the LLM paradigm will keep centering on functional-correctness metrics such as pass@k rather than on text similarity.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • An implication the paper leaves implicit: the correctness-versus-specification relationship could be measured empirically across all five paradigms, plotting user specification effort against empirical failure rates on a shared benchmark suite.
  • Extending the review's reasoning, continued LLM scaling will shift demand toward cheap verification — test generation, lightweight formal checkers, and self-debugging — because generation has already crossed the usability threshold for many common tasks.
  • A testable extension: take a set of tasks from a modern benchmark such as HumanEval and implement the same tasks under each of the five paradigms, then compare correctness, specification effort, and runtime; this would convert the historical narrative into a controlled experiment.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. This manuscript is a bachelor's thesis that surveys five program synthesis paradigms: logic-based (deductive) synthesis, inductive (example-based) synthesis, sketch/schema-based synthesis, LLM-based synthesis, and neuro-symbolic hybrids. It traces the field's evolution from formal proof-based systems (KIDS, Coq) to probabilistic code generation (Codex, AlphaCode), and to current neuro-symbolic approaches. For each paradigm, it discusses foundational principles, representative systems, methodological techniques, applications, and trade-offs. The central claim is that this comparative account accurately synthesizes the field's progress and highlights the shift toward hybrid neuro-symbolic architectures.

Significance. If the survey were reliable, it would provide a broad, accessible overview of program synthesis, useful for students and researchers entering the area. The manuscript covers the major paradigms, includes several well-chosen examples (FlashFill, Sketch/Rosette, DreamCoder, verifier-in-the-loop LLM systems), and presents a clear taxonomy of neuro-symbolic integration styles. The paper contains no formal proofs or experimental evaluations; its value depends entirely on accurate secondary reporting. That reliability is undermined by a false flagship claim about KIDS and by numerous citation misattributions in the later chapters, which are load-bearing for the survey's usefulness as a reference document.

major comments (3)
  1. [§1.3.1] The claim that KIDS solved the k-Queens problem by producing 'a highly efficient, constant-time solution' is implausible and unsupported by the cited Smith (1990) reference. For arbitrary k, any correct algorithm must at least read the input and emit an output, so constant time is impossible in the standard computational model; for fixed k, the statement is trivial and not a meaningful efficiency result. This example is presented as evidence that deductive synthesis was practically effective, so the error is load-bearing. Please remove the claim or replace it with a documented KIDS application (e.g., the scheduling or algorithm-design examples that appear in Smith's publications).
  2. [§2.1.3] The raw LaTeX command 'citepgulwani2011automating' appears in the running text. This formatting artifact indicates the manuscript was not thoroughly proofread. Similar citation inconsistencies appear throughout: §5.3.1 attributes Neural-Guided Deductive Search (NGDS) to [Ellis et al., 2021], but NGDS is introduced in a 2018 paper by Kalyan et al.; §5.4.1 cites [Kaplan et al., 2020] for the LLM-based CEGIS loop, but Kaplan et al. is the scaling-laws paper; §5.4.2 attributes Chain-of-Thought prompting to [Kleinberg et al., 2018], though the technique originates with Wei et al. (2022). A survey's reliability depends on correct attribution; these errors require systematic correction and re-verification against primary sources.
  3. [§4.3.2] The statement that AlphaCode's estimated Codeforces Elo of 1238 placed it 'in the top 54.3% of human competitors' is misleading. The primary source states that 1238 is higher than 54.3% of participants, which corresponds to approximately the 54th percentile, i.e., the top 45.7%. As worded, the claim misrepresents the empirical result. Please correct this and re-verify all quantitative claims in §4.3 (Codex pass@k values, AlphaCode 2 solve rates, MBPP numbers in Table 4.1) against the cited papers.
minor comments (5)
  1. [§5.4] The phrase 'internet-scale corals of text' should read 'internet-scale corpora of text'.
  2. [Title page] The affiliation line 'Universitatea de Vest din Timis, oara' contains a word-splitting artifact; it should be 'Timișoara'.
  3. [§5.2.6] The claim about DSL restrictiveness is attributed to [Devlin et al., 2017], but the cited work (RobustFill, by Devlin et al.) is not the natural source for this general DSL-design trade-off; a more standard reference would be Gulwani et al. or Solar-Lezama.
  4. [§5.3.1] The citation for Neural-Guided miniKanren is given as [Facchin, 2023]; please provide the full author list and venue, and verify that this work is described accurately.
  5. [§4.3.3 and Table 4.1] The LaMDA-PT row in Table 4.1 lists 'MBPP: 58% pass@k (few-shot), 68% (fine-tuned)', but pass@k requires specifying k; please clarify which k these figures refer to and ensure consistency with the source.

Circularity Check

0 steps flagged · score 0.0 of 10

Survey contains no derivation chain; no predictions reduce to fitted inputs or self-citations, so no circularity found.

full rationale

This paper is a comparative literature review of program synthesis paradigms. It does not derive new results, fit parameters, or make predictions that are then compared with data; its claims are historical and descriptive, and each substantive assertion is attributed to external primary sources (e.g., Green 1969, Manna and Waldinger 1980, Smith 1990, Gulwani 2011, Chen et al. 2021, Li et al. 2022). The only work by an author-adjacent figure is the discussion of Dramnesc's proof-based synthesis of sorting algorithms, cited as external literature and used as an example of the deductive paradigm rather than as support for a novel claim of this thesis. There is no equation in which an output quantity is defined in terms of itself, no fitted input renamed as a prediction, and no load-bearing argument whose premise is supplied by a self-citation. The reader's flagged concern about the plausibility of the constant-time k-queens claim in Section 1.3.1 is a matter of factual accuracy and source fidelity, not circularity: even if the claim were a misreading, it would not make the survey's narrative equivalent to its inputs by construction. Accordingly, the appropriate circularity score is 0.

Assumptions & free parameters 0 free parameters · 2 assumptions · 0 invented entities

The thesis is a review; it introduces no free parameters or entities. Its central assumptions are about the accuracy and representativeness of the cited literature.

assumptions (2)
  • domain assumption The secondary literature cited in the thesis accurately reports the behavior and performance of the synthesis systems described.
    All technical content is imported from external sources; the thesis itself does not run experiments or formal proofs.
  • domain assumption The five chosen paradigms and the selected landmark systems are representative of the program synthesis field.
    The thesis selects KIDS, Coq, FlashFill, Sketch, Codex, AlphaCode, DeepCoder, DreamCoder and others as the canonical examples without a systematic sampling method.

how reviews work

0 comments
Cite this review

Pith. "Pith review of From Provable Correctness to Probabilistic Generation: A Comparative Review of Program Synthesis Paradigms." pith.science (2026). https://pith.science/paper/HH5CIB5U

@misc{pith2026250800013,
  author       = {Pith},
  title        = {Pith review of: From Provable Correctness to Probabilistic Generation: A Comparative Review of Program Synthesis Paradigms},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HH5CIB5U}},
  note         = {Machine review of arXiv:2508.00013}
}
read the original abstract

Program synthesis--the automated generation of executable code from high-level specifications--has been a central goal of computer science for over fifty years. This thesis provides a comparative literature review of the main paradigms that have shaped the field, tracing its evolution from formal logic based methods to recent advances using large scale neural models. We examine five key approaches: logic based (deductive) synthesis, inductive (example based) synthesis, sketch/schema based synthesis, large language model based synthesis, and neuro-symbolic hybrids. For each, we analyze foundational principles, notable systems, and practical applications, highlighting trade offs between correctness guarantees, specification requirements, search complexity, and expressive power. By reviewing developments from formally verified synthesis tools such as KIDS and Coq to data driven models generating probabilistic code from natural language like Codex, we present a comprehensive narrative of progress and ongoing challenges. This work emphasizes the transition from symbolic to hybrid neuro-symbolic methods and outlines future directions for reliable and scalable program synthesis.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

45 extracted references · 34 canonical work pages

  1. [8]

    Execution-Guided Neural Program Synthesis

    Xinyun Chen, Chang Liu, and Dawn Song. Execution-Guided Neural Program Synthesis. In 6th International Conference on Learning Representations, ICLR 2018,

    work page 2018

  2. [12]

    Smooth Bilevel Programming for Sparse Regularization

    Marta Garnelo and Murray Shanahan. A survey of neuro-symbolic artificial intelligence. arXiv preprint arXiv:2106.01429,

    work page Pith review arXiv

  3. [13]

    Cordell Green

    Accessed: 2025-07-01. Cordell Green. Application of theorem proving to problem solving. Proceedings of the 1st inter- national joint conference on Artificial intelligence, pages 219–239,

    work page 2025

  4. [14]

    On the naturalness of software

    72 Abram Hindle, Earl T Barr, Mark Gabel, and Zhendong Su. On the naturalness of software. In 2012 34th International Conference on Software Engineering (ICSE) , pages 837–847. IEEE,

    work page 2012

  5. [15]

    Nvidia gtc 2023 keynote,

    Jensen Huang. Nvidia gtc 2023 keynote,

    work page 2023

  6. [16]

    Joomy Jeo, Won-Kee Lee, and Kwangkeun Yi

    Accessed: 2025-07-01. Joomy Jeo, Won-Kee Lee, and Kwangkeun Yi. Synthesizing formal semantics for a program synthesis problem from an executable interpreter. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation , pages 859– 874,

    work page 2025

  7. [17]

    Learning to Synthesize Programs as Interpretable and Generalizable Policies

    Meng Jin et al. Learning to Synthesize Programs as Interpretable and Generalizable Policies. In Proceedings of the 39th International Conference on Machine Learning, ICML 2022,

    work page 2022

  8. [19]

    Oscillations and differences in Triebel-Lizorkin-Morrey spaces

    Jean Kaddour, Joshua Harris, Maximilian Mozes, Herbie Stevens, Jonathan Sivert, Thomas Un- terthiner, and Jean-Baptiste Lespiau. Challenges and applications of large language models. arXiv preprint arXiv:2306.15239,

    work page Pith review arXiv

Show all 45 references
  1. [22]

    Wizardcoder: Empowering code large language models with evolution-in-instruction

    Ziyang Luo, Can Li, Yuchen Sun, Weixiang Wang, Yuxiang Sun, Yixuan Shi, Wenchao Hu, Shice Zhang, Ziyu Chen, Hong-Bin Zhou, et al. Wizardcoder: Empowering code large language models with evolution-in-instruction. arXiv preprint arXiv:2306.08568,

    arXiv

  2. [23]

    Doc-ify: Automatic end-to-end documentation generation for python code

    Brandon Ma et al. Doc-ify: Automatic end-to-end documentation generation for python code. arXiv preprint arXiv:2311.12328,

    arXiv

  3. [24]

    A deductive approach to program synthesis

    Zohar Manna and Richard Waldinger. A deductive approach to program synthesis. ACM Transac- tions on Programming Languages and Systems (TOPLAS), 2(1):90–121, 1980a. Zohar Manna and Richard Waldinger. A deductive approach to program synthesis. ACM, 1980b. Jiayuan Mao, Chuang Gan...

    2019

  4. [26]

    Logic-lm: Empowering large lan- guage models with symbolic solvers for logical reasoning

    Liangming Pan, Ram Al-Rfou, Zihang Li, and Zhiting Zhao. Logic-lm: Empowering large lan- guage models with symbolic solvers for logical reasoning. arXiv preprint arXiv:2305.12295, 2023a. 74 Zhaowei Pan, Yixuan Zhu, Jia Liu, Yuhang Liu, Zhipeng Wang, Yu Yan, Yueling Sun, and Ya...

    arXiv

  5. [27]

    Automating file system manipulation and string transformations from examples

    Ruzica Piskac, Johannes Mayer, and Viktor Kuncak. Automating file system manipulation and string transformations from examples. InProceedings of the 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 726–731. IEEE,

    2015

  6. [29]

    Reflexion: an autonomous agent with dynamic memory and self-reflection

    Noah Shinn, Beck Labash, and Ashwin Gopinath. Reflexion: an autonomous agent with dynamic memory and self-reflection. arXiv preprint arXiv:2303.11366,

    arXiv

  7. [30]

    Neuro- Symbolic Execution: Augmenting Symbolic Execution with Neural Constraints

    Sun Shiqi, Sudipta Shinde, Srivatsan Ramesh, Abhik Roychoudhury, and Prateek Saxena. Neuro- Symbolic Execution: Augmenting Symbolic Execution with Neural Constraints. In NDSS Sym- posium 2019,

    2019

  8. [31]

    Jsketch: sketch-based synthesis for java

    Gagandeep Singh, Chiao Shi, and Armando Solar-Lezama. Jsketch: sketch-based synthesis for java. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 686–704,

    2016

  9. [33]

    CLUTRR: A Diagnostic Benchmark for Inductive Reasoning from Text

    Koustuv Sinha, , et al. CLUTRR: A Diagnostic Benchmark for Inductive Reasoning from Text. In Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing,

    2019

  10. [34]

    Auto-composing domain-specific data plane programs

    75 Anirudh Sivaraman, Srinivas Kaki, Vignesh Jeyakumar, Leonid Poutievski, Amin Vahdat, and George Varghese. Auto-composing domain-specific data plane programs. In Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, pages 234–248,

    2018

  11. [35]

    Chip-chat: A large language model for chip design

    Shailja Thakur et al. Chip-chat: A large language model for chip design. arXiv preprint arXiv:2401.12284,

    arXiv

  12. [37]

    Trustsketch: A trustworthy sketch-based telemetry system with sgx

    Paulo Vasconcelos, João Cunha, David Isidoro, Rui Mendes, and Nuno Santos. Trustsketch: A trustworthy sketch-based telemetry system with sgx. In 2020 50th Annual IEEE/IFIP Interna- tional Conference on Dependable Systems and Networks (DSN), pages 15–27. IEEE,

    2020

  13. [38]

    HOUDINI: Lifelong Learning as Program Synthesis

    Mor Vered et al. HOUDINI: Lifelong Learning as Program Synthesis. In Proceedings of the 39th International Conference on Machine Learning, ICML 2022,

    2022

  14. [39]

    A survey on large language model based autonomous agents

    Lei Wang, Chen Ma, Xueyang Feng, Zeyu Zhang, Hao Yang, Jingsen Zhang, Zhiyuan Chen, Jiakai Tang, Wen_chi Chen, Yujiu Zhang, et al. A survey on large language model based autonomous agents. arXiv preprint arXiv:2308.11432,

    arXiv

  15. [40]

    Ethical and social risks of harm from language models

    Laura Weidinger, John Mellor, Maribeth Rauh, Conor Griffin, Jonathan Uesato, Po-Sen Huang, Myra Cheng, Mia Glaese, Borja Balle, Atoosa Kasirzadeh, et al. Ethical and social risks of harm from language models. arXiv preprint arXiv:2112.04359,

    arXiv

  16. [41]

    Differentiable Symbolic Execution

    Cannon Yang, , et al. Differentiable Symbolic Execution. In 10th International Conference on Learning Representations, ICLR 2022,

    2022

  17. [42]

    Large language models for software engineering: A systematic literature review

    Siyuan Zeng, Zepeng Liu, Zhiming Chen, Ziqing Su, Tianyi Wang, Kaixuan Wu, Xing Wang, and Shang-Wei Ma. Large language models for software engineering: A systematic literature review. arXiv preprint arXiv:2402.13179,

    arXiv

  18. [43]

    A Framework for General-Purpose Behavior Modeling

    Eric Zhan, , et al. A Framework for General-Purpose Behavior Modeling. In arXiv preprint arXiv:2104.09501,

    arXiv

  19. [45]

    Algo: Synthesizing algorithmic programs with oracle-guided learning

    Yewen Zhang, Swaroop Wang, Parth Roy, and Alvin Cheung. Algo: Synthesizing algorithmic programs with oracle-guided learning. arXiv preprint arXiv:2405.07123, 2024a. Zichu Zhang, Yuxiang Zhang, Shang-Yi Feng, Jing Chen, and Lei Li. Proof-of-Thought: A Controllable and Verifiabl...

    arXiv

  20. [1987]

    Language models are few-shot learners

    70 Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. Language models are few-shot learners. In Advances in neural information processing systems, volume 33, pages 1877–1901,

    1901

  21. [1993]

    RobustFill: Neural Program Learning Under Noisy I/O

    Jacob Devlin, Jonathan Uesato, Surya Bhupatiraju, and et al. RobustFill: Neural Program Learning Under Noisy I/O. In Proceedings of the 34th International Conference on Machine Learning, ICML 2017,

    2017

  22. [2001]

    ISBN 1581133898

    Associ- ation for Computing Machinery. ISBN 1581133898. doi: 10.1145/502034.502042. URL https://doi.org/10.1145/502034.502042. Miles Cranmer. Interpretable and Steerable Sequence Learning with Recurrent Neural Networks. In arXiv preprint arXiv:2002.08386,

  23. [2004]

    Hudson, Ehsan Adeli, and et al

    Rishi Bommasani, Drew A. Hudson, Ehsan Adeli, and et al. On the Opportunities and Risks of Foundation Models. In arXiv preprint arXiv:2108.07258,

    arXiv

  24. [2009]

    Multilingual code generation with knowledge distillation

    Jacob Austin, Augustus Odena, Maxwell Nye, Maarten Bosma, Henryk Michalewski, David Do- han, Ellen Jiang, Carrie Cai, Michael Terry, Quoc Le, et al. Multilingual code generation with knowledge distillation. arXiv preprint arXiv:2109.10852,

    arXiv

  25. [2011]

    Brown, Benjamin Chess, Rewon Child, Scott Gray, Chris Hallacy, Jan Leike, Heewoo Lee, et al

    Jared Kaplan, Sam McCandlish, Tom Henighan, Tom B. Brown, Benjamin Chess, Rewon Child, Scott Gray, Chris Hallacy, Jan Leike, Heewoo Lee, et al. Scaling Laws for Neural Language Models. In arXiv preprint arXiv:2001.08361,

    2001 arXiv

  26. [2013]

    Syntax- guided synthesis

    Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo MK Martin, Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. Syntax- guided synthesis. In Formal Methods in Computer-Aided Design (FMCAD), 2013 , pages 1–8. IEEE,

    2013

  27. [2014]

    Codearc: A code abstraction and reasoning challenge for large language models

    Kechi Lee et al. Codearc: A code abstraction and reasoning challenge for large language models. arXiv preprint arXiv:2402.13848,

    arXiv

  28. [2015]

    Synthesizing program transformations for database schema refac- toring

    Linyuan Qiu and Alvin Cheung. Synthesizing program transformations for database schema refac- toring. In 2018 IEEE/ACM 40th International Conference on Software Engineering (ICSE) , pages 694–705. IEEE,

    2018

  29. [2016]

    Interpretable program synthesis

    Gurbir Singh and Armando Solar-Lezama. Interpretable program synthesis. In ICML 2018 Work- shop on Human Interpretability in Machine Learning (WHI 2018),

    2018

  30. [2017]

    Beyond basic prose: A survey of programming with large language models

    71 Victor Dibia. Beyond basic prose: A survey of programming with large language models. In Proceedings of the 2023 ACM on International Conference on Multimodal Interaction , pages 945–950,

    2023

  31. [2018]

    Fusing formal and informal methods: A case for large language models in verifier-driven program synthesis

    Qiaochu Zhang, Zichao Li, Yeting Liu, Zhi Yang, and Lixin Sun. Fusing formal and informal methods: A case for large language models in verifier-driven program synthesis. arXiv preprint arXiv:2305.09560,

    arXiv

  32. [2019]

    User study of a pbe-based command-line text processing tool

    Johannes Mayer, Ruzica Piskac, and Viktor Kuncak. User study of a pbe-based command-line text processing tool. In Proceedings of the 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 261–271. IEEE,

    2015

  33. [2020]

    Sparks of artificial general intelligence: Early experiments with gpt-4

    Sébastien Bubeck, Varun Chandrasekaran, Ronen Eldan, Johannes Gehrke, Eric Horvitz, Ece Ka- mar, Peter Lee, Yin Tat Lee, Yuanzhi Li, Scott Lundberg, et al. Sparks of artificial general intelligence: Early experiments with gpt-4. arXiv preprint arXiv:2303.12712,

    arXiv

  34. [2021]

    Evaluating large language models trained on code

    Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique de Paulo Pires, Hieu Le, Boris Hvy, Shida Gu, Jared hammock, Denny D’souza, et al. Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374,

    arXiv

  35. [2022]

    Termite-2: A system for user- guided synthesis of device drivers

    Pallavi Joshi, Mayur Naik, George C Necula, and Koushik Sen. Termite-2: A system for user- guided synthesis of device drivers. In 2007 USENIX Annual Technical Conference (USENIX ATC’07), pages 321–334,

    2007

  36. [2023]

    Leverag- ing Grammar and Reinforcement Learning for Neural Program Synthesis

    Rudy Bunel, Matthew Hausknecht, Jacob Devlin, Rishabh Singh, and Pushmeet Kohli. Leverag- ing Grammar and Reinforcement Learning for Neural Program Synthesis. In 6th International Conference on Learning Representations, ICLR 2018,

    2018

  37. [2024]

    Learning Programmatic Task Representations for Applications in Neuro-Symbolic Learning

    Melissa Tjandrasuwita, , et al. Learning Programmatic Task Representations for Applications in Neuro-Symbolic Learning. In arXiv preprint arXiv:2106.09623,

    arXiv

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.