# Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming

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

## Key facts

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

## Builds on (most cited first, 30 of 39)

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [LoRA: Low-Rank Adaptation of Large Language Models](https://mlsanity.com/paper/2106.09685/) (2021)
- [Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks](https://mlsanity.com/paper/2005.11401/) (2020)
- [Sentence-BERT: Sentence Embeddings using Siamese BERT-Networks](https://mlsanity.com/paper/1908.10084/) (2019)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Pythia: A Suite for Analyzing Large Language Models Across Training and Scaling](https://mlsanity.com/paper/2304.01373/) (2023)
- [StarCoder: may the source be with you!](https://mlsanity.com/paper/2305.06161/) (2023)
- [Textbooks Are All You Need](https://mlsanity.com/paper/2306.11644/) (2023)
- [Active Retrieval Augmented Generation](https://mlsanity.com/paper/2305.06983/) (2023)
- [Asleep at the Keyboard? Assessing the Security of GitHub Copilot's Code Contributions](https://mlsanity.com/paper/2108.09293/) (2021)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Unified Pre-training for Program Understanding and Generation](https://mlsanity.com/paper/2103.06333/) (2021)
- [Text and Code Embeddings by Contrastive Pre-Training](https://mlsanity.com/paper/2201.10005/) (2022)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [UniPELT: A Unified Framework for Parameter-Efficient Language Model Tuning](https://mlsanity.com/paper/2110.07577/) (2021)
- [Orca 2: Teaching Small Language Models How to Reason](https://mlsanity.com/paper/2311.11045/) (2023)
- [Retrieval Augmented Code Generation and Summarization](https://mlsanity.com/paper/2108.11601/) (2021)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [NaturalProver: Grounded Mathematical Proof Generation with Language Models](https://mlsanity.com/paper/2205.12910/) (2022)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [Copiloting the Copilots: Fusing Large Language Models with Completion Engines for Automated Program Repair](https://mlsanity.com/paper/2309.00608/) (2023)
- [NatGen: Generative pre-training by "Naturalizing" source code](https://mlsanity.com/paper/2206.07585/) (2022)
- [Verus: Verifying Rust Programs using Linear Ghost Types (extended version)](https://mlsanity.com/paper/2303.05491/) (2023)
- [Interactive Code Generation via Test-Driven User-Intent Formalization](https://mlsanity.com/paper/2208.05950/) (2022)

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

- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement](https://mlsanity.com/paper/2412.06176/) (2024)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification](https://mlsanity.com/paper/2412.14063/) (2024)
- [Agentic AI Software Engineers: Programming with Trust](https://mlsanity.com/paper/2502.13767/) (2025)
- [VeruSAGE: A Study of Agent-Based Verification for Rust Systems](https://mlsanity.com/paper/2512.18436/) (2025)
- [Laurel: Unblocking Automated Verification with Large Language Models](https://mlsanity.com/paper/2405.16792/) (2024)
- [Statically Contextualizing Large Language Models with Typed Holes](https://mlsanity.com/paper/2409.00921/) (2024)
- [RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation](https://mlsanity.com/paper/2502.05344/) (2025)
- [EditLord: Learning Code Transformation Rules for Code Editing](https://mlsanity.com/paper/2504.15284/) (2025)
- [Towards Repository-Level Program Verification with Large Language Models](https://mlsanity.com/paper/2509.25197/) (2025)
- [Can LLMs Enable Verification in Mainstream Programming?](https://mlsanity.com/paper/2503.14183/) (2025)
- [ExVerus: Verus Proof Repair via Counterexample Reasoning](https://mlsanity.com/paper/2603.25810/) (2026)
- [Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcity](https://mlsanity.com/paper/2502.11901/) (2025)
- [Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction](https://mlsanity.com/paper/2602.04892/) (2026)
- [Certified Program Synthesis with a Multi-Modal Verifier](https://mlsanity.com/paper/2604.16584/) (2026)
- [Automating Formal Verification with Reinforcement Learning and Recursive Inference](https://mlsanity.com/paper/2605.30914/) (2026)
- [Harnessing Code Agents for Automatic Software Verification](https://mlsanity.com/paper/2607.06341/) (2026)
- [FVSpec: Real-World Property-Based Tests as Lean Challenges](https://mlsanity.com/paper/2606.01008/) (2026)
- [Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability](https://mlsanity.com/paper/2607.09366/) (2026)

## 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.