概要: 大規模言語モデルは、MiniF2Fのような形式的数学ベンチマークで注目すべき成功を収めていますが、これらの結果が真に論理的推論によるものなのか、それとも事前学習データに対する意味的パターンの照合によるものなのかは、依然として不明です。本論文では、建築的推論（Architectural Reasoning）：異なる数学領域において、局所的な公理と定義のみを用いて形式的証明を合成する能力を、将来の自動定理発見AIに不可欠な能力であると特定します。私たちは、建築的推論を評価するためのベンチマークであるObfuscated Natural Number Gameを用います。Lean 4におけるNatural Number Gameの識別子を改名することで、ゼロ知識・閉鎖環境を作成しました。最先端のモデルを評価したところ、難読化によって推論時間が増える普遍的なレイテンシ・ペナルティが見られました。また、頑健性の面での分岐も明らかになりました。すなわち、汎用モデル（Claude-Sonnet-4.5、GPT-4o）は性能低下に苦しむ一方で、推論モデル（DeepSeek-R1、GPT-5、DeepSeek-Prover-V2）は意味的手掛かりが欠如しているにもかかわらず、同一の精度を維持します。これらの知見は、数学的推論の真の能力を評価するための定量的な指標を提供します。
Lean 4における難読化された自然数ゲームを用いたLLMによる定理証明の「建築的推論」能力の評価
arXiv cs.LG / 2026/5/4
📰 ニュースSignals & Early TrendsIdeas & Deep AnalysisModels & Research
要点
- 本論文は、形式数学ベンチマークでの成績が、真の論理的推論というより前学習データに対する意味的なパターン照合に由来する可能性があると指摘し、自動定理発見AIに必要な能力として「Architectural Reasoning（建築的推論）」を定義しています。
- その検証のために、局所的な公理と定義だけを用いて“異星の数学領域”で形式的な証明を合成する能力を測るベンチマークとして「難読化された自然数ゲーム（Obfuscated Natural Number Game）」を提案します。
- Lean 4版の自然数ゲームで識別子をリネームすることで、意味的手がかりを排したゼロ知識・クローズドな環境を構築します。
- 最先端モデルの評価では、難読化により推論時間が増える「ユニバーサルなレイテンシ税」が共通して観測され、精度面では頑健性の分岐が見られます（一般モデルは性能が低下する一方、推論/証明特化モデルは意味手がかりが無くても精度を維持します）。
- 本研究は、ショートカット学習を抑えた制御条件下でモデルの“真の数学的推論能力”を定量的に評価する手法を提供すると主張しています。
