Google DeepMindの研究者は、同社のシステム「AlphaProof Nexus」がエルデシュ問題9問を解決し、その証明の多くを人間の数学者が確認したと報告しました。査読済みの研究論文は、OpenAIが未公開のAIモデルで作成した数学原稿722本を投稿した2日後に公開されました。この研究は10月8日に『サイエンス』で報じられました。

システムはGoogleの言語モデルGeminiを基盤とする複数のエージェントを使い、未解決のエルデシュ問題353問に取り組みました。難しい段階では、数学用に訓練されたモデルAlphaProofを呼び出せます。また、証明の各段階が形式化された命題に従っているかを検査するソフトウェアLeanも使いました。エージェント同士は有望な試みを共有し、進展のない試みは破棄しました。

研究者は、全システムが解いた9問について、より単純な構成も試しました。独立したGeminiエージェントはLeanのフィードバックを使いながら、試みを共有せず、AlphaProofにも相談せずに9問すべてを解きました。この構成は簡単な問題では計算資源が少なくて済み、最難関の2問ではより多く必要でした。全システムが解けなかった問題も解けるかどうかは確認されていません。共著者のスワラット・チョードリー(Swarat Chaudhuri)は結果に驚いたと述べ、高性能な言語モデルが比較的単純な検査ツールを使って研究数学に取り組めることを示唆すると話しました。

Leanが検査するのは、ソフトウェアに入力された命題だけです。数学的命題をLeanに入力する際や、Leanから取り出す際に誤訳される可能性もあります。10月6日のプレプリントは、OpenAIが文章で示したナビエ・ストークス方程式の証明と、対応するLeanの証明の一部に食い違いがあると指摘しました。著者らは、食い違いは文章の証明が誤りだとは示さないと説明しましたが、Leanで証明が成立してもAI生成論文全体が自動的に正しいと確認されるわけではありません。チョードリーは、数学者が問題を考え抜き、システムの目標を設定する必要があると述べました。また、確認済みの段階は証明が未完成の場合に欠落を見つける助けにもなると話しました。

ポール・エルデシュが提起または収集した1,000問超を追跡するサイトを運営するマンチェスター大学の数学者トーマス・ブルーム(Thomas Bloom)は、訪問者が理解できないことも多いAIの証明で問題を解こうと競うようになっていたと述べました。記者との会話後、ブルームは問題を未解決・解決済みと表示するのをやめ、コメント欄を閉じました。その時点ではOpenAIの成果をまだ知りませんでした。ブルームはAlphaProof Nexusの成果は最重要級ではないとし、Google DeepMindはより慎重な姿勢を取っていると評価しました。OpenAIは共有方法について独立した諮問グループと協議したと説明しましたが、同グループによると、未公開AIモデルを高度な数学で試さないよう助言していたにもかかわらず、OpenAIは実施しました。

ノースウェスタン大学の数学者ブリーナ・クラ(Bryna Kra)は、OpenAIが過去の研究文献の引用を改善した一方、AIモデルが未公開研究にアクセスしたのではないかとの懸念が研究者の間に広くあり、アイデアの共有をためらわせていると述べました。Plasma AIの最高技術責任者アンドリュー・ターナー(Andrew Turner)は、AIによって数学がより身近になり、これまで想像もできなかった問いへの回答に役立つ可能性があると話しました。ブルームがサイトの運用を変えてから数日後、Plasma AIはAIによる成果を歓迎する別のエルデシュ問題追跡サイトを発表しました。ブルームは好奇心を持ち続け、AIを補助として扱いながら、自分たちで数学の問題に取り組み続けるよう呼びかけました。

Google DeepMindの研究者は、同社のシステム「AlphaProof Nexus」がエルデシュ問題9問を解決し、その証明の多くを人間の数学者が確認したと報告しました。査読済みの研究論文は、OpenAIが未公開のAIモデルで作成した数学原稿722本を投稿した2日後に公開されました。この研究は10月8日に『サイエンス』で報じられました。

システムはGoogleの言語モデルGeminiを基盤とする複数のエージェントを使い、未解決のエルデシュ問題353問に取り組みました。難しい段階では、数学用に訓練されたモデルAlphaProofを呼び出せます。また、証明の各段階が形式化された命題に従っているかを検査するソフトウェアLeanも使いました。エージェント同士は有望な試みを共有し、進展のない試みは破棄しました。

研究者は、全システムが解いた9問について、より単純な構成も試しました。独立したGeminiエージェントはLeanのフィードバックを使いながら、試みを共有せず、AlphaProofにも相談せずに9問すべてを解きました。この構成は簡単な問題では計算資源が少なくて済み、最難関の2問ではより多く必要でした。全システムが解けなかった問題も解けるかどうかは確認されていません。共著者のスワラット・チョードリー(Swarat Chaudhuri)は結果に驚いたと述べ、高性能な言語モデルが比較的単純な検査ツールを使って研究数学に取り組めることを示唆すると話しました。

Leanが検査するのは、ソフトウェアに入力された命題だけです。数学的命題をLeanに入力する際や、Leanから取り出す際に誤訳される可能性もあります。10月6日のプレプリントは、OpenAIが文章で示したナビエ・ストークス方程式の証明と、対応するLeanの証明の一部に食い違いがあると指摘しました。著者らは、食い違いは文章の証明が誤りだとは示さないと説明しましたが、Leanで証明が成立してもAI生成論文全体が自動的に正しいと確認されるわけではありません。チョードリーは、数学者が問題を考え抜き、システムの目標を設定する必要があると述べました。また、確認済みの段階は証明が未完成の場合に欠落を見つける助けにもなると話しました。

ポール・エルデシュが提起または収集した1,000問超を追跡するサイトを運営するマンチェスター大学の数学者トーマス・ブルーム(Thomas Bloom)は、訪問者が理解できないことも多いAIの証明で問題を解こうと競うようになっていたと述べました。記者との会話後、ブルームは問題を未解決・解決済みと表示するのをやめ、コメント欄を閉じました。その時点ではOpenAIの成果をまだ知りませんでした。ブルームはAlphaProof Nexusの成果は最重要級ではないとし、Google DeepMindはより慎重な姿勢を取っていると評価しました。OpenAIは共有方法について独立した諮問グループと協議したと説明しましたが、同グループによると、未公開AIモデルを高度な数学で試さないよう助言していたにもかかわらず、OpenAIは実施しました。

ノースウェスタン大学の数学者ブリーナ・クラ(Bryna Kra)は、OpenAIが過去の研究文献の引用を改善した一方、AIモデルが未公開研究にアクセスしたのではないかとの懸念が研究者の間に広くあり、アイデアの共有をためらわせていると述べました。Plasma AIの最高技術責任者アンドリュー・ターナー(Andrew Turner)は、AIによって数学がより身近になり、これまで想像もできなかった問いへの回答に役立つ可能性があると話しました。ブルームがサイトの運用を変えてから数日後、Plasma AIはAIによる成果を歓迎する別のエルデシュ問題追跡サイトを発表しました。ブルームは好奇心を持ち続け、AIを補助として扱いながら、自分たちで数学の問題に取り組み続けるよう呼びかけました。