OEIS Open、Leanで492件の未解決予想を検証——クロスチェックで合格数を147件から144件に訂正

Epoch AIの研究者らは、オンライン整数列大辞典（OEIS）に由来する492件の未解決予想を、再現可能なモデル評価へと変換した[OEIS Open](https://arxiv.org/abs/2608.11941)を発表した。各問題はLeanで記述されており、モデルは予想、またはその否定命題について形式証明を提出しなければならない。合否判定は既知の解答との照合や別のモデルによる採点ではなく、Leanカーネルに依存する。これにより、公開された解答がまだ存在しない問題をベンチマークに利用でき、解答が訓練データにそのまま含まれている可能性も抑えられる。

著者らは、Claude Opus 4.8、GPT-5.5、Gemini 3.5 Flashなどのモデルに、基本的なshell、ファイル編集機能、Leanコンパイルツールを使用させた。全問題セットでは1問当たりの予算を50ドルとし、全モデルが成功した証明の和集合は147問、全体の30％に達した。無作為に抽出した100問からなるLite版で1問当たりの予算を200ドルに引き上げると、最高性能のモデルは44％を達成した。注目すべきことに、47万6,000本のarXiv数学論文を追加で提供しても、より複雑なDeepAgentループを採用しても、Lite版の成績は改善しなかった。これは、現在のボトルネックが単なる検索対象コンテンツや計画ステップの不足とは限らないことを示している。

エージェントによる定理の改変、許可されていない公理の追加、ツールチェーンの汚染を防ぐため、各試行はネットワーク接続のないエージェント環境、クリーンなコンパイル環境、検証用コンテナに分離された。SafeVerifyはビルド成果物を最初から再現し、対象宣言の名前、型、使用可能な公理を照合する。公開結果リポジトリには、各問題のLeanファイル、tokenコスト、失敗した段階も保存されており、第三者による監査が可能になっている。

ただし、検証器そのものにも議論の余地が残る。著者らがLeanチームのComparatorを使ってClaude Opus 4.8の結果をクロスチェックしたところ、5問では元の形式化に異常があり、別の2問はSafeVerifyがリソースを使い果たしただけだった。Comparatorによる集計では、成績を147／492から144／492へ訂正すべきだという。これらの予想の多くは注目度が低く、数学的重要性も定まっていないうえ、スコアは数学的推論能力とLeanエンジニアリング能力を同時に測っている。今後は、仕様に対する人手での監査、検証器の統一、モデルがより低いコストで合格済みの証明を再現できるかを追跡する必要がある。