数学の発見で本当のボトルネックになるのは、解くことより問題探し

導入：証明の前に研究が詰まる

AIの数学能力が高まるにつれ、研究の制約はモデルの推論能力だけではなくなっている。より希少なのは、問題が正しく定義されているか、本当に未解決なのか、生成された議論に穴がないかを確認する専門家の時間だ。従来のAI支援では、人間が先に一問を選び、モデルに解かせ、最後に数学者が成果を確認する。この最初と最後の工程が、候補数の増加に伴ってボトルネックになる。

論文「The Problem Is the Problem: Towards Scalable Mathematical Discovery」は、この流れをFARという仕組みで組み替える。専門家は最初から一つの問題を指定するのではなく、自分の関心と知識に合う研究方向を提示する。システムはその方向に沿って文献を調べ、試す価値のある問題を探す。

中核：文献からレビューまでの段階的な選別

FARは次の三段階で構成される。

• Find：広範な数学文献から予想、未解決問題、関連する文脈を抽出する。
• Attempt：初期確認を通過した候補にモデルが取り組み、証明や解答、前進の可能性を探る。
• Recommend：自動トリアージによって、専門家が確認すべき成果物を推薦する。

組合せ論の試験では、5,245本の論文から6,453件の予想または未解決問題を回収した。問題の定式化が妥当そうか、現在も未解決とみられるかを確認した結果、4,717件が残った。続く推論と自動選別では598件の潜在的解答が浮上し、そのうち77件が著者チームのレビュー対象となった。報告された例には、Davies–Jenssen–Perkins–Roberts、Erdős–Straus、Ikenmeyer–Pak–Panova、Lund–Saraf–Wolfに関連する予想や問題が含まれる。

意義と限界：AIは研究の交通整理役になる

FARの転換点は、AIを「人間が選んだ問題に答える装置」から、「どの問題に取り組む価値があるかを整理する装置」へ広げたことだ。文献探索、重複の整理、未解決状態の確認、初期候補のふるい分けを自動化すれば、推論コストと専門家の確認をより有望な候補に集中できる。

ただし、「未解決らしい」ことは厳密な意味で未解決であることと同じではない。また、潜在的な解答も、専門家による数学的検証を経るまでは成果として確定しない。したがってFARは、無監督の定理生成器ではなく、研究ナビゲーションと優先順位付けの基盤として理解するのが適切だ。この研究が示すのは、AI数学を拡張する鍵が、推論を長くすることだけでなく、問題と専門家の注意をどう配分するかにもあるという点である。

出典：Hugging Face Daily Papers