Construyendo un Programador Orientado a la Prueba que es un 64% Mejor que GPT-4o Bajo Escasez de Datos

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

Resumen

Los LMs existentes enfrentan dificultades con la programación orientada a la prueba debido a la escasez de datos, que se manifiesta de dos formas clave: (1) una falta de corpus suficientes para lenguajes de programación orientados a la prueba como F*, y (2) la ausencia de implementaciones orientadas a la prueba a nivel de proyecto a gran escala que puedan enseñar al modelo el intrincado proceso de razonamiento al realizar programación orientada a la prueba. Presentamos el primero en aumento de datos sintéticos para la programación orientada a la prueba a nivel de proyecto tanto para generación como para reparación. Nuestro método aborda la escasez de datos mediante la síntesis de problemas básicos de programación orientada a la prueba para la competencia en ese lenguaje; incorporando datos de codificación diversos para la elicitation de capacidad de razonamiento y creando nuevos datos de pruebas y reparación dentro de repositorios existentes. Este enfoque permite a los modelos de lenguaje tanto sintetizar como reparar pruebas para código a nivel de función y de repositorio. Mostramos que nuestro modelo PoPilot, afinado con 14B parámetros, puede superar el rendimiento de los modelos que superan a GPT-4o en programación orientada a la prueba a nivel de proyecto en un margen relativo del 64%, y puede mejorar el rendimiento de GPT-4o en un 54% reparando sus salidas sobre la auto-reparación 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.