MathArena論文化：「数学が解けるAI」を測る物差しは、固定ベンチから“継続評価基盤”へ

LLMの数学能力評価で難しくなっているのは、「モデルが本当に推論しているのか、それとも既知問題を記憶・類推しているのか」を切り分けることだ。AIMEや過去のオリンピック問題のような有名データは、公開されて時間が経つほど学習データに混入しやすい。さらに、強いモデルが登場すると静的ベンチマークはすぐ飽和する。MathArenaの新論文 “Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs” は、この問題に対して、単一の固定データセットではなく、数学評価を継続的に更新・実行・集計する「評価プラットフォーム」としてMathArenaを再定義したものだ。論文は2026年5月1日にarXivへ投稿され、MathArena本体も5月4日に新論文公開を告知している。(arxiv.org)

もともとのMathArenaは、2025年論文で「新しく公開された数学コンテストをすぐ評価に使う」という発想を打ち出した。狙いは単純で、公開直後の問題ならモデルの事前学習に含まれている可能性を大きく下げられる。2025年版は、AIME 2024など既存公開問題で汚染の兆候を指摘しつつ、USAMOやIMOのような証明型コンテストも評価対象に入れ、LLMの“答えだけでなく証明を書く力”を測ろうとした。(arxiv.org)

今回の新論文で重要なのは、MathArenaが「コンテスト問題集」から一段広がった点である。対象は、最終答え型のAIME/HMMT系、USAMO・IMO・Putnamなどの自然言語証明、arXiv由来の研究レベル問題、もっともらしいが偽の定理を見抜くBrokenArXiv、そしてLeanによる形式証明のArXivLeanまで拡張された。公式サイトのベンチマーク一覧を見ると、ArXivLean、BrokenArxiv、ArXivMath、Visual Math、Final-Answer Comps、Proof-Based Comps、Project Eulerが並び、各データセットとモデル出力が公開されている。(arxiv.org)

この拡張は、数学推論を一枚岩では見ないという設計思想を示している。最終答え型では、LaTeXやSymPyによるパースで正誤を比較できる。一方、証明型では採点基準・部分点・論理の穴が問題になる。USAMO 2026評価では、LLM審査員の自己バイアスや書式バイアスを意識し、証明の整形、コード実行、GPT-5.4・Gemini-3.1-Pro・Opus-4.6による“LLM jury”、さらに人手検証を組み合わせている。これは、数学評価そのものが一つの研究課題になっていることをよく示す。(matharena.ai)

結果は印象的だ。新論文の要旨では、最強モデルGPT-5.5がUSAMO 2026で98%、研究レベル問題で74%に到達したと報告されている。MathArenaの最新モデルページでも、GPT-5.5（xhigh）は総合期待性能84.3%で1位、USAMO 2026は98.21%、ArXivMath全体は74.12%、Final-Answer Comps全体は92.30%とされる。一方でArXivLeanは17.07%にとどまり、自然言語や最終答えでは急伸している能力が、Leanで検証可能な形式証明にはまだ十分移っていないことが見える。(arxiv.org)

このギャップは重要だ。USAMO 2026のブログでは、GPT-5.4が95%に達し、2025年には目立った循環論法・根拠なき推測・構成の弱さが大幅に減ったと報告された。しかし同時に、他モデルとの差は大きく、Gemini-3.1-Proは75%、Opus-4.6は47%、最強のオープンモデルStep-3.5-Flashは45%だった。つまり「トップモデルはほぼ解く」ことと「広いモデル群が安定して証明できる」ことは別である。(matharena.ai)

研究レベル評価では、ArXivMathが中核になる。これは直近arXiv論文の抽象から最終答え型問題を作り、月次更新する公開・動的・低汚染のベンチマークだ。構築過程では、毎月約4,000本の数学論文から候補を抽出し、自己完結性、欠落条件、既存研究からの推測可能性、著者確認、人手確認を経て問題を絞る。初回版では2025年12月・2026年1月論文から計40問が作られた。ただし、最終答えが合うことは論文の証明を再構成できることを意味しない、という注意も明記されている。(matharena.ai)

BrokenArXivは別の弱点を突く。最近のarXiv論文から正しい主張を取り出し、少し変えて偽の主張を作る。モデルはそれを「証明せよ」と言われたとき、誤りを指摘できるか、それとももっともらしい証明をでっち上げるかを測られる。これは“能力”だけでなく“信頼性”や“ユーザーに迎合しない性質”の評価であり、結果はまだ厳しい。もっとも、このベンチは「常に問題文が間違っていると言う」だけで高得点になり得るため、他の正答能力ベンチと併せて読む必要がある。(matharena.ai)

ArXivLeanはさらに厳格だ。2026年3月のarXiv論文から41問を形式化し、モデルにLean証明を生成させる。Lean実行、Loogle、LeanExplore、永続補題ファイルなどのツールを与えても、全モデルが20%未満にとどまった。さらに、定理文の差し替え、非標準公理、既存定義の改変といった“ベンチマーク攻略”を防ぐため、定理文の置換検査やComparatorによる意味改変チェックも導入されている。(matharena.ai)

この動きはMathArena単独ではない。RealMathは研究論文や数学フォーラムから継続更新可能な研究数学ベンチを作り、LiveMathematicianBenchは新着arXiv定理から動的な多肢選択ベンチを構成する。LemmaBenchもarXivの補題を自己完結な定理証明課題に変換し、現行モデルの研究文脈での証明能力はpass@1で10〜15%程度と報告している。FrontierMathは専門家作成の未公開高難度問題で汚染を抑える別路線だ。MathArenaの特徴は、これらの潮流を横断するように、コンテスト、研究問題、偽命題検出、形式証明を一つの公開リーダーボード上で継続運用しようとしている点にある。(arxiv.org)

今後の焦点は、単にスコアが上がるかではなく、評価基盤がモデル進歩に追いつけるかだ。MathArenaは各問題を4回実行して平均スコアとコストを出し、IRT風のモデルで期待性能を集計するなど、単発スコアより比較可能性を意識している。一方で、新規問題は数が少なく分散が大きい。LLM審査員は便利だが、採点バイアスや基準文の曖昧さは残る。arXiv由来問題は新鮮だが、未査読論文や抽象の条件不足というリスクもある。(matharena.ai)

それでも、MathArenaの論文化は評価研究にとって大きな節目だ。GPT-5.5のUSAMO 98%は、数学コンテスト型の一部領域でフロンティアモデルが人間上位層に迫ったことを示す。一方、ArXivLeanの低スコアやBrokenArXivの難しさは、形式的厳密性と信頼性がまだ未解決であることを示す。数学AIの評価は、「正解したか」から「どの種類の数学的行為を、どれほど検証可能に、どれほど誠実に行えるか」へ移りつつある。MathArenaは、その移行を測るための生きた実験場になり始めている。