Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcity
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.
Code (0)
등록된 구현이 없습니다.
Tasks
Data AugmentationSimilar Papers 제목 키워드 기반
Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
Neural theorem proving combines large language models (LLMs) with proof assistants such as Lean, where the correctness of formal proofs can be rigorously verified, leaving no room for hallucination. With existing neural …
Automated Theorem ProvingHallucinationMachine Translation from Natural Language to Code using Long-Short Term Memory
Making computer programming language more understandable and easy for the human is a longstanding problem. From assembly language to present day's object-oriented programming, concepts came to make programming easier so …
BIG-bench Machine LearningMachine TranslationTranslationWatChat: Explaining perplexing programs by debugging mental models
Often, a good explanation for a program's unexpected behavior is a bug in the programmer's code. But sometimes, an even better explanation is a bug in the programmer's mental model of the language or API they are using. …
counterfactualLanguage ModellingMisconceptionsProgram SynthesisCodeClash: Benchmarking Goal-Oriented Software Engineering
Current benchmarks for coding evaluate language models (LMs) on concrete, well-specified tasks such as fixing specific bugs or writing targeted tests. However, human programmers do not spend all day incessantly addressin…
A Problem-Oriented Perspective and Anchor Verification for Code Optimization
Large language models (LLMs) have shown remarkable capabilities in solving various programming tasks, such as code generation. However, their potential for code optimization, particularly in performance enhancement, rema…
Code Generation