データの不足条件下で、GPT-4oよりも64%優れた証明指向プログラマを構築する

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

February 17, 2025

著者: Dylan Zhang, Justin Wang, Tianran Sun

cs.AI

要旨

既存の言語モデルは、データの希少性により証明指向プログラミングに苦労しており、これは2つの主要な方法で現れています：（1）F*などの証明指向プログラミング言語用の十分なコーパスの不足、および（2）証明指向プログラミングを行う際の複雑な推論プロセスをモデルに教えることができる大規模なプロジェクトレベルの証明指向実装の不在。私たちは、プロジェクトレベルの証明指向プログラミングのための合成データ拡張に関する初めての研究を提案します。当該手法は、その言語における熟練度向上のために基本的な証明指向プログラミング問題を合成し、推論能力の引き出しのために多様なコーディングデータを組み込み、既存のリポジトリ内で新しい証明と修復データを作成することで、データの希少性に対処します。このアプローチにより、言語モデルは関数およびリポジトリレベルのコードの証明を合成および修復することが可能となります。私たちは、ファインチューニングされた14BパラメータモデルであるPoPilotが、プロジェクトレベルの証明指向プログラミングにおいてGPT-4oを上回るモデルの性能を64％の相対マージンで示し、GPT-4oの出力を修復することでGPT-4oの性能を54％向上させることができることを示します。

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.