最新情報

OpenAIの次世代AIモデル「Astra」、約2,000ドルの計算コストで10件の未解決数学問題を解決

OpenAIは、まだ一般公開されていない次世代AIモデル「Astra」が、数学および理論計算機科学の分野において、長年未解決だった10件の問題を解決したと発表した。これらはいずれも少なくとも10年以上にわたり未解決だった問題である。

OpenAIは今回の成果とともに、249ページに及ぶ論文原稿と、Lean 4による機械検証可能な証明データをGitHub上で公開した。Leanによる形式検証では、すべての証明について未証明部分を示す「sorry」がゼロとなっており、形式化された証明の各ステップが検証済みであることを意味している。

27年間未解決だった「非ソフィック群」の問題を解決

今回の成果の中でも特に注目されているのが、非ソフィック群（non-sofic group）の具体的な構成である。

ソフィック性という概念は数学者ミハイル・グロモフによって1999年に提示されて以来、「非ソフィック群が実際に存在するのか」という問題が長年議論されてきた。Astraは今回、その具体例を構成したとされている。

このほかAstraは、

フォン・ノイマン環に関するConnesの剛性予想を反証
Ehrhartの体積予想を証明
Paul Erdős（ポール・エルデシュ）が残した問題のうち3件を解決
多色Ramsey数
高次元球充填問題
二元符号・球面符号
算術回路の計算量
量子並列反復
最近ベクトル問題（Closest Vector Problem）の計算困難性

など、幅広い数学・理論計算機科学分野で新たな成果を生み出したとされている。

10問すべてを解くための計算コストは約2,000ドル

さらに注目されているのが、そのコストだ。

OpenAIによると、Astraがこれら10件すべての解答を発見するために必要とした計算コストは、GPT-5.6 Sol APIの料金換算で約2,000ドルだったという。

OpenAIの数学研究責任者Sebastien Bubeck氏も成果を確認しており、研究科学者Noam Brown氏は、この成果について科学的推論能力における大きな前進だとの見方を示している。

数学的な核心部分の推論はAstraによって生成され、その後、人間の研究者がAstraの出力を整理し、学術論文として発表できる形式へとまとめたという。

Leanによって第三者でも証明を検証可能

今回の研究で重要なのは、OpenAIが単に「AIが数学問題を解いた」と発表しただけではなく、Leanという形式証明システムで検証可能な証明を公開している点である。

Leanでは、証明が論理的に正しいかどうかをシステムのカーネルが判定する。そのため、第三者の数学者も公開された証明データを使って、Astraの証明が形式的に正しいかどうかを独立して確認できる。

ただし、今回発表された10件の成果については、記事掲載時点では正式な査読（peer review）をまだ受けていない点にも注意が必要である。

数学界ではAI研究をめぐる議論も

一方で、AI企業と数学研究コミュニティの間では、AIを研究に利用することについて議論も続いている。

国際数学連合（IMU）は2026年6月、AI企業による研究成果の利用、査読プロセス、研究成果の帰属やクレジットなどに関する懸念を示した「Leiden Declaration」を支持した。

OpenAI自身も、AIが生成した数学的成果を人間だけの成果として扱うことは適切ではなく、AIが研究にどの程度貢献したのかを明確に示す必要があるという姿勢を示している。

Astraの公開時期は未定

現時点でOpenAIは、Astraをいつ一般公開するのかについて正式な日程を発表していない。

また、Astraが将来的に「GPT-6」という名称になるのか、それとも現在のGPT-5シリーズの一部として提供されるのかについても明らかにされていない。

今回の成果が外部研究者による検証を経て確認されれば、AIが既存の数学知識を説明したり既知の問題を解いたりするだけではなく、人類がまだ解決していない科学・数学上の問題に対して、新しい発見を生み出す段階に入りつつあることを示す重要な事例になる可能性がある。

https://tech.yahoo.com/ai/articles/openai-astra-model-solves-10-124919950.html