Costruire un Programmatore Orientato alle Dimostrazioni che è il 64% Migliore di GPT-4o in Condizioni di Scarsità di Dati

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

February 17, 2025

Autori: Dylan Zhang, Justin Wang, Tianran Sun

cs.AI

Abstract

I modelli linguistici esistenti (LMs) incontrano difficoltà nella programmazione orientata alle dimostrazioni a causa della scarsità di dati, che si manifesta in due modi principali: (1) la mancanza di corpora sufficienti per linguaggi di programmazione orientati alle dimostrazioni come F*, e (2) l'assenza di implementazioni su larga scala a livello di progetto che possano insegnare al modello il complesso processo di ragionamento durante la programmazione orientata alle dimostrazioni. Presentiamo il primo approccio di sintesi di dati per la programmazione orientata alle dimostrazioni a livello di progetto, sia per la generazione che per la riparazione. Il nostro metodo affronta la scarsità di dati sintetizzando problemi di base di programmazione orientata alle dimostrazioni per acquisire competenza in quel linguaggio; incorporando dati di codifica diversificati per stimolare la capacità di ragionamento e creando nuove dimostrazioni e dati di riparazione all'interno di repository esistenti. Questo approccio consente ai modelli linguistici sia di sintetizzare che di riparare dimostrazioni per codice a livello di funzione e di repository. Dimostriamo che il nostro modello fine-tuned da 14 miliardi di parametri, PoPilot, può superare le prestazioni dei modelli che superano GPT-4o nella programmazione orientata alle dimostrazioni a livello di progetto con un margine relativo del 64%, e può migliorare le prestazioni di GPT-4o del 54% riparando i suoi output rispetto all'autoriparazione di 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.