動察 Beatingのモニタリングによると、OpenAIは初めて次期主力モデル「Astra」を正式に公開した。内部バージョンは、10年間未解決だった数学および理論計算機科学の問題において新たな結果を達成した。これらの問題の核心的な結論は少なくとも10年間進展がなく、多くはさらに長い間停滞していた。
そのうちいくつかの問題は直接解決または覆された。Astraは初めて非sofic群を構築し、群論における中心的な未解決問題に回答した。また、Connes剛性予想を覆し、3つのErdős問題を解決した。その他の成果には、球充填、符号理論、量子複雑性、およびポスト量子暗号に関連する問題の新しい上下界と困難性の証明が含まれる。
OpenAIによると、モデルがこれら10の結果を見つけるために使用したトークンは、Sol API価格で換算すると約2000ドルに相当する。
これらの数学的論証はAstraによって生成された。人間がその後、論文の整理を支援し、モデルは各証明をLean証明書に変換して、コンピュータが推論の妥当性を段階的に検証できるようにした。OpenAIは論文、証明書、およびモデルの推論プロセスを公開している。