「正しさ確認済み」のAIプログラム、合格率9割超でも中身は不完全と判明

LLM（大規模言語モデル）が生成したプログラムの「検証済み」評価において、形式検証の合格と実際の仕様適合が乖離している実態を指摘する論文がarXivで公開された。既存の評価手法では検証器の通過率が単一の指標として報告されがちだが、研究チームは「検証器の受理」「仕様との統語的結合」「仕様の意味的忠実度」という3つの独立した段階に分解して監査すべきだと提起した。

Claude Opus 4.7を用いてPythonベンチマーク「HumanEval」で再現検証を行ったところ、検証器の受理率は99.1％に達した一方、仕様に正しく結合していた割合はわずか1.9％にとどまった。さらに、完全な検証出力を強制した独自のRust環境「VCG」による検証でも、構造的に検証されたコードの11.48％（MBPP-Rust）および14.82％（VeriContest LCスライス）が隠しテストで失敗した。研究チームは、単一の検証数値だけでは真の正しさを保証できないと警鐘を鳴らしている。