VeriAct：可証性を超えて——正しく完全な形式仕様のエージェント的合成

要旨: 正式仕様は、ソフトウェアの信頼性と正しさを保証するうえで中核的な役割を果たします。しかし、高品質な正式仕様を自動的に合成することは依然として困難な課題であり、多くの場合ドメインの専門知識を要します。最近の研究では、大規模言語モデルを用いてJava Modeling Language（JML）で仕様を生成し、高い検証パス率が報告されています。しかし、検証器を通過したことは、その仕様が実際に正しくかつ完全であることを意味するのでしょうか。本研究では、まず、自動JML仕様合成における古典的手法とプロンプトベース手法を比較する包括的な評価を行います。次に、構造化された検証フィードバックを通じてプロンプトを進化させることで、プロンプト最適化が合成品質をさらに押し上げられるかを調べます。最適化は検証器のパス率を改善しますが、明確な性能の頭打ち（上限）があることを見出します。より重要には、我々はSpec-Harnessを提案します。これは、シンボリック検証によって仕様の正しさと完全性を測定する評価フレームワークであり、最適化されたものを含む、検証器に受理された仕様の大きな割合が、実際には正しくも完全でもなく、検証器には見えない形で入出力の両方を過剰に拘束したり過小に拘束したりしていることを明らかにします。この上限を超えるために、VeriActを提案します。VeriActは、LLM主導の計画、コード実行、検証、Spec-Harnessフィードバックの閉ループによって、仕様を反復的に合成し修復する、検証ガイド付きのエージェント型フレームワークです。2つのベンチマークデータセットに対する実験の結果、VeriActはプロンプトベースおよびプロンプト最適化のベースラインの両方を上回り、検証可能であるだけでなく正しく完全な仕様を生成することが示されました。