OpenAIのAstraモデル、10件の未解決数学問題にブレークスルー
OpenAIは2026年8月2日(現地時間)、次期主要モデルAstraの内部版が、数学および理論計算機科学における長年の未解決問題10件でブレークスルーを達成したと発表した。同モデルは、発見した各問題の証明をLeanで形式化し、定理証明システムによる検証を可能にした。
Tag
#Lean
5 件の関連記事
OpenAI、次世代AIモデル「Astra」発表 未解決数学問題10件を解決
OpenAIは2026年8月1日(現地時間)、次世代AIモデルファミリー「アストラ (Astra)」を発表しました。Astraは長時間タスクと複雑な問題に対応するよう設計され、数学および理論計算機科学の未解決問題10件を解決したとされます。同社は、解決した証明を形式化言語リーン (Lean) で公開し、機械検証を可能にしました。これらの解決にかかる推論コストは、既存モデルSolのAPIレートで約2,000ドルに相当するとされています。
OpenAI、数学・計算機科学の10問題で進展を発表
OpenAIは2026年8月1日(現地時間)、数学および理論計算機科学分野で長年にわたり未解決だった10の主要問題に対し、新たな研究成果を発表した。これらの成果は、開発中の大規模言語モデル「アストラ (Astra)」の内部バージョンを用いて達成されたという。
【速報】Microsoft、SymCryptでRust暗号の形式検証を公開
Microsoftは2026年7月13日(現地時間)、セキュリティ保証を高めるため、SymCryptにおけるRust暗号の形式検証に関する進捗を発表した。同社はRust、Aeneas、Leanを用いて、生産環境で使用される暗号アルゴリズムの形式検証をスケールアップしている。特にSHA-3とML-KEMの検証済みコード、仕様、プロパティ、証明を公開し、現在Windowsのインサイダービルドに導入されていることを明らかにした。
メタエージェントの操作を形式化する「Shepherd」、実行トレースで開発効率向上
Simon Yu氏らは5月11日(現地時間)、メタエージェントの動作を関数として形式化する新たなプログラミングモデル「Shepherd（シェパード）」を発表した。このモデルは、メタエージェントと環境の全相互作用をTypedイベントとして記録し、Gitに類似した実行トレースを生成する。これにより、過去のいかなる状態も効率的に分岐および再現できるようになり、開発とデバッグの効率向上が期待される。