Aufbau eines Beweisorientierten Programmierers, der unter Datenknappheit um 64% besser ist als GPT-4o

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

February 17, 2025

Autoren: Dylan Zhang, Justin Wang, Tianran Sun

cs.AI

Zusammenfassung

Bestehende Sprachmodelle haben Schwierigkeiten mit dem Beweis orientierten Programmieren aufgrund von Datenknappheit, die sich auf zwei wesentliche Arten manifestiert: (1) einem Mangel an ausreichenden Korpora für beweisorientierte Programmiersprachen wie F*, und (2) dem Fehlen von groß angelegten, projektbezogenen beweisorientierten Implementierungen, die dem Modell den komplexen Denkprozess beim Durchführen des beweisorientierten Programmierens vermitteln können. Wir stellen die erste Methode zur synthetischen Datenanreicherung für projektbezogenes beweisorientiertes Programmieren sowohl für die Generierung als auch für die Reparatur vor. Unsere Methode begegnet der Datenknappheit, indem sie grundlegende beweisorientierte Programmieraufgaben zur Beherrschung dieser Sprache synthetisiert; vielfältige Codierungsdaten zur Erhebung von Denkfähigkeiten einbezieht und neue Beweise und Reparaturdaten innerhalb bestehender Repositories erstellt. Dieser Ansatz ermöglicht es Sprachmodellen, Beweise sowohl zu synthetisieren als auch zu reparieren, sowohl für funktions- als auch für repositoryebene Codes. Wir zeigen, dass unser feinabgestimmtes 14B-Parameter-Modell, PoPilot, die Leistung der Modelle übertreffen kann, die GPT-4o im projektbezogenen beweisorientierten Programmieren um 64% relativ übertreffen, und die Leistung von GPT-4o um 54% verbessern kann, indem es seine Ausgaben über die Selbstreparatur von GPT-4o repariert.

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.