Het creëren van een op bewijs gerichte programmeur die 64% beter presteert dan GPT-4o bij gegevensschaarste

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

Samenvatting

Bestaande taalmodellen hebben moeite met bewijsgericht programmeren vanwege een gebrek aan gegevens, wat zich op twee belangrijke manieren manifesteert: (1) een gebrek aan voldoende corpora voor bewijsgerichte programmeertalen zoals F*, en (2) het ontbreken van grootschalige, op projectniveau bewijsgerichte implementaties die het model kunnen leren het complexe redeneerproces uit te voeren bij bewijsgericht programmeren. We presenteren de eerste aanpak voor synthetische gegevensvermeerdering voor projectniveau bewijsgericht programmeren voor zowel generatie als reparatie. Onze methode pakt het gebrek aan gegevens aan door basisbewijsgerichte programmeerproblemen te synthetiseren voor bekwaamheid in die taal; het opnemen van diverse codeergegevens voor het oproepen van redeneervermogen en het creëren van nieuwe bewijzen en reparatiegegevens binnen bestaande repositories. Deze aanpak stelt taalmodellen in staat zowel bewijzen te synthetiseren als te repareren voor code op functie- en repositoryniveau. We tonen aan dat ons fijn afgestelde model met 14B parameters, PoPilot, de prestaties van de modellen die GPT-4o overtreffen in projectniveau bewijsgericht programmeren met 64% relatieve marge kan overtreffen, en de prestaties van GPT-4o met 54% kan verbeteren door de uitvoer ervan te repareren ten opzichte van de zelfreparatie van 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.