トレース可能なリファインメントによる、意図に整合した形式仕様の合成

要旨: 大規模言語モデルは自然言語からコードを生成するためにますます使われていますが、その正しさを保証することは依然として難しい課題です。形式的検証は、プログラムが形式仕様を満たすことを証明することで、そのような保証を筋の通った形で得る方法を提供します。しかし、仕様は現実のコードベースではしばしば欠落しており、高品質な仕様を書くことは費用がかかり、専門知識も必要です。本稿では、VeriSpecGen という、要件レベルの帰属と局所的な修復によって Lean 上で意図に整合した仕様を合成する、追跡可能な洗練（refinement）フレームワークを提案します。VeriSpecGen は自然言語を原子的な要件に分解し、生成された仕様を検証するための、明示的な追跡可能性マップ付きの要件ターゲットのテストを生成します。検証が失敗した場合、追跡可能性マップによって失敗が特定の要件に帰属され、節（クローズ）レベルでの的を絞った修復が可能になります。VeriSpecGen は、Claude Opus 4.5 を用いて VERINA SpecGen タスクで 86.6% を達成し、さまざまなモデルファミリやスケールにおいてベースラインを最大 31.8 ポイント改善します。推論時の向上にとどまらず、VeriSpecGen の洗練軌跡から 343K の学習例を生成し、これらの軌跡で学習すると、相対的に 62-106% もの仕様合成の改善が得られること、さらに一般的な推論能力にも利得が移転することを示します。