🔬非公式AIを超えるスケーリング - Carina Hong, Axiom Math

2025年、創業7か月のスタートアップAxiomは、名門の学部数学試験であるPutnam試験の全12問を解決しました（制限時間内に8/12点、最終的に12/12点）。この成績は、最優秀の学部生（110/120）やこれまでに結果を報告したAIシステム（DeepSeek 103/120）を上回っていますが、時間がもっとあれば人間や他のシステムがどれだけの点数を取れたかは不明です。それでも、Putnam試験はその難しさで伝説的であり、中央値は通常0点か1点です。この成果は、Deep BlueがKasparovに勝利したことに始まる、AIが人間とのエリート競技で達成してきた一連の成果の1つに過ぎないように見えます。

しかし、2026年半ばに早送りすると、Claude CodeとCodexが世界を席巻しています。2024年には、Anthropicのコードとエンタープライズへの賭けは、OpenAIの優れたモデルと巨大なコンシューマースケールに対して、より実用的なニッチ戦略に見えました。今日、Amodeiのコードによる加速への全力投球（画像やビデオは無視）は先見の明があったように思えます。

Anthropicの勢いが増す一方で、AxiomのCEO Carina Hong氏は、コーディング能力はAGIへの道において必要なマイルストーンではあるが、十分ではないと考えています。コードは、おそらくコーディング以外のいくつかの領域で、フロンティアを超知能のポイントに押し上げますが、驚くべきギャップがあり、それがAIの進歩のボトルネックになるとCarina氏は考えています。

非公式のボトルネック

「検証型AI」は、ブロッコリーを食べたり税金を払ったりするように聞こえるかもしれませんが、Axiomにとってはまったく異なる意味を持ちます。「検証とは、私にとっては brilliance をスケールし、brilliance を複利で成長させることです」とCarina氏は語ります。

彼女が何を意味するのか理解するのには時間がかかりました（マーケティング用語に聞こえましたが、突然納得しました）。Carina氏は、伝説的な数学者Srinivasa Ramanujan（『知られざる無限』）を引き合いに出して、この点を説明します。G.H. Hardyが最終的にRamanujanに、彼の（強力な）直感に頼るのではなく、定理を形式的に証明するよう説得したとき、それが彼自身の能力を向上させたとされています。これはおそらく、形式的に証明することが、Ramanujanに詳細を明確に表現させ、新しい思考の線を開くためです。これが数学における「複利効果」です——不安定な基盤ではなく、堅固な基盤の上に構築することであり、これが公理として知られています。

しかし、形式的に証明することは、他の人が彼の直感から利益を得ることも可能にしました。証明は直感を伝え、その直感が正しいことを他人に納得させる方法です。これがスケーリング（より多くの人が結果を利用する）と複利効果（人々が彼の研究から学び、それを基に構築できる）です。

これが、Axiomが取っているアプローチを理解するための核となる洞察です。

検証された生成

検証型AIは、トレーニングと推論の2つの方法で現れます。

しかし、少し脱線します。大ざっぱに言うと、「形式的検証」とは、Leanのような言語で綿密に指定された数学的証明を検証するために、型チェッカー（TypeScript、C++、Rustの型チェッカーよりも強力なもの）を使用することを意味します。「非公式な」証明（ほとんどの人が「非公式」とは呼ばないであろうもの）をLeanの証明に変換するには、多くの作業が必要です。Axiom自身は、AXLEという画期的なツールキットをオープンソース化しています。これは、数学的証明を探索、検証、操作するためのインタラクティブなLeanアプリケーションのセットです。

これが強化学習中に非常に有用であることが想像できます。統計に基づく最良の推測（GRPO、RLHFなど）に頼る代わりに、Lean検証器を使用して証明が正しいかどうかを直接検証できます。これは明らかに、コードをコンパイルしてテストする（コーディングのRLで通常行われること）と同様に、はるかに強力な報酬シグナルです。

問題は、LLMが現在Leanでの証明をあまり得意としていないことです。

Axiomの登場：彼らは12/12のPutnam結果以外のベンチマーク数値を公式に報告していませんが、Carina氏によると、Verinaコード生成ベンチマークで非常に印象的な99％（187/189）のProofGenを達成したとのことです。このベンチマークは、一連の問題に対してコードと正しさの証明を生成することを要求します。比較として、OpenAI o3（最後に知られているOpenAIの実行）はこのベンチマークで4.9％しか達成していません。

散発的なベンチマークに基づくと、フロンティアラボが現在どのような状況かを言うのは難しいですが、Carina氏は、彼らがまだLean証明を直接生成するようにトレーニングしておらず、非公式の証明に依存していると示唆しています。

フロンティアラボの現在のアプローチがこのギャップを埋めるかどうかは、時間が経てばわかるでしょう。

スケーリングと複利効果

Carina氏のRamanujanの類推は非常に直接的です。より良い証明 → より良いLean生成 → より良いRL。より強いシグナルは、より高いサンプル効率とより高い最大性能を意味します。素晴らしい！

スケーリングも明確です：Leanで何かを証明してしまえば、出力の品質は基本的に人間が作ったものと同じくらい高いので、高品質なトレーニングセットは非公式のロールアウトコーパスでは不可能な方法で成長します。Leanの証明を信頼できます。

複利効果も明確です：将来のすべての推論とトレーニングは、それらの証明の上に構築できます。

一方、GRPOなどの統計的シグナルのみを使用してトレーニングされたモデルは、RL中にサンプル効率、最大性能、および複利効果コーパスを欠いており、形式的検証を使用するシステムが恩恵を受けます。

すべての道は検証に通ず

ブロッコリーや税金はさておき、検証は私たちの多くの会話に登場しています。物理システムの領域では、Applied Intuitionを思い出してください：

「[検証可能性]はおそらく現在最も難しい問題だと思います。なぜなら、モデルが良くなるにつれて、システムの欠陥を見つけるのがますます難しくなるからです。そして、それらの欠陥を見つけるための適切な評価を行う問題も、モデルが良くなるにつれて難しくなっています。」

理論物理学では、Alex Lupsascaを思い出してください：

「…現在は、ChatGPTに同時に何千もの質問に取り組ませることができ、そのかなりの割合に対して証明を返してくれる時代です。今や責任は人間に戻り、すべての出力を検証することになります。そして、それがボトルネックになるにつれて、数学の形式化と検証の自動化がより価値を持つようになるでしょう。」

実際、検証は科学のためのAIと計算のためのAIの重要な違いです。科学では、物理実験を行うことによって仮説を実際にテスト（検証）する必要があります。Radical AIやLilaのようなラボ・イン・ザ・ループシステムは、まさにこの前提に基づいて構築されています（これらのチームとのエピソードを録画済みで、近日公開予定です！）

そしてもちろん、飛行制御、原子力発電所、ペースメーカーなどの重要なシステムの形式的検証は、それらを実行するソフトウェアとハードウェアが複雑になるにつれて、ますます注目されています。

Carina氏は、AGIには検証された生成が必要だと強く信じており、「他に可能な未来はない」と断言しています。

生産にはコストがかかり、検証には安価

Leanの証明は生成が難しいですが、正しいかどうかを簡単に示すことができます。しかし、作成した証明が関心のある問題に正しくマッピングされていることをどうやって知るのでしょうか？Carina氏が言うように、「指定できるものはすべて証明できます。人間は、望むすべてを指定するのが苦手です。」

私たちは今、指定ビジネスにいるのでしょうか？Carina氏の見解を聞くには、エピソードをご覧ください。また、次の内容も含まれています：

ハードウェア検証がキラーアプリである理由

AXLEオープンAPIと最近リリースされたDiscoveryツールキットの詳細

Erdos論争

OpenAI GPT-fディアスポラ

完全なビデオポッドキャスト

タイムスタンプ：

0:00 イントロ：2億ドルのシリーズAと数学スタートアップのテーゼ

4:52 検証型AI：ブリリアンスのスケーリング、粗雑さの修正ではない

13:42 Axiomのシステム：Leanデータ、RL、Putnam完全スコア

22:12 数学的発見 — 予想の前に

25:12 Riceの定理、不完全性、実用的限界

30:42 コードと証明 — Verinaベンチマーク

37:57 証明木、コンテキストウィンドウ、スケーリング限界

43:57 市場、堀、ビジネスケース（16億ドル評価）

55:27 個人の起源：オックスフォード、UCLギャツビー、スタンフォードロースクール

1:00:57 Erdos論争と探索の難しさ

1:06:02 数学のAlphaZero、自己改善

1:08:47 スタートアップの優位性とOpenAI GPTFスレッド

1:13:17 Axle API — Leanのためのスケーラブルなオープンインフラ

1:20:47 コラボレーション、Polymath、人間の注意がボトルネック

1:22:21 創業の物語 — 執着、ロースクール、Julie Zhuo

1:26:17 より大きなビジョン — AGI、科学、転移学習

1:35:02 ボトルネック、断片化、分野の未来