First Proofの研究数学テスト、ProofCouncilが10問中9問正解 オープンウェイト系は0問
2026年10月17日 18:11
研究数学の問題でAIの証明能力を測る「First Proof」は2026年10月14日、第3回の結果を公表した。未公開の問題10問に対し、複数のAIモデルを組み合わせたProofCouncilは9問、オープンウェイトモデルKimi K3を使うHumanizeは0問が正解と判定された。結果は、モデルの選択に加え、検証の仕組みや計算費用が研究での使いやすさを左右することを示している。
■未公開の研究課題を専門家が採点
First Proofの問題は、数学者が研究中に解き、証明をまだ公開していない課題から選ばれる。今回の10問は幾何学、位相幾何学、統計学、力学系などにまたがり、人間による証明はいずれも12ページ以内だった。既存の解答を検索するだけでは対応しにくい問題で、AIが証明を組み立てる力を調べる。
試験には5つのシステムが参加した。First Proof Foundationによると、各システムは人間の追加指示を受けず、問題ごとに最長24時間で解答した。10月8～9日には30人の数学者が提出元を伏せた答案を読み、数学的な正しさ、説明の明瞭さ、先行研究の適切な引用を別々に評価した。
運営するFirst Proof Foundationの編集者は、スタンフォード大学のMohammed Abouzaid、カリフォルニア大学バークレー校のNikhil Srivastava、テキサス大学オースティン校のRachel Ward、ハーバード大学のLauren Williamsだ。第3回にはDARPA、Survival and Flourishing Fund、AI for Math Fund、Google.orgが資金を提供し、AnthropicとOpenAIも使途を限定しない寄付を行った。
■ProofCouncilは複数のモデルで証明を検討
最高成績のProofCouncilは、ETHチューリヒのTim Gehrungerを中心とするチームなどが開発した。著者役のAIが証明を書き、批評役が論証の誤りや不足を指摘して改稿を促す。別の批評役による確認や、複数モデルからの助言、数学ソフトを使う計算担当も組み込んでいる。
First Proofの報告書によると、第3回のProofCouncilはGPT-6 Astra Pro、GPT-6 Astra、Claude Fable 5.1、Claude Sonnet 5、Gemini 3.1 Proのプレビュー版を利用した。開発チームが公表した仕組みでは、批評役の会話履歴を定期的にリセットし、先入観のない評価を得る。計算担当は必要に応じてSageMathやGAP、PARI/GPなどを使い、具体的な計算を点検する。
10問全体の実行費用はProofCouncilが1888ドル（約29万8000円）、GPT-6 Astraを単独で呼び出す構成が36ドル（約5690円）だった。正解数はそれぞれ9問と7問で、いずれも前回より2問増えた。ProofCouncil開発チームが公表した前回の費用内訳では、著者役が48.8％、批評役が31.6％を占め、証明の作成と点検を繰り返す構成に費用がかかっていた。
■Kimi K3を使う提出システムは正解0問
HumanizeはZhengyang Zhangを中心とするチームが開発し、Moonshot AIが2026年7月に公開した2兆8000億パラメータのKimi K3を利用した。First Proofの試験ではモデルを自前で稼働させ、10問すべてに答案を提出したが、専門家はいずれにも重大な誤りがあると判定した。実行費用は約2000ドルだった。
First Proofは参考として、2025年12月公開のGPT-5.2 Proによる答案も同じ問題の査読者に比較してもらった。報告書ではHumanizeの答案を総じてGPT-5.2 Proより低く評価しているが、この比較は正式な採点とは別に行われた。さらに5種類のオープンウェイトモデルを簡易的に試し、生成された答案を自動評価した結果、肯定的な点数が見込めるものはなかったとしている。
Epoch AIが2026年5月までの幅広いベンチマークを集計した分析では、オープンウェイトモデルは最先端の非公開モデルに平均約4カ月遅れていた。First Proofが測ったのは、その総合指標とは異なる、未公開の研究数学問題への対応力だ。今回の結果は、この分野で利用するシステムを選ぶ際、モデル名だけでなく証明の検証手順まで見る必要があることを浮かび上がらせた。
■費用、機密性、証明の読みやすさ
オープンウェイトモデルは、自分で管理する計算環境で動かせる。未発表の研究内容を外部サービスに送ることを避けたい研究者には、その運用方法が選択肢となる。一方、OpenAIはビジネス向けサービスとAPIの入出力を、初期設定ではモデルの学習に使わないと説明している。研究内容を扱う際には、利用するサービスの設定とデータの取り扱いを確認することが重要だ。
2026年9月には、数学者のTristan Buckmasterらによる流体方程式の研究とOpenAIの研究成果を巡り、情報の扱いが議論になった。OpenAIは調査後、Buckmasterが発表前の約2カ月間にCodexへ入力した内容は、学習を含むいかなる形でも同社システムの成果に影響しなかったと説明した。
証明の質にも課題が残った。First Proofによると、先行研究への適切な言及が認められた答案は、GPT-6 Astra単独で10件中4件、ProofCouncilで7件だった。ProofCouncilでも答案の約3分の1は説明の平均点がマイナスで、論証を専門家が読み解きやすい形にまとめる余地がある。
バッファロー大学のAdam Sikoraが提供した量子トポロジーの問題では、ProofCouncilだけが正解した。同大学の発表でSikoraは、この構成にはプログラミングの専門知識と複数の高性能モデルへの有料アクセスが必要だと述べた。研究者がAIの能力を活用するには、解答の正確さに加え、費用と利用環境も検討することになる。
■次回はモデルの種類を分けて試験
First Proofは第4回の結果を2027年1月前半に公表する予定だ。最先端の非公開モデルを使うシステムとオープンウェイトモデルを使うシステムを分け、それぞれに適した問題で能力や失敗の傾向を詳しく調べる。編集委員会は、より自由度の高い数学の問いも今後扱いたいとしている。
第3回の発表と同じ10月14日には、数学者のDeanna NeedellとHayden SchaefferがTerence Taoのブログに寄稿し、人間とAIの協働事例を募った。過去の研究をどう生かし、AIが示した論証をどう検証して発展させたかも募集対象に含まれる。First Proofの採点結果とともに、AIの答案を研究の過程でどう使うかを考える材料となる。
元記事: First Proof Math Benchmark: Open-Weight AI Ten Months Behind Frontier Tools