TIP
← Research

Research

LLMは未解決の数学問題を本当に「再発見」できるのか——ベンチマーク「OpenFrontiers」が示した厳しい現実

2026/11/01

LLMの「研究レベル」問題解決能力を測る難しさ

Large Language Model(LLM)は、国際数学オリンピック(IMO)のような極めて難易度の高い理論科学テストで高い成績を収めるようになった。さらに近年では、研究者でさえ未解決の問題に対してLLMを活用する試みが増えており、形式的に検証されたオリンピック問題の証明や、数学的構造の新たな構成・改善された境界の発見などが報告されている。

しかし、「未解決問題を解く能力」を測定することは、「試験の成績を測ること」とは本質的に異なる。既存のベンチマーク(FrontierMath、Humanity’s Last Exam、GPQAなど)は、出題者があらかじめ答えを知っている問題を使う。競技問題のセットは急速に飽和し、モデルの訓練データに紛れ込む可能性もある。証明レベルでの評価が示すように、最終答えの正確さは、モデルが実際に確立したことを誇張する可能性もある。

イリノイ大学アーバナ・シャンペーン校の研究者らは、こうした課題に正面から取り組む新たなリソース「OpenFrontiers」を発表した。

OpenFrontiersの構成:コーパス、ベンチマーク、評価プロトコル

12,151件の研究問題コーパス

OpenFrontiersの中核となるのは、10の最上位分野・32のサブ分野にわたる62のソースコレクションから収集された 12,151件の問題レコード からなるコーパスだ。TheoremDB(3,909件)、AIM問題リスト(3,470件)、ICM Conjectures(2,898件)など7つのコレクションが100件以上を提供している。

コーパスの特徴は、問題の状態管理にある。ステータスは「open(未解決)」「unassessed(未評価)」「partially-solved(部分的解決)」「solved(解決済み)」「disputed(係争中)」「withdrawn(撤回)」に分類される。重要なのは、ステータスが不確かな場合はopenではなく unassessed とラベル付けすることで、未解決問題の水増しを避けている点だ。実際、レコードの50.7%がopen、46.0%がunassessedとなっている。

数学が全体の93.4%(11,349件)を占め、そのうち数論(2,867件)と幾何・トポロジー(2,371件)が上位を占める。レコードの65.9%にMSC 2020コードが付与されており、16.0%にはLean 4のステートメントが添付されている。

OpenFrontiers-Bench:形式的に検査された200問のベンチマーク

コーパスから選別されたのが OpenFrontiers-Bench で、200問の研究レベル数学問題から構成される。各問題にはLean 4のステートメントが付与され、自動検証と独立した2名のレビューを通過している。

  • Rediscovery-110:2026年時点で未解決だったが、現在は解決策が特定された110問。そのうち85問には独立検証済みのLeanプルーフまたは厳密な証明書が存在する
  • Open-90:現在も未解決の90問

注目すべき観察として、Rediscovery-110の110問のうち 55問では、解決の核心部分にAIシステムが貢献したと解決資料に記載されている ことが判明した。これは、単に「モデルの訓練カットオフ以降に解決された」という条件だけでは汚染を制御できないことを意味する。そのため、評価プロトコルはモデルのリネージ(系譜)ごとに該当問題を除外し、クローズドブック条件を主たる評価とした。

高品質フィルタをかけた HQ-50(50問のサブセット)が主要な評価対象として用いられた。

3つのアクセス条件と形式的評価

評価プロトコルは、隔離されたサンドボックス内で2つの独立したLeanチェッカーが形式的証明を採点する。アクセス条件は以下の3種類だ:

  1. クローズドブック:外部情報なし
  2. フローズン検索:カットオフ前の固定コーパスのみ参照可能
  3. ライブウェブ:リアルタイムのウェブ検索が可能

評価結果:クローズドブックでの再発見は稀

7つのLLMエージェントをHQ-50サブセットで評価した結果は明確だった。

クローズドブック条件 では、40問の解決済み問題に対してエージェントが解けたのは最大7問にとどまった。しかもその多くは、短い構成(construction)で解ける人間向けの問題だったと報告されている。

ライブウェブ条件 では最大27問まで正解できたが、これはほぼすべて公開済み解法を検索・取得した結果であり、真の意味での問題解決とは言えないと著者らは指摘する。未解決の問題(Open-90に含まれるもの)については、ウェブ上に解法を見つけることなく解決したケースはゼロだったという。

また、フロンティアエージェントは問題が難しすぎると判断した場合、タイムバジェットを使い切らずに早期に諦める傾向があることも観察された。

OpenFrontiersが投げかける問い

この研究は、LLMの能力評価において重要な視点を提供している。既存のベンチマークが「既知の答えがある問題」を対象としてきたのに対し、OpenFrontiersは「誰も答えを知らない問題」に対する真の問題解決能力を測ろうとしている。

評価結果は、現在のLLMが数学的な未解決問題を独力で再発見する能力はまだ限定的であることを示唆している。一方で、AIシステムが実際の研究問題の解決に寄与しているケースが55問で確認されたという事実は、人間とAIの協働という観点からも興味深い。

データセットとベンチマークはHugging Faceで公開されており(https://huggingface.co/collections/FlippyDora/openfrontiers)、研究コミュニティによるさらなる活用が期待される。


出典: OpenFrontiers: A Collection of Open Research Problems and a Benchmark for Scientific Rediscovery