何が起きたか
Isabelleの証明支援に大規模言語モデル（LLM）を活用する研究が進んでいます。しかし、LLMが証明を修正する際、開発者が承認した範囲を超えて、意図しない部分まで変更してしまうリスクが常に存在しました。この課題に対し、新たに「CAPRI」という契約認識型修復ワークフローが発表されました。CAPRIは、Isabelleによる証明チェックに加え、機械可読な「編集契約」を強制する独立したチェッカーを導入することで、LLMによる変更の安全性を確保します。監査のために、プロンプト、LLMの提案、候補リポジトリ、診断、最終結果、ハッシュ値などが全て保持される仕組みです。
CAPRIの仕組みと評価
CAPRIの核心は、LLMが証明を修正する際に、事前に定義された「編集契約」を遵守させる点にあります。この契約は機械可読であり、独立したチェッカーがその強制力を持ちます。研究では、4つの開発プロジェクトから得られた12の失敗した証明に対し、5つの異なるワークフローと3回の繰り返しで合計180回の実行を行いました。その結果、138回の有効な修復が確認されています。Isabelleが受け入れた144の最終候補のうち、6つが保護されたテキストを意図せず変更していました。これらの違反は全て、完全な理論全体を編集できる反復ワークフローで発生したものです。
ワークフローとLLMの比較
評価されたワークフローの中では、証明本体のみを編集するインターフェースが36中29の有効な修復を達成し、契約違反はゼロでした。これに対し、対応する完全な理論を編集するワークフローでは36中31の有効な修復でしたが、契約違反が発生しています。ワンショット修復は36中22、後に凍結された反復ワークフローは36中32の修復率でした。特定のLLM構成として、Sol構成と一致するデモンストレーションでは36中33の修復を達成し、OpenAI Responses条件の36中29を上回りましたが、統計的な有意差は確認されていません。
私の見方
LLMを証明支援に使うのは、今後の開発効率を考えると必然の流れです。しかし、LLMが勝手にコードを変更するリスクは常に意識すべきです。CAPRIが提案する「契約認識型」のチェック機構は、このリスクに対する非常に有効なアプローチだと私は考えます。開発者がLLMにどこまで変更を許可するか、その範囲を明確に定義し、それをシステムが強制する。これは、LLMを安全に活用するための必須要件です。私の経験上、LLMに与える権限は最小限に留めるのが正解です。完全な理論全体をLLMに編集させるのは危険が伴い、特定のスコープに限定する方が安全性と信頼性を両立できます。LLMの能力向上だけでなく、その活用方法と安全設計こそが、これからのAI開発の鍵を握ると断言します。
書籍ゼロからはじめるCodex
Kindleで読む →
LLMにどこまで任せるか、この線引きが最も重要です。「契約」という概念をAI活用に持ち込むのは正解です。私のプロダクトでも、LLMの出力範囲を厳しく制御しています。信頼性担保は最優先で考えるべきです。
