Re:Form -- 大規模な形式的ソフトウェア検証における人間の事前知識の削減：LLMを用いたRLによるDafnyの予備的研究

要旨

既存の自然言語ベース（例：人間の言語）の大規模言語モデル（LLM）は、強化学習（RL）を用いて訓練されていますが、重要な課題に直面しています。その検証プロセスは、重要な訓練信号を提供するものの、信頼性も拡張性もありません。実際、主流の大規模なプロプライエタリモデルは、検証可能なプログラムを生成することがほとんどできません。有望でありながらも未開拓の代替手段として、形式的言語ベースの推論があります。LLMを厳密な形式的システムに基づかせ、生成モデルが形式的言語空間（例：Dafny）で動作するようにすることで、その推論プロセスと結果を自動的かつ数学的に証明可能な形で検証することが可能になります。この能力は、大規模で信頼性の高い形式的ソフトウェア検証を実現するために極めて重要です。LLMの推論能力とコーディング能力を誘導するために、人間が注釈を付けた連鎖的思考（chain-of-thought）やその他の人間の事前知識を利用することが一般的です。しかし、複雑なプログラミングタスクを監督するためにそのような事前知識を提供することは、許容できないほど多大な労力を要します。本研究では、形式的言語である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 -- 大規模な形式的ソフトウェア検証における人間の事前知識の削減：LLMを用いたRLによるDafnyの予備的研究

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

要旨

Support