Learning to Disprove: Formal Counterexample Generation with Large Language Models

この論文は、数学的推論における証明構築だけでなく反例発見も重視し、記号的変異戦略と多報酬エキスパート反復フレームワークを用いて、Lean 4 で検証可能な形式的反例を生成するよう大規模言語モデルを微調整する手法を提案し、新しいベンチマークでその有効性を示しています。

要約

この論文は、**「AI に『間違いを見つける力』を教える」**という画期的な研究について書かれています。

通常、AI（特に数学が得意な AI）は「正しい証明を作る」ことには長けていますが、「なぜその考え方が間違っているのか」を示す**「反例（はんれい）」**を見つけることにはあまり慣れていません。

この研究では、AI に「正解を探す」だけでなく、「間違いを暴く」ための特別なトレーニングを行いました。その仕組みを、3 つのステップに分けて、わかりやすく解説します。

---

1. 問題点：AI は「正解」ばかり探している

これまでの AI は、数学の定理（法則）を証明することに集中していました。
しかし、現実の数学や論理の世界では、「この法則は常に正しい」と思っていたものが、実は**「ある特定のケースでは間違っている」**という発見が非常に重要です。

• 例え話：
  料理のレシピ（定理）が「すべての魚は美味しい」と言っているとします。
  今の AI は「どうすれば魚を美味しく作れるか」を研究しますが、「実はこの魚は毒がある（反例）」という発見には消極的です。
  しかし、「毒がある魚」を見つけることこそが、より安全で正確なレシピ（真実）を見つけるための鍵なのです。

2. 解決策：AI に「仮説を壊す」練習をさせる

この研究では、AI を鍛えるために**「シンボリック・ミューテーション（記号的な突然変異）」**という面白い方法を使いました。

• 仕組み：

  1. まず、AI が「絶対に正しい」と証明できた定理を用意します。
  2. その定理から、「あえて重要な条件（仮説）を 1 つ消し去ります」。
  3. 条件が抜けたせいで、その定理は「もう成り立たない（間違っている）」状態になります。
  4. ここで AI に**「じゃあ、この間違いを証明する『反例』を 1 つ作ってごらん」**と問いかけます。

• 例え話：
  「『雨』が降っているとき、地面は濡れる」という正しい法則があるとします。
  AI は「雨」という条件を消して、「地面は濡れる」という状態だけを残します。
  AI は「じゃあ、雨が降っていないのに地面が濡れている例（例えば、ホースで水をかけた場合）を見つけなさい」と言われます。
  これを AI に何十万回も繰り返させることで、AI は「どんな条件が抜けると法則が崩れるか」を徹底的に学びます。

3. 評価方法：AI の答えを「自動採点」する

AI が「反例」を思いついたとしても、それが本当に正しいかどうかを人間がチェックするのは大変です。そこで、**Lean 4（リーン・フォー）**という「数学の厳密なチェック機能」を持った AI 裁判官を使いました。

• ダブル・リワード（二重の報酬）システム：
  AI が反例を出したとき、2 つのチェックを行います。

  1. メインのチェック： 「消した条件がない状態で、本当に法則が崩れるか？」
  2. サブのチェック： 「消した条件が、本当に必要だったことを証明できるか？」

  もし AI が「あ、消した条件が本当に必要だったんだ！」と理解して、その証拠も示せれば、AI は大きな「ご褒美（報酬）」を得ます。これにより、AI は難しい問題でも「諦めずに頑張る」ようになり、学習が格段に効率化されました。

---

結果：AI はどう変わった？

この新しいトレーニングを受けた AI は、従来の AI と比べて**「間違いを見つける能力」が 47%〜74% も向上**しました。

• 従来の AI： 「正解を探すのが得意」だが、「間違っているものを指摘するのは苦手」。
• 新しい AI： 「正解を探す」だけでなく、「なぜそれが間違っているのか」を論理的に説明し、証明できるまでに成長しました。

まとめ

この論文は、AI に**「批判的思考（クリティカル・シンキング）」**を教えるための新しい道を開きました。

AI が単に「正解」を並べるだけでなく、「ここが間違っているよ！」と指摘できるようになることは、数学の発見だけでなく、AI が人間と協力して複雑な問題を解決する上で、非常に重要な一歩です。まるで、優秀な学生が「先生に正解を教わる」だけでなく、「先生が間違っている可能性を検証する」まで成長したようなものです。

技術概要

論文「LEARNING TO DISPROVE: FORMAL COUNTEREXAMPLE GENERATION WITH LARGE LANGUAGE MODELS」の技術的サマリー

この論文は、数学的推論における「反証（Counterexample）の発見」という重要なタスクに焦点を当て、大規模言語モデル（LLM）をそのために微調整（Fine-tuning）する新しいフレームワークを提案しています。既存の研究が「定理の証明」に偏重しているのに対し、偽の命題を反証する能力の欠如を指摘し、それを解決するためのデータ合成戦略と多報酬学習アプローチを提案しています。

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

---

1. 問題定義と背景

背景

数学的推論には、真の命題に対する厳密な証明の構築と、偽の命題に対する反証（反例）の発見という、互いに補完的な 2 つのスキルが必要です。近年、OpenAI-o1 や DeepSeek-R1 などの推論能力を持つ LLM や、Lean 4 などの定理証明器と連携する「形式推論 LLM」の性能は向上していますが、これらのモデルは主に証明構築に特化しており、反証の発見能力は未だ十分に研究されていません。

課題

反証生成を LLM に学習させることには、以下の 2 つの重大な課題が存在します。

1. トレーニングデータの深刻な不足: 反証生成に特化したデータセットは極めて少なく、既存の CounterMath データセット（自然言語問題 1,216 件）は LLM の微調整には不十分です。
2. スパースな報酬信号: 複雑な問題において LLM が正しい反証を生成できない場合、トレーニング中の報酬が得られず（スパース化）、モデルの性能向上が停滞します。

タスク定義

本論文では**「形式反証生成（Formal Counterexample Generation）」**を定義します。これは、LLM に以下の 2 段階のタスクを要求するものです。

1. 非形式的推論: 与えられた問題に対して、具体的な反例（数値や関数など）を自然言語で提案する。
2. 形式的証明: 提案された反例を用いて、その反例が命題を否定することを示す証明を Lean 4 などの定理証明器で検証可能な形式コードとして生成する。

---

2. 提案手法

提案フレームワークは、**「記号的変異（Symbolic Mutation）によるデータ合成」と「多報酬ガイド付きトレーニング（Multi-Reward Guided Training）」**の 2 つの主要な段階で構成されています。

2.1 反証問題の合成（データ合成）

既存の証明可能な定理から、自動的に反証問題（反例が存在する命題）を生成する手法を提案します。

• シード定理の収集: Mathlib や Leanworkbook などの形式ライブラリ、および LLM によって生成された証明から、普遍量化された定理（$\forall x, P(x)$）を抽出します。
• 記号的変異（Symbolic Mutation）:
  • 元の定理 $H_1(x) \land H_2(x) \to C(x)$ から、必須の仮説（Hypothesis）$H_1$ を意図的に削除します。
  • これにより、$H_2(x) \to C(x)$ という新しい命題（変異版）が生成されます。
  • 削除された仮説が必須であれば、この変異版は偽となり、反例が存在することになります。
  • 変異版の妥当性は、Lean 4 証明器を用いて元の証明を解析し、冗長な仮説を排除した上で確認します。
• 結果: この戦略により、約 57.5 万件の多様な反証問題データセットを構築しました。

2.2 多報酬ガイド付きトレーニング（Expert Iteration）

従来の単一報酬（反証が成功したか否か）ではなく、より効率的な学習を可能にする多報酬戦略を導入します。

• マルチ報酬の設計:
  生成された反例 $x^*$ に対して、以下の 2 つの証明を生成し、それぞれに報酬を与えます。
  1. 変異版の証明: 削除された仮説なしで命題が偽であることを示す証明（$\exists x, H_2(x) \to C(x)$）。
  2. 削除された仮説の否定証明: 反例 $x^*$ が、削除された仮説 $H_1$ を満たさないことを示す証明（$\exists x, \neg H_1(x)$）。
• 報酬の利点:
  • 削除された仮説の否定証明は比較的容易に構成できるため、変異版の証明が失敗しても、この部分で報酬が得られます。
  • これにより、スパースな報酬問題を緩和し、学習の効率と安定性を向上させます。
• トレーニングフロー:
  1. LLM が反例を提案し、形式証明を生成。
  2. Lean 4 証明器で検証。
  3. 検証結果に基づき、2 つの証明の正誤を重み付けして報酬を計算。
  4. 成功したサンプルを用いて、LLM を教師あり微調整（SFT）する（Expert Iteration）。

---

3. 主要な貢献

1. 形式反証生成タスクの確立: 自然言語だけでなく、Lean 4 による形式証明を伴う反証生成タスクを定義し、そのための専用データセットとベンチマークを構築しました。
2. 記号的変異戦略: 証明可能な定理から仮説を削除することで、自動的に高品質な反証問題データを大規模に合成する手法を提案しました。これにより、データ不足の問題を解決しました。
3. 多報酬学習フレームワーク: 反証生成の難易度に応じたスパースな報酬問題を、2 つの関連する証明（変異版と仮説否定）の組み合わせによって緩和する新しいトレーニング手法を提案しました。
4. SOTA の達成: 3 つの新しいベンチマークにおいて、既存の最先端 LLM（Proprietary モデルやオープンソースの定理証明モデル）を大幅に上回る性能を達成しました。

---

4. 実験結果

評価ベンチマーク

3 つのタスクでモデルを評価しました。

1. FOR-COUNTER: 既存の反証問題集（CounterMath）を形式化して作成した 1,058 件の問題。
2. VERI-REASON: 正しい定理の推論ステップにおける誤りを特定するタスク。
3. VERI-FORMALIZE: 自動形式化された結果の誤りを特定するタスク。

性能結果

• Pass@1 性能: 3 つのベンチマークすべてにおいて、提案モデルは最強のベースライン（DeepSeek-R1 や GPT-4.1-mini など）と比較して、47% から 74% の相対的な改善を達成しました。
  • 例：FOR-COUNTER タスクで、ベースラインが 61 件正解したのに対し、提案モデルは 222 件を正解（95 件増）。
• トレーニング効率: 多報酬学習を用いることで、単一報酬学習と比較して収束が速く、最終性能も向上しました（Pass@1 で約 49% vs 43%）。
• データ合成の効果: 57.5 万件の合成データを用いることで、小規模なモデルでも高い性能を発揮できることが示されました。

---

5. 意義と結論

この研究は、AI による数学的推論において長らく見落とされてきた「反証（Disproof）」の能力を体系的に強化する画期的なアプローチです。

• 数学的探究への貢献: 反証は仮説の洗練や理論の発展に不可欠です。本フレームワークは、数学者が新しい仮説を検証するための実用的なコパイロットとして機能します。
• LLM の推論能力の向上: 反証生成は「試行錯誤（Guess-and-Check）」のパラダイムを必要とし、LLM に自己検証（Self-verification）と自己修正（Self-correction）の能力を付与します。これは、単なる論理的推論を超えた、より高度な推論能力の獲得につながります。
• 将来展望: 合成データの品質向上や、より大規模なモデルへの適用、ツール使用戦略の統合など、さらなる発展の可能性を秘めています。

総じて、本論文は「証明する」だけでなく「反証する」ことを学習させることで、LLM の数学的推論能力を新たな次元へと引き上げる重要なステップです。