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

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

## Key facts

- Cited by 2 papers in the map (data through 14 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.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

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

- [Training language models to follow instructions with human feedback](https://mlsanity.com/paper/2203.02155/) (2022)
- [LoRA: Low-Rank Adaptation of Large Language Models](https://mlsanity.com/paper/2106.09685/) (2021)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Finetuned Language Models Are Zero-Shot Learners](https://mlsanity.com/paper/2109.01652/) (2021)
- [Training a Helpful and Harmless Assistant with Reinforcement Learning from Human Feedback](https://mlsanity.com/paper/2204.05862/) (2022)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [Self-Instruct: Aligning Language Models with Self-Generated Instructions](https://mlsanity.com/paper/2212.10560/) (2022)
- [Code Llama: Open Foundation Models for Code](https://mlsanity.com/paper/2308.12950/) (2023)
- [DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligence](https://mlsanity.com/paper/2401.14196/) (2024)
- [DeepSeek-V2: A Strong, Economical, and Efficient Mixture-of-Experts Language Model](https://mlsanity.com/paper/2405.04434/) (2024)
- [WizardLM: Empowering large pre-trained language models to follow complex instructions](https://mlsanity.com/paper/2304.12244/) (2023)
- [LIMA: Less Is More for Alignment](https://mlsanity.com/paper/2305.11206/) (2023)
- [Teaching Large Language Models to Self-Debug](https://mlsanity.com/paper/2304.05128/) (2023)
- [CodeGen: An Open Large Language Model for Code with Multi-Turn Program Synthesis](https://mlsanity.com/paper/2203.13474/) (2022)
- [WizardCoder: Empowering Code Large Language Models with Evol-Instruct](https://mlsanity.com/paper/2306.08568/) (2023)
- [OpenAssistant Conversations -- Democratizing Large Language Model Alignment](https://mlsanity.com/paper/2304.07327/) (2023)
- [StarCoder 2 and The Stack v2: The Next Generation](https://mlsanity.com/paper/2402.19173/) (2024)
- [LMSYS-Chat-1M: A Large-Scale Real-World LLM Conversation Dataset](https://mlsanity.com/paper/2309.11998/) (2023)
- [Magpie: Alignment Data Synthesis from Scratch by Prompting Aligned LLMs with Nothing](https://mlsanity.com/paper/2406.08464/) (2024)
- [Magicoder: Empowering Code Generation with OSS-Instruct](https://mlsanity.com/paper/2312.02120/) (2023)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [Large Language Model as Attributed Training Data Generator: A Tale of Diversity and Bias](https://mlsanity.com/paper/2306.15895/) (2023)
- [How Abilities in Large Language Models are Affected by Supervised Fine-tuning Data Composition](https://mlsanity.com/paper/2310.05492/) (2023)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [InferFix: End-to-End Program Repair with LLMs](https://mlsanity.com/paper/2303.07263/) (2023)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [SelfCodeAlign: Self-Alignment for Code Generation](https://mlsanity.com/paper/2410.24198/) (2024)

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

- [A Comprehensive Survey on Benchmarks and Solutions in Software Engineering of LLM-Empowered Agentic System](https://mlsanity.com/paper/2510.09721/) (2025)
- [A Pilot Study on LLM-Based Agentic Translation from Android to iOS: Pitfalls and Insights](https://mlsanity.com/paper/2507.16037/) (2025)

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