Alessandro Sosso氏、Akhil Arora氏、Bas Spitters氏らは2026年5月22日(現地時間)、arXiv cs.AIで公開した論文「Agentic Proving for Program Verification」で、エージェンティックシステム (Agentic System) がプログラム検証において著しい能力を示したと発表した。この研究では、大規模言語モデル「Claude Code」をLean 4向けの検証可能なコード生成ベンチマークCLEVER (CLEVER Benchmark) で評価。プログラム生成と検証のエンドツーエンドパイプラインで98.1%の成功率を記録した。
この論文は、Alessandro Sosso氏、Akhil Arora氏、Bas Spitters氏らが執筆したもので、形式数学の自動定理証明で最先端とされるエージェンティックシステムが、プログラム検証にどの程度応用可能かを評価している。
評価プロセスでは、Claude CodeがCLEVERベンチマーク上のエージェンティック証明フレームワーク (Agentic Proving Framework) で利用された。その結果、Claude Codeは問題の98.8%に対してarguably valid specifications（議論の余地はあるが有効な仕様）を生成した。このうち81.3%は、CLEVERの同型性に基づいた採点基準でも受理された。
さらに、Claude Codeは正しいground-truth specifications（真の仕様）が与えられた場合、問題の87.5%で実装の証明を行った。また、自己無矛盾な前提を持つエントリーにおいては、エンドツーエンドのプログラム生成および検証パイプラインで98.1%という高い成功率を達成した。
Claude Codeは自身の試行について高品質なフィードバックを提供し、失敗の根本原因やデータセットに残るバグを特定する能力も示した。これらの発見は、既存のプログラム検証ベンチマークの難易度と現代のエージェンティックプルーバーの能力との間に乖離が生じていることを示唆している。論文は、より厳密でバグに強い評価方法の必要性、特に生成された仕様に対する同型性に基づいた採点に代わるアプローチが求められると指摘した。
広範な見地から、この研究は、コンパイラを緊密に組み込んだエージェンティックパラダイムが、基礎的なプログラム検証において最も効果的なアプローチであるという経験的証拠を提供すると結論付けている。
参考: arXiv cs.AI — 2026年5月23日 00:41 (JST)
原文ハイライト"tight compiler-in-the-loop agentic paradigms are currently the most effective approach"