Создание программиста, ориентированного на доказательства, который на 64% лучше, чем GPT-4o при ограниченности данных

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

February 17, 2025

Авторы: Dylan Zhang, Justin Wang, Tianran Sun

cs.AI

Аннотация

Существующие языковые модели испытывают трудности с программированием, ориентированным на доказательства, из-за недостатка данных, что проявляется двумя основными способами: (1) отсутствием достаточных корпусов для языков программирования, ориентированных на доказательства, таких как F*, и (2) отсутствием масштабных реализаций программ, ориентированных на доказательства на уровне проекта, способных обучить модель сложному процессу рассуждения при выполнении программирования, ориентированного на доказательства. Мы представляем первый метод синтетического увеличения данных для программирования на уровне проекта, ориентированного на доказательства, как для генерации, так и для исправления. Наш метод решает проблему недостатка данных путем синтеза базовых задач программирования, ориентированных на доказательства, для владения этим языком; включения разнообразных данных кодирования для вызова способности к рассуждению и создания новых доказательств и данных по исправлению в существующих репозиториях. Этот подход позволяет языковым моделям как синтезировать, так и исправлять доказательства для кода на уровне функций и репозиториев. Мы показываем, что наша донастроенная модель с 14 миллиардами параметров, PoPilot, может превзойти производительность моделей, превосходящих GPT-4o в программировании на уровне проекта, ориентированного на доказательства, на 64% относительной маржой, и может улучшить производительность GPT-4o на 54% путем исправления ее выводов по сравнению с самостоятельным исправлением 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.