自然言語から検証済みコードへ：Dafnyベースの形式検証を用いたAI支援の問題からコード生成に向けて

arXiv cs.AI / 2026/4/27

💬 オピニオンDeveloper Stack & InfrastructureIdeas & Deep AnalysisModels & Research

共有:

要点

本論文は、LLMがソフトウェア工学を自動化する可能性がある一方で、生成コードが誤りやハルシネーションによって正しさ要件を満たせないことが多い点を指摘しています。
NL2VC-60データセット（60の複雑なアルゴリズム問題）を提示し、自然言語の問題文からDafnyに基づく正確な形式仕様と実装ロジックへの変換方法を評価します。
7種類のオープンウェイトLLMに対して、文脈なし・構造的アンカーを与えるシグネチャ付き・Dafny検証器のフィードバックを使う反復的自己修復という段階的プロンプトを比較し、その結果、文脈なしは極めて不調であることが分かります。
シグネチャによる誘導と、Dafny駆動の自己修復を組み合わせることで大幅に改善し、Gemma 4-31Bでは検証成功率90.91%を達成し、GPT-OSS 120Bもシグネチャ誘導フィードバックにより成功率0%から81.82%へ大きく伸びました。
ゼロでも形式的に“通るだけ”の無意味な検証（自明な仕様で合格するケース）を防ぐため、uDebugによる機能検証を用いて、検証器の受理だけに留まらない高い保証を目指します。

Abstract

大規模言語モデル（LLM）は自動ソフトウェア工学における有望さを示しているものの、その正しさの保証は、誤ったコードや幻覚（ハルシネーション）によってしばしば損なわれます。モデルの誠実さを強制するために、形式的検証では、LLMに対して、実装ロジックを形式仕様と並行して合成させ、その後、数学的検証器によって正しいことが証明される必要があります。しかし、自然言語の非形式的記述から、正確な形式仕様へ移行することは依然として困難な作業です。本研究では、NaturalLanguage2VerifiedCode（NL2VC）-60データセットを提供することでこの課題に取り組みます。これは60の複雑なアルゴリズム問題からなるコレクションです。階層化されたプロンプト戦略を用いて、7つのオープンウェイトLLMに対し、ランダムに選んだ11の問題セットを評価します。具体的には、文脈なしプロンプト、構造上のアンカーを与えるシグネチャ（署名）プロンプト、そしてDafny検証器からの反復的フィードバックを利用する自己修復プロンプトです。検証が空疎になる問題、つまりモデルが自明な仕様によって検証器を満たしてしまう状況に対処するため、機能検証を確実にするべく uDebug プラットフォームを統合します。結果として、文脈なしプロンプトはほぼ普遍的な失敗を招く一方で、構造シグネチャと反復的な自己修復が、驚くべき性能の立て直しを可能にすることが示されました。具体的には、Gemma 4-31B は検証成功率 90.91\% を達成し、GPT-OSS 120B は、シグネチャに導かれたフィードバックによって成功率がゼロから81.82\%へと上昇しました。これらの知見は、複雑な注釈を合成し、高い保証を持つソフトウェア開発を促進するための効果的な助手として機能するオープンウェイトLLMに対して、形式的検証がいまや実現可能になっていることを示しています。