8月1日、The Decoderが「OpenAI announces its "next major model" Astra by dropping ten previously unsolved math solutions」と題した記事を公開した。この記事では、OpenAIが次世代モデルファミリー「Astra」を発表し、数学・理論計算機科学における未解決問題10件をAIが解いたとする報告について詳しく紹介されている。
なお、本記事で「Astra」と呼ぶモデルはOpenAIが内部開発中の未公開モデルであり、一般にはまだ提供されていない。Googleが同名で展開するAIアシスタントプロジェクト「Project Astra」とは無関係の別プロダクトである点に注意されたい。
AIが10年以上未解決だった数学の難問を10件解いた
最も衝撃的な事実から述べる。OpenAIが内部開発中の未公開モデル「Astra」は、数学・理論計算機科学の未解決問題を10件解いた。いずれも少なくとも10年以上、多くはそれ以上にわたって人類が進展を遂げられなかった問題だ。
対象分野は高次元幾何学、符号理論、群論、量子複雑性理論、格子暗号、極値組合せ論にまたがる。中でも群論における「非sofic群(non-sofic groups)の存在証明」は、長年の未解決問題に決着をつけるものだ。
マンチェスター大学の数学者Thomas BloomはX上でこの結果を「大きなニュース」と評した。
「5月に公開されたunit distance予想への反例よりも重要かもしれない。少なくとも構成(constructions)という観点では、これは大きい」
— Thomas Bloom(マンチェスター大学)
Bloomはまた、AIが数学者を代替するという言説を否定している。「AIが100年以上の数学理論を引用し、数学者によって構築され、数学者の書いたものすべてで訓練されているのだから、その主張は意味をなさない」という立場だ。
10件の証明にかかったコストは約2,000ドル
OpenAIによれば、10件すべての解を生成するために使ったトークン量は、APIレートで約2,000ドル相当だという。なおここで比較基準となっているのは「Sol」と呼ばれるOpenAI内部のモデル(既存モデルファミリーの一つ)のAPIレートであり、公開されている一般向け料金体系とは異なる内部指標である点に留意されたい。
モデルが出力した数学的議論をもとに、人間が同じモデルと協力して論文に仕上げた。また各証明は、定理証明支援系言語である**Leanでも形式化されており、機械的に検証可能な証明書として公開されている。OpenAIが公開したLean形式の証明ファイル群はopenai/ten-proofs**リポジトリで参照できる。OpenAIはさらに各解に対するモデルの推論プロセスのウォークスルーも公開した。
クレジット(功績の帰属)についてはOpenAIも明確な立場を取っている。数学的議論はAstraが生成したものであり、AIが生成した証明に人間の著者名を冠することは「AIの貢献と人間の知的作業の本質を誤表示する」として、Leiden Declaration on AI and Mathematicsを参照しながら、適切な帰属の在り方を論じている。
Astraの推論技術を担う研究者の一人、Noam BrownはX上でこう述べた。
「残念ながら、ミレニアム賞問題はまだ解けていない。ただ、各問題に使ったコンピューティングはそれほど多くない。テスト時計算(test-time compute)をもっと増やせば、さらに先へ進める可能性がある」
— Noam Brown(OpenAI)
クレイ数学研究所が設定するミレニアム賞問題は7問あり、各問題に100万ドルの賞金がかかっているが、2000年の設定以来解かれたのは1問だけだ。
Astraとは何か——マルチエージェントで「数時間〜数日」動き続けるモデル
Astraは、OpenAIの既存モデルファミリー(Sol、Terra、Luna)と並ぶ新しいモデルクラスとして位置づけられている。The Informationの報道によれば、Sam AltmanはワシントンD.C.で政治家・規制当局にAstraをデモした。
Astraの核心は「複数のエージェントを長時間にわたって協調させる能力」にある。現在のAIシステムが短いタスクに限られるのに対し、Astraは数時間から数日かけて計画・推論・実験を繰り返す設計だ。製品ラインにおける位置づけ——GPT-6として独立リリースされるのか、GPT-5系列のバリアントとして提供されるのか——はまだ決定していない。リリース日も未定だ。
ただし、マルチエージェント構成には固有のリスクもある。元記事でも言及されているとおり、長いコンテキストの中でエラーが積み重なると軌道修正が難しくなる問題が指摘されている。また、タスクが密接に連携している場合にはエージェント間の調整コストが性能を逆に下げるケースも報告されている点は、実運用上の課題として注目される。
規制と長期目標
Astraは、トランプ政権が設計中の新AI規制フレームワークに基づき、公開前に連邦政府へ提出される最初のモデルになる見込みだ。
長期目標は自律的なAI研究者の実現だ。OpenAIは2028年3月までに、独立して研究プロジェクトを遂行できる完全自律AIシステムの構築を目指している。それ以前の今年9月には、研究インターンレベルのスキルを持つAIシステムを投入し、人間の科学者の研究を大幅に加速する計画もある。Astraがその役割を担う可能性がある。
Chief ScientistのJakub Pachockiはこれらのシステムには大幅に多くの計算資源が必要になると述べており、OpenAIのインフラ計画もその規模に対応した内容になっている。
詳細はOpenAI announces its "next major model" Astra by dropping ten previously unsolved math solutionsを参照していただきたい。