mlsanityData to 7 Oct 2026

Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcity

arXiv 2502.11901 ↗First posted 17 Feb 2025cs.CL cs.PL cs.SEcited by 2

On the map: LLM reasoning → Mathematical reasoning

Abstract (arXiv)

Existing LMs struggle with proof-oriented programming due to data scarcity, which manifest in two key ways: (1) a lack of sufficient corpora for proof-oriented programming languages such as F*, and (2) the absence of large-scale, project-level proof-oriented implementations that can teach the model the intricate reasoning process when performing proof-oriented programming. We present the first on synthetic data augmentation for project level proof oriented programming for both generation and repair. Our method addresses data scarcity by synthesizing basic proof-oriented programming problems for proficiency in that language; incorporating diverse coding data for reasoning capability elicitation and creating new proofs and repair data within existing repositories. This approach enables language models to both synthesize and repair proofs for function- and repository-level code. We show that our fine-tuned 14B parameter model, PoPilot, can exceed the performance of the models that outperforms GPT-4o in project-level proof-oriented programming by 64% relative margin, and can improve GPT-4o's performance by 54% by repairing its outputs over GPT-4o's self-repair.

Key facts. Cited by 2 papers in the map (data through 7 Oct 2026). Placed in Mathematical reasoning, one of 17 directions in LLM reasoning. Builds on 38 of its 63 references that are in the map. First posted on arXiv 17 Feb 2025.

Builds on

38 of 63 references.

References · 38

  1. 2022Training language models to follow instructions with human feedbackcited by 15,712
  2. 2021LoRA: Low-Rank Adaptation of Large Language Modelscited by 14,084
  3. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  4. 2021Finetuned Language Models Are Zero-Shot Learnerscited by 3,747
  5. 2022Training a Helpful and Harmless Assistant with Reinforcement Learning from Human Feedbackcited by 3,634
  6. 2021Program Synthesis with Large Language Modelscited by 3,509
  7. 2023SWE-bench: Can Language Models Resolve Real-World GitHub Issues?cited by 3,193
  8. 2022Self-Instruct: Aligning Language Models with Self-Generated Instructionscited by 2,674
  9. 2023Code Llama: Open Foundation Models for Codecited by 2,105
  10. 2024DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligencecited by 1,154
  11. 2023WizardLM: Empowering large pre-trained language models to follow complex instructionscited by 1,116
  12. 2024DeepSeek-V2: A Strong, Economical, and Efficient Mixture-of-Experts Language Modelcited by 1,093
26 more
  1. 2023LIMA: Less Is More for Alignmentcited by 1,080
  2. 2023Teaching Large Language Models to Self-Debugcited by 963
  3. 2022CodeGen: An Open Large Language Model for Code with Multi-Turn Program Synthesiscited by 876
  4. 2023WizardCoder: Empowering Code Large Language Models with Evol-Instructcited by 728
  5. 2023OpenAssistant Conversations -- Democratizing Large Language Model Alignmentcited by 712
  6. 2024StarCoder 2 and The Stack v2: The Next Generationcited by 484
  7. 2023LMSYS-Chat-1M: A Large-Scale Real-World LLM Conversation Datasetcited by 449
  8. 2024Magpie: Alignment Data Synthesis from Scratch by Prompting Aligned LLMs with Nothingcited by 341
  9. 2023Magicoder: Empowering Code Generation with OSS-Instructcited by 251
  10. 2023Large Language Model as Attributed Training Data Generator: A Tale of Diversity and Biascited by 230
  11. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  12. 2023How Abilities in Large Language Models are Affected by Supervised Fine-tuning Data Compositioncited by 222
  13. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  14. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
  15. 2023InferFix: End-to-End Program Repair with LLMscited by 113
  16. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  17. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 97
  18. 2024SelfCodeAlign: Self-Alignment for Code Generationcited by 61
  19. 2024DafnyBench: A Benchmark for Formal Software Verificationcited by 54
  20. 2023Knowledge Transfer from High-Resource to Low-Resource Programming Languages for Code LLMscited by 45
  21. 2020Learning to Prove Theorems by Learning to Generate Theoremscited by 43
  22. 2024CodecLM: Aligning Language Models with Tailored Synthetic Datacited by 39
  23. 2023Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Provingcited by 37
  24. 2024Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programmingcited by 19
  25. 2024CoqPilot, a plugin for LLM-based generation of proofscited by 10
  26. 2024Only-IF:Revealing the Decisive Effect of Instruction Diversity on Generalizationcited by 7

Built on by

Cited by year

Citing papers per year: 2025: 2.

2 papers.

  1. 2025A Comprehensive Survey on Benchmarks and Solutions in Software Engineering of LLM-Empowered Agentic Systemcited by 15
  2. 2025A Pilot Study on LLM-Based Agentic Translation from Android to iOS: Pitfalls and Insightscited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2026P3: Joint Program-and-Proof Planning for Verified Code Generation
  2. 2026TheoremForge: Scaling up Formal Data Synthesis with Low-Budget Agentic Workflow
  3. 2024Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification
  4. 2025ProofCompass: Enhancing Specialized Provers with LLM Guidance
  5. 2026Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification
  6. 2025Towards Repository-Level Program Verification with Large Language Models
  7. 2024Investigating the Transferability of Code Repair for Low-Resource Programming Languages
  8. 2024Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast