アダシュ・アグラワル (Adarsh Agrawal) 氏（独立研究者）は2026年10月15日(現地時間)、プログラムの正確性フィードバックが、仕様の完全性監査（specification-completeness auditing）が発見すべき証拠を抑制するという研究結果をarXivで発表した。同氏は、この客観的な逆転現象を12のVerus/Rustタスクで実証し、フィードバックなしのアプローチが認定された証拠の発見率を大幅に向上させる可能性を示した。
この研究は、契約は満たすものの意図した動作に反するプログラムといった、仕様の完全性監査が発見を目的とする証拠を、正確性フィードバックが隠蔽するという問題点を指摘している。
アグラワル氏は、4つのモデルファミリーにわたる12のVerus/Rustタスクに対し、同等の呼び出し予算（call budgets）のもとで実験を行った。その結果、独立したフィードバックなしの発見（Independent no-feedback discovery）は、インテントシールド（IntentShield）の是正フィードバックループと比較して、認定された証拠（certified-witness yield）の発見率を2倍以上（59.0%対27.1%）に増加させた。このギャップの大部分は、独立した再起動ではなく、フィードバックの内容に起因するとされる。
この利点は、全てのモデルファミリーで確認され、パーサー（parser）の修復後も維持された。また、別のフェーズ分離実行（phase-separated execution）は、応答を再利用することなく、集計された収率に匹敵する結果を達成している。ほとんどの認定された証拠は、ホールドアウトされたケースでも失敗した。
これらの証拠を保存することは、より強力な仕様修復につながることも示された。Phase-Revised契約は81.3%の実装成功率を達成したのに対し、IS-Revised契約は62.5%であった。フィードバックなしの証拠源は、弱体化した契約よりも大幅に優れた性能を示している。
ただし、この効果は既存のDafnyおよびLeanの評価では再現せず、研究対象のVerus/Rustワークフローに経験的な境界を確立している。同研究は、完全性監査と正確性修復が直接的に相反する目的を持つことを強調し、修復の前に認められた失敗を保存し認定することの重要性を提言している。この論文は、NeurIPS 2026 Workshop on AI for Verifiable Codingで採択された。
参考: arXiv cs.AI — 2026年10月16日 13:00 (JST)
原文ハイライト"Correctness feedback suppresses the very evidence that specification-completeness auditing is designed to uncover"