用合成数据提升代码证明模型性能，比GPT-4o快64%。
Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcity
- 通过合成项目级代码证明数据，解决训练数据不足问题。
- 140亿参数模型PoPilot在项目级证明任务上超GPT-4o 64%。
- 可修复GPT-4o输出，提升其性能54%，适合代码验证场景。
现有大语言模型在证明导向编程中表现不佳，主要因两类数据缺失：(1) F*等证明语言的语料库不足；(2) 缺乏大规模、项目级别的证明实现，无法有效训练模型的复杂推理能力。本文首次提出面向项目级证明编程的合成数据增强方法，涵盖生成与修复两个方面。通过生成基础证明问题以提升语言熟练度，融合多样化编码数据以激发推理能力，并在已有仓库中创建新证明与修复数据。该方法使模型能够对函数级和仓库级代码进行证明生成与修复。我们微调的140亿参数模型PoPilot，在项目级证明任务上相较表现最优的模型超越64%，且可使GPT-4o性能提升54%（通过修复其输出而非自修复）。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。