CAPRI、Isabelleの証明修復に編集契約を導入し、ビルド可能だが権限を逸脱した6件の候補を阻止

証明支援系でビルドが通っても、AIが依頼された作業を完遂したとは限らない。モデルは、定理を弱めたり、結論を導くのに都合のよい仮定を追加したり、近傍の証明義務を削除したりしても、変更後の理論をIsabelleに正しく受理させることができる。そこでCAPRIは、モデルを信頼できないパッチ生成元として扱い、Isabelleで証明を検証するとともに、独立したチェッカーで機械可読な契約に基づいて変更権限を検証する。候補が成功と見なされるのは、`Build`と`Conforms`の両方を満たした場合に限られる。

契約では、編集可能なファイルと領域、対象となる宣言、Isabelleのバージョン、sessionを指定し、`sorry`、`oops`、`axiomatization`、`oracle`などのコマンドを禁止する。チェッカーは、証明本体以外の保護対象コンテンツに対して、バイト単位の同一性を求める厳格なframe conditionを適用し、許可されていないファイルの追加や削除も拒否する。コントローラーは、提案ごとに元のリポジトリの新しいコピーへ変更を適用し、プロンプト、モデル出力、候補ツリー、Isabelleの診断、契約判定、token数、SHA-256 manifestを保存する。記録済みの提案は、ホスト型モデルを再度呼び出すことなくリプレイできる。

研究では、4つのIsabelle開発に含まれる失敗した証明12件を対象に、5種類のワークフローを各問題につき3回ずつ反復し、合計180回実行した。最終候補144件がIsabelleを通過したが、そのうち6件は保護対象のテキストを変更しており、いずれもtheory全体を編集可能とする反復型ワークフローから生成された。返答を証明本体のみに限定するインターフェースでは、36件中29件の有効な修復を達成し、theory全体を扱う場合の36件中31件をわずかに下回ったものの、契約違反は6件からゼロに減少した。one-shotワークフローは36件中22件、後続の設定を凍結した反復型ワークフローは36件中32件だった。

この結果は、エージェント型ツールにおいて、テストや形式証明は成果物を検証できても、エージェントの変更権限そのものを定義することはできないと示している。180回の実験データ一式と探索的データは[Zenodo](https://doi.org/10.5281/zenodo.21917680)に保存されている。ただし、ベンチマークは12問に限られ、主に1つのホスト型モデルを使用しており、契約チェッカー自体も形式検証されていない。また、厳格なバイト単位のポリシーは監査しやすい一方、無害なフォーマット整理まで拒否してしまう。