mlsanityData to 7 Oct 2026

Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming

arXiv 2405.01787 ↗First posted 3 May 2024cs.PL cs.AI cs.SEcited by 19

Not on the map. Why?

Abstract (arXiv)

Proof-oriented programs mix computational content with proofs of program correctness. However, the human effort involved in programming and proving is still substantial, despite the use of Satisfiability Modulo Theories (SMT) solvers to automate proofs in languages such as F*. Seeking to spur research on using AI to automate the construction of proof-oriented programs, we curate a dataset of 600K lines of open-source F* programs and proofs, including software used in production systems ranging from Windows and Linux to Python and Firefox. Our dataset includes around 32K top-level F* definitions, each representing a type-directed program and proof synthesis problem producing a definition given a formal specification expressed as an F* type. We provide a program fragment checker that queries F* to check the correctness of candidate solutions. We also report on an extended version of our dataset containing a total of 940K lines of programs and proofs, with a total of 54k top-level F* definitions. We believe this is the largest corpus of SMT-assisted program proofs coupled with a reproducible program-fragment checker. Grounded in this dataset, we investigate the use of AI to synthesize programs and their proofs in F*, with promising results. Our main finding in that the performance of fine-tuned smaller language models (such as Phi-2 or StarCoder) compare favorably with large language models (such as GPT-4), at a much lower computational cost. We also identify various type-based retrieval augmentation techniques and find that they boost performance significantly. With detailed error analysis and case studies, we identify potential strengths and weaknesses of models and techniques and suggest directions for future improvements.

Key facts. Cited by 19 papers in the map (data through 7 Oct 2026). Builds on 39 of its 74 references that are in the map. First posted on arXiv 3 May 2024.

Builds on

39 of 74 references.

References · 39

  1. 2023GPT-4 Technical Reportcited by 18,132
  2. 2021LoRA: Low-Rank Adaptation of Large Language Modelscited by 14,084
  3. 2020Retrieval-Augmented Generation for Knowledge-Intensive NLP Taskscited by 9,160
  4. 2019Sentence-BERT: Sentence Embeddings using Siamese BERT-Networkscited by 9,049
  5. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  6. 2023Pythia: A Suite for Analyzing Large Language Models Across Training and Scalingcited by 1,734
  7. 2023StarCoder: may the source be with you!cited by 790
  8. 2023Textbooks Are All You Needcited by 561
  9. 2023Active Retrieval Augmented Generationcited by 506
  10. 2021Asleep at the Keyboard? Assessing the Security of GitHub Copilot's Code Contributionscited by 417
  11. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  12. 2021Unified Pre-training for Program Understanding and Generationcited by 361
27 more
  1. 2022Text and Code Embeddings by Contrastive Pre-Trainingcited by 358
  2. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  3. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  4. 2021UniPELT: A Unified Framework for Parameter-Efficient Language Model Tuningcited by 162
  5. 2023Orca 2: Teaching Small Language Models How to Reasoncited by 157
  6. 2021Retrieval Augmented Code Generation and Summarizationcited by 148
  7. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  8. 2019The Lean mathematical librarycited by 127
  9. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  10. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  11. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
  12. 2022NaturalProver: Grounded Mathematical Proof Generation with Language Modelscited by 72
  13. 2023Clover: Closed-Loop Verifiable Code Generationcited by 62
  14. 2024Towards AI-Assisted Synthesis of Verified Dafny Methodscited by 58
  15. 2023Copiloting the Copilots: Fusing Large Language Models with Completion Engines for Automated Program Repaircited by 55
  16. 2022NatGen: Generative pre-training by "Naturalizing" source codecited by 53
  17. 2022Interactive Code Generation via Test-Driven User-Intent Formalizationcited by 50
  18. 2023Magnushammer: A Transformer-Based Approach to Premise Selectioncited by 50
  19. 2023Verus: Verifying Rust Programs using Linear Ghost Types (extended version)cited by 50
  20. 2018TacticToe: Learning to Prove with Tacticscited by 43
  21. 2024MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Datacited by 43
  22. 2019Generating Correctness Proofs with Neural Networkscited by 36
  23. 2023Finding Inductive Loop Invariants using Large Language Modelscited by 35
  24. 2023Ranking LLM-Generated Loop Invariants for Program Verificationcited by 33
  25. 2023GrACE: Generation using Associated Code Editscited by 16
  26. 2023Leveraging Large Language Models for Automated Proof Synthesis in Rustcited by 11
  27. 2017Verified Low-Level Programming Embedded in F*cited by 3

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2024: 6; 2025: 7; 2026: 6.

19 papers.

Sort:

By area:

  1. 2024AutoVerus: Automated Proof Generation for Rust Codecited by 46
  2. 2024AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinementcited by 33
  3. 2024Automated Proof Generation for Rust Code via Self-Evolutioncited by 31
  4. 2024Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verificationcited by 25
  5. 2025Agentic AI Software Engineers: Programming with Trustcited by 19
  6. 2025VeruSAGE: A Study of Agent-Based Verification for Rust Systemscited by 11
  7. 2024Laurel: Unblocking Automated Verification with Large Language Modelscited by 10
  8. 2024Statically Contextualizing Large Language Models with Typed Holescited by 9
  9. 2025EditLord: Learning Code Transformation Rules for Code Editingcited by 4
  10. 2025Towards Repository-Level Program Verification with Large Language Modelscited by 4
  11. 2025RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generationcited by 3
  12. 2025Can LLMs Enable Verification in Mainstream Programming?cited by 3
7 more
  1. 2025Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcitycited by 2
  2. 2026Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Inductioncited by 2
  3. 2026Certified Program Synthesis with a Multi-Modal Verifiercited by 2
  4. 2026ExVerus: Verus Proof Repair via Counterexample Reasoningcited by 1
  5. 2026Harnessing Code Agents for Automatic Software Verificationcited by 1
  6. 2026FVSpec: Real-World Property-Based Tests as Lean Challengescited by 0
  7. 2026Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiabilitycited by 0