メインコンテンツまでスキップ

OpenAI Astra: プレビュー・フィールドノート

中級

2026 年 8 月 1 日、OpenAI は次期主要モデルファミリー Astra を予告した — 基調講演やローンチページではなく、これまで未解決だった数学および理論計算機科学の問題に対する Lean-4 で形式化された 10 本の証明 を公開 GitHub リポジトリに push する形で。API も価格表も ChatGPT 上のサーフェスも公開日もない。今週目にする「Astra vs GPT-5.6」「Astra vs Claude」の購入ガイドは、報道の体裁をまとった憶測にすぎない。

このページは Claude ユーザーのための率直なフィールドノートである。確定している事実、そうではないもの、そして 今日の判断を変えるべきか を示す。

What you'll learn
  • 2026 年 8 月 1 日に OpenAI が採った告知手段と、実際に述べたこと / 述べなかったことを把握する
  • Astra が解いた 10 の問題を読み、なぜ数学 / TCS を発表サーフェスに選んだかを理解する
  • 確定事実(マルチエージェント・長期ホライズン・社内限定)と憶測(コンテキストサイズ・価格・ChatGPT ロールアウト・ベンチマーク)を切り分ける
  • 今日は Claude Opus 5 / Fable 5 の上に構築を続けるか、それとも待つか — 具体的な指針で判断する

ひと言でまとめると​

Astra は OpenAI の 社内限定・マルチエージェント・長期ホライズン の次世代モデルであり、Lean で検証可能な 10 本の数学証明を通じて公表された。GPT-5.6 Sol / Terra / Luna とは別物 であり、製品サーフェスは存在しない。したがって今月あなたが下すマイグレーション判断は依然として、Astra ではなく Claude と GPT-5.6 と Gemini 3.6 の間の判断である。

OpenAI が実際に述べたこと(そして述べなかったこと)​

告知の仕方が異例だ。OpenAI は「次の主要モデル」を研究記事の 第 3 段落 で公表し、プレスリリースもベンチマーク数字も可用性も価格もない。この見せ方はモデルそのものと同じくらい多くを語っている — 「まだ製品ではなく、規制審査中」と述べているのだ。

2026 年 8 月 1 日に確定した事実​

  • Astra はモデルファミリー名である。 OpenAI は「私たちの次の主要モデル」と表現する。GPT-5.6 の Sol / Terra / Luna 各ティアの内側ではなく、隣に位置する。
  • 結果は社内バージョンから得られた。 ChatGPT アプリでもなく、API でもなく、パートナー限定チェックポイントでもない。
  • 公開サーフェスは数学 + TCS である。 これまで未解決の 10 問について、それぞれ Lean-4 の証明を github.com/openai/ten-proofs(Apache-2.0)に push した。
  • システムはマルチエージェントかつ長期ホライズン。 OpenAI 自身の説明は、Astra が「複数のエージェントを協調させ、数時間から数日にわたる長時間タスクを実行するよう設計されている」というもので、研究・コーディング・科学問題を主眼とする。
  • コストの目安(モデル価格ではない)。 OpenAI は 10 本の解答生成に使ったトークンが「Sol の API 料金で計算すると約 $2,000 に相当した」と述べている。これは Astra の定価でも証明あたりのコストでも再現性保証でもない — 別モデルのメーターで見積もったトークン量の目安 にすぎない。
  • 政府審査のプロセス。 サム・アルトマンは 2026 年 7 月末にワシントン D.C. で米連邦当局者に本システムをデモした。報道は、Astra が公開前に連邦審査を必須とする米国の新たな枠組みの下で提出される最初のモデルになる可能性が高い、と位置づけている。
  • 本人発言。 OpenAI 研究者のノーム・ブラウンは Astra を「科学的推論の大きな一歩」と評し、「残念ながら、ミレニアム懸賞問題はまだない」と付け加えた。

目にするかもしれないが、確定していない事項​

  • リリース日はない。 ChatGPT ロールアウトのスケジュールも、API の GA も、ベータ登録もない。
  • 価格はない。 トークン単位でも、実行単位でも、ティア単位でもない。
  • コンテキストウィンドウのサイズも最大出力も未公表。
  • マルチモーダルの主張はない。 画像・音声・動画については何も述べられていない。
  • 直接比較のベンチマークはない。 SWE-Bench も ARC-AGI も Frontier-Bench も数値なし。
  • 「これは GPT-6 か?」への回答はない。 Astra が GPT-6 として出荷されるのか、GPT-5.x の別ポイントリリースなのか、独自名で出るのか、OpenAI は語っていない。
  • ティア構造の確認はない。 GPT-5.6 の Sol/Terra/Luna パターンが Astra に対応するかは示されていない。

今週の見出しが上記のいずれかを事実として提示していれば、それは憶測である。

10 本の証明を 1 画面で​

Astra の公表を Lean-4 で形式化された未解決問題の証明に託した選択は多くの役割を担っている — OpenAI は 機械検証可能 な能力主張が可能になる。ゲーミングされうるリーダーボード数字ではなく。lake build All で証明が検証されれば、モデルに対する評価に関わらず数学的主張は本物である。

#問題分野
1球充填密度に関する漸近上界の改良高次元幾何学
2バイナリ符号に対する指数的により強い上界符号理論
3非 sofic 群の構成群論 / 作用素環論
4Connes 剛性予想への反例作用素環論
5permanent 計算の新しい下界算術回路計算量
6任意有限ゲームに対する指数的並列反復量子計算量
7Closest Vector Problem の多項式因子近似困難性格子暗号
8各次元における最大体積の鋭い評価(Ehrhart)離散幾何学
9多色ラムゼー数の超指数的下界極値組合せ論
10コンパクト性および退化性予想への反例極値数論

なぜ数学 + TCS を発表サーフェスに選んだのか​

実務的な理由が 3 つある — 気づいてしまえばどれも神秘的ではない:

  1. 機械検証可能な主張はスピンできない。 ベンチマーク数値はマーケティングのピクセルにすぎないが、Lean 証明は型検査に通るか通らないかのどちらかだ。すべての研究所の主張が疑問視されている年において、これが最もクリーンな能力主張である。
  2. リーダーボード・ゲーミングの疑いを招かない。 これまで未解決だった問題の解法を Astra が丸暗記したと疑う者はいない。
  3. 規制上の見せ方。 OpenAI は米国の新たな連邦審査プロセスに Astra を通しつつある。「我々の新しいモデルは暗号と量子計算量における未解決問題を前進させた」というフレーミングは、「我々の新しいモデルは SWE-Bench で 96% を取った」とはまったく別物である。

今日の Claude vs GPT-5.6 判断において、Astra が変えるもの​

今月中にアクションを要するものはない。Astra には製品サーフェスが存在しない: その上に構築することはできない。あなたの実際のトレードオフは依然として モデル選択 のとおりである:

  • 実リポジトリのソフトウェアエンジニアリング、大規模リファクタリング、うまく管理されたプラットフォーム上の長いツールループ → Claude Opus 5(claude-opus-5)または Fable 5(Opus 5 field guide、Fable 5 / Mythos 5 flagship 参照)。
  • 最安ティアでのロングコンテキスト大量処理 → GPT-5.6 Luna、入力 $1 / 出力 $6 で 1.05M フルコンテキスト(Sol / Terra / Luna)。
  • ブラウザ主体またはエージェント・インデックス型のタスク → GPT-5.6 Sol または Gemini 3.6 Flash(Gemini 3.6 Flash family)。
  • 長期ホライズンのマルチエージェント研究・エンジニアリング — まさに Astra が狙う形 — 今日利用できる最も近い選択肢は OpenAI Responses API 上の ネイティブ・マルチエージェント API ベータと、Anthropic の managed agents + memory stores である。どちらも出荷済み製品だが、Astra はそうではない。

Astra を待つべきか?​

Guided walkthrough1 of 4
  1. Astra には API も価格も公表されたリリース時期もない。開示は研究記事であり、製品発表ではない。今あるもので出荷し、価格と品質が見合うなら後で移行すればよい。

10 本の証明をローカルで検証する

# Requires elan (Lean toolchain manager)
# Install: curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh
git clone https://github.com/openai/ten-proofs.git
cd ten-proofs
lake exe cache get     # pre-built mathlib artifacts
lake build All         # type-checks every proof; exits 0 on success

lake build All が 0 で終了すれば、10 本の証明すべてが mathlib に対して型検査を通っている。これは OpenAI が今年発表した最も強い能力主張であり、あなたのラップトップで検証可能である。

ジャーナリストが繰り返し取り違えていること 3 つ​

Enter キーまたはスペースキーでカードを裏返します。左右の矢印キーでカードを移動できます。用語を表示しました。
1 / 5

AILmanac がこのページを更新するタイミング​

OpenAI がモデルカード、API エンドポイント、価格表、あるいは公式の ChatGPT ロールアウトを公表したときに 限って このページの lastVerified を更新する — 噂ではない。それまでの間、10 本の証明とマルチエージェントのフレーミングが記憶すべき恒久的な事実である。

  • 価格ページが出たら → このページはティア表付きのフル Astra フィールドガイドになり、Sol / Terra / Luna や Opus 5 と同じ体裁になる。
  • API が出たら → 「Claude Opus 5 プロンプトを Astra に移植する」セクションを既存の porting prompts across models ガイドと並べて追加する。
  • Anthropic が『長期ホライズン・マルチエージェント』相当のプリミティブを出荷したら → managed agents を更新し、相互リンクする。

Check yourself

0/3
  1. 2026 年 8 月 1 日、OpenAI は Astra について実際には何を確定させたか?
  2. 開示の中の『Astra は約 $2,000 かかる』という数字が指すのは……
  3. Astra を理由に今月あなたの本番 Claude アーキテクチャで変更すべきものはどれか?

情報源とさらに読むもの​

次に​