🤖 machine learning

Evaluating the Architectural Reasoning Capabilities of LLM Provers via the Obfuscated Natural Number Game

本論文は、意味的手がかりを用いずに局所的な公理のみで証明を合成する能力である「構造的推論」を評価するためのベンチマークとして「難読化自然数ゲーム」を導入し、一般的な大規模言語モデルは難読化下で性能が低下する一方、専門的な推論モデルは精度を維持することを示すことで、真の論理的推論とパターンマッチングを区別することを明らかにする。

原著者： Lixing Li

公開日 2026-05-04

📖 1 分で読めます☕ さくっと読める

CC0 1.0

原著者： Lixing Li

原論文は CC0 1.0 (http://creativecommons.org/publicdomain/zero/1.0/) のもとパブリックドメインに提供されています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

数学パズルを学生に教える場面を想像してください。通常、そのパズルには「足し算」「掛け算」「後者」といった役立つラベルが付いています。賢い学生は、必ずしもゲームのルールを理解しているわけではなく、「足し算」という単語を認識し、以前に見た記憶されたトリックを思い出すだけかもしれません。

この論文は、厳しい問いを投げかけます：これらのAIモデルは実際に数学を行っているのでしょうか、それとも単語の認識が得意なだけなのでしょうか？

これを明らかにするため、研究者たちは有名な数学ゲーム「Natural Number Game」の「目隠し」バージョンを作成しました。以下に、彼らがどのように行い、何を発見したかを簡潔に説明します。

実験：「エイリアン」ゲーム

研究者たちは、すべてのルールと数値に明確な名前（add や zero など）が付いた標準的な数学ゲームを取りました。そして、それに対して「スクランブラ」を実行しました。彼らは、すべての意味のある名前を、x9z、q22、b7a といったランダムで無意味な文字列に置き換えました。

元のゲーム: add を見て、それが足し算を意味するとわかります。
スクランブルされたゲーム（難読化 NNG）: x9z を見て、それが何を意味するのか見当もつきません。推測することはできません。x9z が何をするのかを解明するには、部品がどのように組み合わさっているかの論理を見る必要があります。

これは、著者が**「アーキテクチャ的推論」**と呼ぶものをテストするものです。それは、ドアにある役立つ看板（名前）を無視し、構造の設計図（論理）のみを使用して解決策を構築する能力です。

結果：「レイテンシ税」

研究者たちは、複数のトップクラスのAIモデルを、元のゲームとスクランブルされたゲームの両方でテストしました。彼らは主に2つのことを発見しました。

1. 「普遍的なレイテンシ税」（誰もが遅くなる）
名前がスクランブルされると、すべてのAIモデルが問題を解くのに時間がかかるようになりました。

比喩: 慣れ親しんだコーヒーショップへ車で向かっていると想像してください。看板、通り名、ランドマークを知っています。さて、誰かがすべての看板を塗りつぶし、通りをランダムな文字列に改名したと想像してください。あなたは運転の仕方は知っていますが、すべての曲がり角で立ち止まり、地図を見て、より深く考えなければなりません。結局は到着しますが、はるかに長い時間がかかります。
発見: AIモデルは、すべての問題に対してこの「メンタルマップの再構築」を行わなければなりませんでした。記憶に頼ることはできず、生きた論理を処理する必要があり、それが時間を要しました。

2. 「推論対暗記」の分裂
誰もが遅くなった一方で、モデルの精度は2つの明確なグループに分かれました。

「汎用」モデル（例：GPT-4o、Claude）: これらのモデルは、フラッシュカードの暗記が得意な学生のようなものです。名前がスクランブルされると、混乱しました。成功率は大幅に低下しました。
- 意味するところ: これらはパズルを解くために「看板」（名前）に依存していました。看板がなくなると、道を見つけることができませんでした。
「推論」モデル（例：DeepSeek-R1、GPT-5、DeepSeek-Prover-V2）: これらのモデルは、実際にゲームのルールを理解している学生のようなものです。名前がスクランブルされても、成功率は以前と全く同じままでした。
- 意味するところ: これらはラベルを必要としませんでした。論理的な構造（「アーキテクチャ」）を見て、以前と同じように解決策を導き出しました。

結論

この論文は、単語（「add」という言葉の認識など）のパターンを一致させるだけのAIと、論理構造を通じて真に推論できるAIの間には、現実的な違いがあると結論付けています。

汎用モデルは、名前が記載されたガイドブックを必要とする観光客のようなものです。ガイドブックを取り上げれば、道に迷ってしまいます。
推論モデルは、設計図を読み解ける建築家のようなものです。建物に看板がなくても、壁と梁がどのように組み合わさっているかを依然として理解できます。

この研究は、ラベルなしで思考を強要された場合、すべてのAIモデルが「遅くなる」一方で、真の「推論」モデルだけがこの「エイリアン」環境において高い精度を維持できることを証明しています。これは、将来（まだ名前やラベルが存在しない）にAIが新しい数学を発見するためには、パターンマッチングが得意なモデルだけでなく、推論に焦点を当てたモデルが必要であることを示唆しています。

「暗号化された自然数ゲームを通じた LLM 証明機の構造的推論能力の評価」に関する詳細な技術的サマリーを以下に示す。

1. 問題定義

MiniF2F や PutnamBench などの形式数学ベンチマークにおける大規模言語モデル（LLM）の成功にもかかわらず、重要な曖昧さが残されている：これらのモデルは真の論理的推論能力を有しているのか、それとも単に事前学習データに対する意味的パターンマッチングを実行しているに過ぎないのか？

ギャップ: 現在のベンチマークは、しばしば Mathlib などのライブラリ検索に依存しており、成功は高次の補題や意味的識別子（例：add、succ）の認識に依存する。これは、外部ライブラリや慣れ親しんだ意味的手がかりが存在しない「異質な」数学領域において、モデルが証明を合成する能力をテストするものではない。
必要性: 自動定理発見を実現するためには、AI は構造的推論（Architectural Reasoning）を実証しなければならない。すなわち、外部ライブラリや意味的意味に依存せず、局所的な公理、定義、構造的論理のみを用いて形式証明を合成する能力である。

2. 手法

著者らは、語彙的検索から構造的推論を分離するために設計されたゼロ知識ベンチマークである**暗号化された自然数ゲーム（O-NNG）**を導入する。

A. 暗号化アルゴリズム

中核的な革新は、Lean 4 における自然数ゲーム（NNG）から意味的手がかりを体系的に除去することにある：

ノイズレベル（ $\lambda$ ）: 範囲 $[0, 1]$ $[0, 1]$ で定義される。
- $\lambda = 0$ : 元の NNG（意味的識別子が intact）。
- $\lambda = 1.0$ : 識別子の完全なランダム化。
摂動メカニズム: 指数関数的関係 $P = \lambda^{2.5}$ $P = λ^{2.5}$ が文字レベルの摂動の確率を決定する。
- 置換: 文字を有効な Unicode/ASCII 候補と置換する。
- 挿入: 新しい文字を注入する（確率 $0.4P$ ）。
- 削除: 文字を削除する（確率 $0.3P$ ）。識別子が空にならないことを保証する。
目的: このプロセスにより、データセットは識別子（公理、定理、戦術など）がランダムな文字列となる「閉じた環境」へと変換され、モデルがペアノ公理の論理的構造にのみ依存することを強制する。

B. 実験設定

データセット: 8 つのモジュール（加法、乗法など）に整理された NNG からの 68 の形式問題。
評価対象モデル: API を通じて評価された 5 つの最先端モデル：
- 推論モデル: DeepSeek-R1, GPT-5, DeepSeek-Prover-V2。
- 汎用モデル: GPT-4o, Claude-Sonnet-4.5。
パイプライン:
1. 解析: 厳密な依存順序で NNG を抽出。
2. 暗号化: $\lambda$ に基づいて文字レベルの摂動を適用。
3. クエリ生成: 「異質な」公理、対象定理、利用可能な戦術を含むプロンプトを構築。
4. 推論: モデルは自然言語の計画（「Draft」）と Lean 4 コード（「Code」）を含む JSON を出力。
5. 検証: Lean 4 コンパイラ（v4.27.0）を用いた自動検証により、構文および論理エラーをチェック。
指標:
- 正解率（%）: 成功裏に証明された定理の比率。
- 平均時間（秒）: 推論レイテンシ。

3. 主要な貢献

構造的推論の定義: 外部ライブラリや高次の自動化戦術（linarith など）を排除し、閉じた理論内の局所的な定義と公理のみを用いて証明を合成する能力として形式化。
O-NNG ベンチマーク: 意味的識別子が除去された際の性能低下を測定することで、「意味 - 推論ギャップ」を定量化する、新規のゼロ知識評価フレームワーク。
「レイテンシ税」の定量化: 異質なドメインをナビゲートすることが、アーキテクチャに関わらずすべてのモデルに普遍的な計算コスト（推論時間の増加）を課すことを確立。

4. 結果と分析

本研究は、意味的手がかりが除去された際のモデル行動の鋭い分岐を明らかにする：

普遍的なレイテンシ税:
- 全てのモデルにおいて、 $\lambda$ が増加するにつれて推論時間が統計的に有意に増加した。
- 示唆: 意味的識別子を除去することは、モデルの基礎能力に関わらず、モデルにより集中的な内部検索または論理再構築を強制する。
頑健性（精度）における分岐:
- 推論モデル（DeepSeek-R1, GPT-5, DeepSeek-Prover-V2）: 全てのノイズレベル（ $\lambda \in [0, 1]$ $λ \in [0, 1]$ ）で安定した精度を維持した。性能の低下は統計的に有意ではなかった。
  - 結論: これらのモデルは構造的論理に依存しており、意味的アンカーなしにペアノ公理をナビゲートできる。
- 汎用モデル（GPT-4o, Claude-Sonnet-4.5）: $\lambda$ $λ$ が増加するにつれて成功率が統計的に有意に低下した。
  - 結論: これらのモデルの標準的な形式タスクにおける性能は、純粋な論理合成ではなく、意味的パターンマッチングおよび命名慣習への慣れに大きく依存している。
統計的有意性: 一元配置分散分析（One-Way ANOVA）により、汎用モデルの性能低下と全モデルのレイテンシ増加が統計的に有意（ $p < 0.05$ ）であることが確認された。

5. 意義と示唆

真の推論のベンチマーク: O-NNG は、パターンマッチングを通じて数学を「知っている」モデルと、構造的論理を通じて「推論」できるモデルを区別するための厳密な指標を提供する。
アーキテクチャの方向性: 結果は、自動定理発見（AI4Math）の将来において、意味的事前知識の欠如に対して頑健であるため、汎用モデルよりも推論に焦点を当てたアーキテクチャ（DeepSeek-R1 や GPT-5 など）が優れていることを示唆する。
「推論の不気味の谷」: データは、部分的なノイズが完全な暗号化よりも有害である可能性がある非線形関係を暗示しており、残存する意味的手がかりが混乱を招くヒューリスティックとして機能する可能性を示唆している。
将来の AI エージェント: 本知見は、不完全または隠蔽されたオントロジーを有するドメインで動作可能な「知識に基づく意味的エージェント」の開発を提唱する。これは、新たな数学的定理を発見するための前提条件である。

要約すると、本論文は、現在の LLM がパターンマッチングを通じて既知の問題を解決できる一方で、完全に未知の暗号化された論理環境における問題を解決するために必要な構造的推論を有しているのは特定の「推論」アーキテクチャのみであることを実証している。