Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers

LLM の証明戦略を抽出して Rocq の定理に形式化し、CoqHammer の証明成功率を 13.41% 向上させる「Strat2Rocq」という手法を提案し、その有効性を示した。

要約

🎭 物語の舞台：2 人の探偵と 1 つの事件

この研究には、2 人の「探偵（証明ツール）」が登場します。

1. AI 探偵（LLM）:
   • 特徴: 非常に頭が良く、直感力に長けています。「あ、このパターンはこうなるはずだ！」と瞬時に答えを導き出せます。
   • 弱点: 計算リソースを大量に消費し、高価です。また、機密情報の入ったコードを外部の AI に見せるのはセキュリティ上、危険です。
2. 機械式探偵（CoqHammer/記号的証明器）:
   • 特徴: 非常に正確で、安価です。自分のパソコンで動かせ、機密情報も漏れません。
   • 弱点: 直感がないので、一つ一つのステップを地道に積み重ねないと答えにたどり着けません。複雑な問題だと、すぐに「手がかりが見つからない」として諦めてしまいます。

これまでの課題:
AI 探偵は優秀ですが、高くて危険なので、常に彼に頼ることはできません。一方、機械式探偵は安全ですが、AI ほどの「直感」がないため、難しい事件（証明）を解決できないことが多いのです。

---

💡 この論文のアイデア：「AI のコツをノートに書き写す」

著者たちは、**「AI 探偵の『直感的なコツ』を、機械式探偵が理解できる『マニュアル（ノート）』に書き写して、機械式探偵に持たせてあげればどうだろう？」**と考えました。

これを**「Strat2Rocq（ストラット・トゥ・ロク）」**というシステム名で実現しました。

🔄 2 つのステップ

ステップ 1：オフライン学習（コツの抽出）

• 事前に、AI 探偵にたくさんの「事件（定理）」を解かせて、その思考プロセスを見ます。
• AI が「あ、ここはこうすればいいんだ！」と瞬時に判断した部分を見つけ出し、それを**「新しい法則（補題）」**として、機械式探偵が読める形式（Rocq という言語）でノートに書き留めます。
• 例え話: AI が「このパズルは、まず角を揃えれば 90% 解決する」と気づいたとき、それを「角を揃えるルール」としてマニュアルに記録します。

ステップ 2：オンライン実戦（証明の実行）

• 新しい事件（証明）が発生したとき、機械式探偵は**「AI からのマニュアル（新しい法則）」**を参照しながら探偵をします。
• 以前は「地道に計算しないと解けない」問題も、マニュアルに「実はこうすれば一発だよ」と書いてあれば、機械式探偵でも瞬時に解決できるようになります。
• 重要: この実戦段階では、AI は登場しません。すべて機械式探偵が一人で完結するため、安くて安全です。

---

📊 結果：劇的な改善！

この実験を行ったところ、驚くべき結果が出ました。

• 機械式探偵の活躍:
  • 従来の機械式探偵（CoqHammer）が解決できた問題が、13.4% も増えました。
  • 具体的には、AI の「直感」をマニュアル化したおかげで、複雑な計算や「帰納法（数学的帰納法）」を使わなくても済むようになり、解決が楽になったのです。
• AI 探偵への恩恵:
  • 意外なことに、このマニュアルは AI 探偵自身にも役立ちました。AI がマニュアルを参照して解くと、4% ほど成功率が上がり、使うトークン（コスト）も減りました。
  • 意味: AI と機械式探偵は、お互いの「コツ」を共有することで、より賢くなれるということです。

---

🌟 なぜこれがすごいのか？（まとめ）

1. 安全で安い: 機密コードを外部の AI に送る必要がありません。自分のパソコンで、安価に高性能な証明ができます。
2. AI の知恵を継承: AI が「なぜそうなるのか」を説明できなくても、その「答えの導き方（戦略）」を形に残して、誰でも使えるようにしました。
3. 未来へのヒント: この研究は、「AI がどうやって考えているのか」を理解するための新しい窓を開きました。AI の黒箱（ブラックボックス）の中身を、人間が理解できる「論理のルール」として取り出せることを示したのです。

一言で言うと：
「天才的な AI 探偵の『ひらめき』を、誰でも使える『マニュアル』に変換して、堅実な機械式探偵をスーパー探偵に昇格させた！」というお話です。

技術概要

論文「Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers」の技術的サマリー

本論文は、大規模言語モデル（LLM）が持つ証明戦略を抽出し、それを形式証明支援系（記号証明器）の能力向上に活用する新しいアプローチ「Strat2Rocq」を提案しています。LLM の推論能力を記号証明器に埋め込むことで、コスト効率とセキュリティを維持しつつ、証明の成功率を大幅に向上させることを目指しています。

以下に、問題定義、手法、主要な貢献、結果、そして意義について詳細にまとめます。

---

1. 背景と問題定義

• ソフトウェア検証の重要性: 対話型定理証明（ITP）は、コンパイラや OS カーネルなどの安全クリティカルなシステムの検証に不可欠ですが、証明の記述には莫大な人的コストがかかります。
• LLM の台頭と限界: 近年、LLM は定理証明において高い能力を示し、従来の記号証明器を補完する「証明エージェント」として注目されています。しかし、LLM ベースのアプローチには以下の課題があります。
  • コスト: 大規模な計算リソースが必要。
  • セキュリティ: 機密コードの外部 LLM サービスへの送信はリスクとなる。
  • 依存性: 証明プロセス全体で LLM に依存するため、オフライン環境やリソース制約のある環境では利用が困難。
• 研究課題: 「LLM の内部証明戦略を抽出し、それを記号証明器の能力を強化するために活用することは可能か？」という問いに対し、LLM の知識を記号証明器が直接利用可能な形式（補題）に変換する手法を提案します。

2. 提案手法：Strat2Rocq

Strat2Rocq は、LLM の証明戦略を「オフライン」で抽出し、「オンライン」で記号証明器に適用する 2 段階のフレームワークです。

ステージ 1：オフライン補題マイニング（Lemma Mining）

トレーニングセット（既存の定理群）に対して以下の処理を行います。

1. 自然言語証明の生成:
   • 各定理に対し、LLM に「ステップバイステップの自然言語（NL）による証明」を生成させます。
   • 形式証明ではなく NL 証明を生成させるのは、LLM の内部推論プロセスがより明確に反映されるためです。
   • 入力には、関連する型定義、関数定義、および定理が記述されているファイルの文脈を含めます。
2. 戦略の一般化と形式化（Autoformalization）:
   • 生成された NL 証明から、特定の定理に依存しない「一般的な証明戦略（補題）」を抽出・一般化します。
   • LLM に、これらの戦略を Rocq（Coq の後継）の形式言語で補題（Lemma）として定義させ、証明を生成させます。
   • 自己修復エージェント: 生成された補題や証明が誤っている場合、エラーメッセージに基づいて LLM を反復的に呼び出し、修正を試みるエージェント機構を採用しています。

ステージ 2：オンライン定理証明（Online Theorem Proving）

• 抽出された補題群を、証明対象の新しい定理の文脈（Context）に挿入します。
• 対象となる記号証明器（本論文では Rocq における最先端のCoqHammer）は、これらの追加された補題を参照して証明探索を行います。
• 特徴: オンライン証明段階では LLM を呼び出さず、純粋な記号証明器のみで動作するため、高速かつ安全です。

3. 主要な貢献

1. 新しい研究課題の提案: LLM の証明戦略をオフラインで抽出し、記号証明器のパフォーマンスを向上させるという新たなアプローチを提示しました。
2. 再利用可能な補題の抽出手法: LLM が生成する自然言語証明を分析し、それを再利用可能な形式補題に変換する手法を設計しました。これにより、LLM の「暗黙の知識」を記号証明器が直接利用可能な形に統合しています。
3. 実装と実証: 手法を「Strat2Rocq」として実装し、オープンソースの Rocq プロジェクト（CompCert, Coq-Art など）を用いた大規模な評価により、その有効性を検証しました。

4. 評価結果

実験は、ソフトウェア検証に焦点を当てたオープンソースの Rocq プロジェクト（CompCert, Ext-Lib, Coq-Art, Vfa）から抽出した 2,394 個の定理を用いて行われました。

• 記号証明器（CoqHammer）の性能向上:
  • Strat2Rocq によって抽出された補題を CoqHammer に追加した結果、証明成功率が平均 13.41% 向上しました。
  • 特に CompCert（認証済み C コンパイラ）では 17.75% の向上が見られました。
  • メカニズム: 抽出された補題により、記号証明器は「帰納法（Induction）」を回避して証明を簡略化できたり、適切な補題の選択（Lemma Selection）が改善されたりすることが確認されました。
• LLM エージェントへの波及効果:
  • 抽出された補題は、LLM 証明エージェント（RAG モジュール付き）の性能も4.00% 向上させました。
  • また、LLM の呼び出し回数が減るため、トークン消費量が減少し、コスト削減にも寄与しました。
• モデル非依存性:
  • Claude 3.7 Sonnet と OpenAI o3-mini の両方の LLM をバックエンドとして使用した実験により、手法が特定のモデルに依存せず、異なる LLM からも戦略を抽出できることが確認されました。
• 自然言語証明の重要性:
  • 自然言語証明を介さずに直接形式補題を生成させるアブレーション実験では、抽出される補題数が 63.56% 減少し、性能も低下しました。これは、LLM の推論プロセスを NL で可視化・一般化することが重要であることを示しています。

5. 意義と将来展望

• 実用的価値: 本手法は、LLM の高い推論能力を、低コストかつ高セキュリティな「純粋な記号証明器」に定着させることを可能にします。これにより、機密性の高い環境やリソース制約のある環境でも、高度な自動化証明が実現可能になります。
• LLM の理解: 本アプローチは、LLM がどのように形式的証明を行っているかを理解するための新しい窓を提供します。抽出された補題は LLM の内部戦略を記号モデルとして近似したものであり、将来的には「LLM の振る舞いを記号系で完全に再現・説明する」ための基盤となる可能性があります。
• 拡張性: 現在は Rocq/CoqHammer 上で実装されていますが、他の証明支援系（Lean, Isabelle など）への移植も可能であり、将来的な拡張が期待されます。

結論として、Strat2Rocq は、LLM の「ブラックボックス」化された推論能力を、記号証明器が理解・利用可能な「ホワイトボックス」の知識（補題）に変換する画期的な手法であり、ソフトウェア検証の自動化を次の段階へと押し上げる可能性を秘めています。