IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch

インドの数学オリンピック問題を対象とした、AI と人間の協働パイプラインにより構築され、312 件の人間検証済み Lean 4 定理を含む新しいベンチマーク「IndiMathBench」を提案し、大規模言語モデルにおける自動形式化の現状と課題を明らかにした。

要約

数学の「翻訳」と「証明」を助ける新しい仲間：INDIMATHBENCH の物語

この論文は、**「人工知能（AI）が、人間の数学の問題を、コンピュータが厳密にチェックできる『証明言語』に正しく翻訳できるか？」**という問いに挑んだ研究です。

そのために作られたのが、**「INDIMATHBENCH（インディマスベンチ）」**という新しいテスト問題集です。

まるで、**「AI に数学の難問を解かせるための、新しいトレーニングジム」**を作ったようなものです。以下に、その仕組みと発見を、身近な例え話で解説します。

---

1. なぜこの研究が必要だったのか？（「完璧な翻訳」の難しさ）

数学の問題をコンピュータに理解させるには、日常言語（英語や日本語）で書かれた問題を、**「Lean（リーン）」という、非常に厳格で論理的なプログラミング言語に書き換える必要があります。これを「自動形式化（Autoformalization）」**と呼びます。

• これまでの課題：
  既存のテスト問題は数が少なく、AI が「文法（構文）」は正しくても、「意味（論理）」を間違えているケースが多かったです。
  • 例え話： AI が「リンゴは果物だ」という文を翻訳する際、「リンゴは果物です」と正しく訳せても、「リンゴは野菜です」という意味で使ってしまうような、**「文法は完璧だが、中身がズレている」**状態です。
• 人間の役割：
  正しい翻訳を作るには、数学とプログラミングの両方に精通した「専門家」が手作業でチェックする必要があります。しかし、これは**「職人が一つ一つ手作業で高級時計を組み立てる」**ようなもので、時間とコストがかかりすぎます。

2. INDIMATHBENCH とは？（「インドの数学オリンピック」から生まれた新テスト）

研究者たちは、**「インドの数学オリンピック（INMO）」**の問題 312 問を素材に選びました。

• なぜインドのオリンピック？
  既存のテスト（アメリカの数学オリンピックなど）は AI が「丸覚え」してしまっている可能性がありました。インドのものは、AI がまだ見たことのない「新鮮で、かつ非常に難しい」問題ばかりです。
• 内容：
  幾何学（図形）、代数、数論、組み合わせ論など、多様な分野を網羅しています。特に、図形の問題は AI が苦手とする分野なので、AI の真の実力を測るのに最適です。

3. 開発の秘密兵器：「AI と人間のチームワーク」

このテスト問題集を作る際、研究者たちは**「AI と人間のハイブリッドなチーム」**を作りました。

• 従来の方法（人間だけ）：
  職人が一から時計を作る。→ 非常に時間がかかる。

• 新しい方法（AI ＋ 人間）：

  1. AI が下書きを作る： AI がまず「時計の部品」を大量に作ります（ただし、少しズレていることもあります）。
  2. AI が自分でチェックする： 作った部品が「正しく動くか」をコンピュータ（コンパイラ）に試させます。エラーが出れば、AI は自分で直します（これを 6 回繰り返します）。
  3. 人間が最終チェック： 人間は、AI が作った「ほぼ完成した部品」を見て、細かい調整（意味の修正など）をするだけです。

• 効果：
  この方法を使うと、人間が一人でやる場合の**「3.5 倍も速く」**作業が進みました。AI が「下書き」をしてくれるおかげで、人間は「最終調整」に集中できるのです。

4. 実験結果：AI はどれくらいできた？（「文法は得意、意味は苦手」）

この新しいテストで、最新の AI（GPT-5 や Claude など）を試したところ、驚くべき結果が出ました。

• 文法は上手い：
  AI は「Lean 言語の書き方」を覚えており、エラーが出ずにコードが通る（コンパイル成功）率は高かったです。
  • 例え話： AI は「高級時計の部品を、正しい工具で正しく組み立てる」ことはできます。
• 意味は苦手：
  しかし、その時計が「本当に正しい時間を刻んでいるか（論理的に正しい証明になっているか）」は、50% 程度しか正しくありませんでした。
  • 例え話： 組み立てられた時計は綺麗ですが、針が逆回りに動いていたり、時間が狂っていたりします。
• 証明の成功率：
  人間が「証明」を完成させるのを AI に任せた場合、10 回挑戦してやっと 1 割（11%）程度しか成功しませんでした。特に「図形（幾何学）」の問題は、AI が全く手こずりました。

5. 結論：AI は「天才」ではなく「優秀な見習い」

この研究が示したのは、**「今の AI は、数学の『文法』はマスターしたが、『意味』を理解するにはまだ遠い」**ということです。

• 重要な発見：
  AI だけで完璧な証明を作るのはまだ無理ですが、**「AI が下書きを作り、人間がチェックする」**という協力体制なら、非常に効率的に高品質なデータを作ることができます。
• 今後の展望：
  この「INDIMATHBENCH」というテストと、開発した「人間と AI が協力するツール」を公開しました。これにより、世界中の研究者が、AI の数学的思考能力をより正確に測り、次のステップに進むための道筋がつきました。

---

まとめ：
この論文は、**「AI に数学を教えるには、人間が手取り足取り教えるのではなく、AI に『下書き』をさせて、人間が『編集者』としてチェックする」**という新しい働き方（人間と AI の共創）が、最も効果的であることを証明しました。

AI はまだ「数学の天才」にはなれませんが、**「優秀な見習い」**として、人間の能力を大きく引き伸ばしてくれる存在になりつつあります。

技術概要

INDIMATHBENCH: 数学推論問題の人間支援型自動形式化に関する技術的サマリー

本論文は、大規模言語モデル（LLM）の時代においても依然として困難である「数学定理証明の自動形式化（Autoformalization）」の課題に焦点を当て、INDIMATHBENCH という新しいベンチマークと、それを構築するための人間と AI の協調パイプラインを提案しています。

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

1. 背景と問題定義

自動形式化とは、自然言語で記述された数学的な命題や証明を、機械検証可能な形式論理（ここでは Lean 4）に変換するタスクです。しかし、以下の課題が存在します。

• 高品質なデータの不足: 自動形式化を学習させるための「自然言語問題」と「形式化された定理」のペアデータが極めて不足しています。
• 専門家の負荷: 既存のベンチマーク（MINIF2F や PutnamBench など）は規模が小さく、専門家が手作業で形式化・検証する必要があり、スケーラビリティに欠けます。
• データ汚染: 既存の主要ベンチマークの多くが LLM の事前学習コーパスに含まれており、真の推論能力の評価が困難になっています。
• 構文と意味の乖離: LLM は形式構文（Syntax）は生成できますが、数学的な意図（Semantics）を正しく反映した形式化を行う能力は依然として低いです。特に、幾何学や組合せ論の分野での形式化は未熟です。

2. 提案手法：INDIMATHBENCH と構築パイプライン

データセットの概要

INDIMATHBENCH は、インドの数学オリンピック（RMO および INMO）から選抜された312 問の問題で構成されるベンチマークです。

• 構成: 各問題は、自然言語の問題文、証明（または解）、そして人間によって検証された Lean 4 の定理形式化のペアです。
• 分野: 幾何学（98 問）、代数学（92 問）、数論（77 問）、集合論・組合せ論（45 問）を網羅しており、特に幾何学と組合せ論の多様性に富んでいます。
• 特徴: 微積分を含まず、高校数学の範囲に限定されているため、基礎的な数学的推論の深さを評価するのに適しています。

自動形式化パイプライン（人間-AI 協調）

高品質なデータセットを効率的に構築するため、以下の 3 段階のプロセスを提案しています（アルゴリズム 1 参照）。

1. カテゴリベースの検索（Category-based Retrieval）:
   • 各問題を 4 つのカテゴリに分類し、該当する分野の Mathlib（Lean の標準ライブラリ）のドキュメントやコード例を自動的に抽出・収集します。
   • これをプロンプトに含めることで、LLM が存在しない関数を生成する（ハルシネーション）のを防ぎ、適切な構文とインポートを促します。
2. 反復的コンパイラフィードバック（Iterative Refinement）:
   • LLM が生成した形式化コードを Lean コンパイラで検証します。
   • エラーが発生した場合、そのエラーメッセージをフィードバックとして LLM に返し、最大 6 回まで修正を繰り返させます。これにより、構文的に正しいコードの生成率が大幅に向上します。
3. マルチモデルアンサンブルと比較分析:
   • 12 種類の最先端 LLM（GPT-5, Claude Opus 4, Gemini 2.5 Pro など）にそれぞれ形式化を生成させます。
   • 生成された候補を別の LLM が要約・比較し、どのモデルがどの部分を正しく扱えたかを分析します。

人間-AI 協調ダッシュボード

• 生成された複数の候補、コンパイル結果、エラー履歴、および LLM による要約を一元管理する VS Code 拡張機能（ダッシュボード）を開発しました。
• 人間のアノテーターは、このダッシュボードを用いて、AI が生成した「ほぼ正しい」候補から微調整を行うことで、ゼロから形式化を行うよりもはるかに効率的に作業できます。

3. 主要な貢献

1. INDIMATHBENCH の公開: 人間が検証した 312 問の Lean 4 形式化を含む、インドの数学オリンピックに特化した新しいベンチマーク。
2. スケーラブルな形式化パイプライン: カテゴリ検索、コンパイラフィードバックループ、マルチモデルアンサンブルを組み合わせた、効率的なデータ構築手法の確立。
3. 人間-AI 協調ツールの提供: 形式化作業を支援する VS Code 拡張機能のオープンソース化。
4. 包括的な評価: 最先端の汎用 LLM および微調整済みモデルに対する、自動形式化と定理証明能力の体系的評価。

4. 実験結果と評価

自動形式化の評価（Autoformalization）

• 評価指標: 意味的等価性を測る「双方向等価性（BEq）」と、構文的類似性を測る「一般化ツリー編集距離（GTED）」を使用。
• 結果:
  • Claude Opus 4 が最も高い性能を示しましたが、BEq 合格（人間による正解と論理的に等価）は 312 問中 54 問（約 17%）にとどまりました。
  • 構文と意味のギャップ: コンパイル成功（構文正解）率は 77.9% でしたが、意味的に正しい（BEq 合格）のは 21.5% でした。これは、LLM が構文は正しくても数学的な意味を誤解しているケースが多いことを示しています。
  • 幾何学の難易度: 上位モデルでも幾何学問題の解決は極めて困難でした（108 問の BEq 合格中、幾何学はわずか 12 問）。

定理証明の評価（Automated Theorem Proving）

• 設定: 形式化された定理に対して、証明（sorry の部分）を生成させるタスク。
• 結果:
  • シングルターン: どのモデルも 312 問中 1 問程度しか解けませんでした（既存の Mathlib の定理をそのまま使える簡単な問題のみ）。
  • 10 ターン（反復改善）: 反復的なフィードバックを繰り返すことで、GPT-5 が 36/312（約 11%）の成功率を達成しました。
  • 比較: この成功率は、同様に難易度の高い PutnamBench での結果と同等であり、INDIMATHBENCH が数学推論の限界を測る厳しいテストベッドであることを示しています。

効率性研究

• 人間のアノテーターによる作業時間を比較したところ、「完全な手作業」に比べ、「マルチモデル生成＋要約ダッシュボード」を使用すると、問題あたりの所要時間が4 分（手作業の約 1/4）に短縮されました。

5. 意義と結論

INDIMATHBENCH とその構築手法は、以下の点で重要な意義を持ちます。

1. 評価基準の刷新: 既存のベンチマークが汚染されている状況に対し、未学習のデータセットを提供し、LLM の真の推論能力を評価可能にしました。
2. 人間-AI 協調の妥当性: 完全な自動化ではなく、AI が候補を生成し、人間が検証・修正する「ハイブリッド」アプローチが、高品質な形式化データセットをスケーラブルに作成する現実的な解決策であることを実証しました。
3. 現在の限界の可視化: 最先端の LLM であっても、数学的な意味の正確な形式化や、複雑な幾何学問題の証明には依然として大きなギャップがあることを明らかにしました。特に、構文の正しさと意味の正しさの乖離は、今後の研究において重要な課題です。

本論文は、数学的推論における AI の能力限界を明確にしつつ、人間と AI が協力して高度な形式数学を進めるための具体的な枠組みとリソースを提供しています。