11月5日にarXivで公開された論文は、大規模言語モデルが生成したコードについて、「検証済み」とは何を意味するのかを検討している。検証器がコードを受け入れるか、証明が仕様に結び付いているか、その仕様が元の要件を反映しているかという3つの観点に分けて調べた。
著者らによると、あるテストではHumanEvalで検証器の合格率は99.1%だった一方、仕様で定義された述語または関数に結び付いた証明書があったサンプルはわずか1.9%だった。そうした結び付きを確保するために設計された別のRustパイプラインでは、構造上は検証済みのMBPP-Rustサンプルの11.48%、VeriContestの一部データの14.82%が、それでも非公開テストに失敗した。
なぜ重要か
生成コードの評価に証明検査を使うチームにとって、この結果は、検証器に合格しただけでは、要件との意味のある結び付きも、非公開テストでの正しさも確認できない可能性を示している。
