Construindo um Programador Orientado a Provas que é 64% Melhor que o GPT-4o em Cenários de Escassez de Dados

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

February 17, 2025

Autores: Dylan Zhang, Justin Wang, Tianran Sun

cs.AI

Resumo

Os modelos de linguagem (LMs) existentes enfrentam dificuldades com programação orientada a provas devido à escassez de dados, que se manifesta de duas maneiras principais: (1) a falta de corpora suficientes para linguagens de programação orientadas a provas, como F*, e (2) a ausência de implementações em grande escala e em nível de projeto que possam ensinar ao modelo o processo de raciocínio intrincado ao realizar programação orientada a provas. Apresentamos o primeiro método de aumento de dados sintéticos para programação orientada a provas em nível de projeto, tanto para geração quanto para reparo. Nosso método aborda a escassez de dados sintetizando problemas básicos de programação orientada a provas para proficiência na linguagem; incorporando dados de codificação diversificados para eliciar capacidade de raciocínio e criando novas provas e dados de reparo em repositórios existentes. Essa abordagem permite que os modelos de linguagem sintetizem e reparem provas para códigos em nível de função e de repositório. Mostramos que nosso modelo ajustado de 14 bilhões de parâmetros, PoPilot, pode superar o desempenho dos modelos que superam o GPT-4o em programação orientada a provas em nível de projeto por uma margem relativa de 64%, e pode melhorar o desempenho do GPT-4o em 54% ao reparar suas saídas em comparação com o autorreparo do 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.