Re:Form — Уменьшение влияния человеческих предубеждений в масштабируемой формальной верификации программного обеспечения с использованием обучения с подкреплением в больших языковых моделях: Предварительное исследование на примере Dafny

Аннотация

Существующие крупные языковые модели (LLM), обученные с использованием обучения с подкреплением (RL) на основе неформальных языков (например, естественного языка), сталкиваются с серьёзной проблемой: их процессы верификации, которые предоставляют важные сигналы для обучения, не являются ни надёжными, ни масштабируемыми. Фактически, преобладающие крупные проприетарные модели едва ли способны генерировать верифицируемые программы. Многообещающей, но малоизученной альтернативой является рассуждение на основе формальных языков. Основание LLM на строгих формальных системах, где генеративные модели работают в пространствах формальных языков (например, Dafny), позволяет автоматически и математически доказуемо проверять их процессы рассуждения и результаты. Эта возможность имеет ключевое значение для достижения крупномасштабной и надёжной формальной верификации программного обеспечения. Обычной практикой является использование аннотированных человеком цепочек рассуждений и других человеческих априорных знаний для развития способностей LLM к рассуждению и написанию кода. К сожалению, предоставление таких априорных знаний для контроля сложных задач программирования становится неприемлемо трудоёмким. В данной работе мы систематически исследуем способы сокращения человеческих априорных знаний с использованием формального языка Dafny в качестве основной среды для нашего пилотного исследования. Наш подход в основном опирается на внедрение автоматического и масштабируемого конвейера курирования данных, а также тщательно продуманные методы RL, интегрированные с обратной связью от верификатора формального языка. Мы представляем DafnyComp — набор композиционных формальных программ с автоматически формализованными спецификациями для рассуждения на основе спецификаций. Наш этап контролируемого тонкого настройки (SFT) позволяет даже небольшим моделям (например, 0.5B) генерировать синтаксически корректный и верифицируемый код на Dafny, превосходя проприетарные модели. RL с регуляризацией дополнительно улучшает производительность, достигая более сильной обобщаемости на задачи вне домена и превосходя все сильные базовые модели на сложном наборе данных DafnyComp.

English

Existing informal language-based (e.g., human language) Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification processes, which provide crucial training signals, are neither reliable nor scalable. In fact, the prevalent large proprietary models could hardly generate verifiable programs. A promising yet largely uncharted alternative is formal language-based reasoning. Grounding LLMs in rigorous formal systems where generative models operate in formal language spaces (e.g., Dafny) enables the automatic and mathematically provable verification of their reasoning processes and outcomes. This capability is pivotal for achieving large-scale, reliable formal software verification. It is a common practice to employ human-annotated chain-of-thought and other human priors to induce the reasoning and coding capabilities of LLMs. Unfortunately, it becomes unacceptably all-consuming to provide such priors for supervising complex programming tasks. In this work, we systematically explore ways to reduce human priors with the formal language, Dafny, as the main environment for our pilot study. Our pipeline mainly relies on introducing an automatic and scalable data curation pipeline, and careful RL designs integrated with feedback from the formal language verifier. We introduce DafnyComp, a benchmark of compositional formal programs with auto-formalized specifications for specification reasoning. Our supervised fine-tuning (SFT) stage enables even small models (e.g., 0.5B) to generate syntactically valid and verifiable Dafny code, surpassing proprietary models. RL with regularization further improves performance, achieving stronger generalization to out-of-domain tasks and outperforming all strong baselines on the challenging DafnyComp benchmark.

Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny

Аннотация

Support