Développement d'un programmeur axé sur la preuve qui est 64 % plus performant que GPT-4o en cas de rareté des données

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

February 17, 2025

Auteurs: Dylan Zhang, Justin Wang, Tianran Sun

cs.AI

Résumé

Les LMs existants rencontrent des difficultés avec la programmation orientée vers la preuve en raison de la rareté des données, qui se manifeste de deux manières clés : (1) un manque de corpus suffisants pour les langages de programmation orientés vers la preuve tels que F*, et (2) l'absence de mises en œuvre à grande échelle orientées vers la preuve au niveau du projet qui pourraient enseigner au modèle le processus de raisonnement complexe lors de la programmation orientée vers la preuve. Nous présentons la première approche sur l'augmentation de données synthétiques pour la programmation orientée vers la preuve au niveau du projet, à la fois pour la génération et la réparation. Notre méthode aborde la rareté des données en synthétisant des problèmes de programmation orientée vers la preuve de base pour la maîtrise de ce langage ; en incorporant des données de codage diverses pour l'élucidation de la capacité de raisonnement et en créant de nouvelles preuves et données de réparation au sein des référentiels existants. Cette approche permet aux modèles de langage de synthétiser et de réparer des preuves pour du code au niveau de la fonction et du référentiel. Nous montrons que notre modèle PoPilot fine-tuné avec 14 milliards de paramètres peut dépasser les performances des modèles qui surpassent GPT-4o dans la programmation orientée vers la preuve au niveau du projet de 64 % en termes de marge relative, et peut améliorer les performances de GPT-4o de 54 % en réparant ses sorties par rapport à l'auto-réparation de GPT-4o.

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.