非公式 AI の限界を超える - Carina Hong, Axiom Math

2025 年、設立から 7 ヶ月しか経っていないスタートアップである Axiom は、権威ある学部生向け数学試験であるプットナム試験（Putnam exam）の全 12 問を解決しました。制限時間内に 8/12 のスコアを獲得したのです。この 12/12 という得点は、上位の学部生たち（110/120）や結果を発表した最も近い AI システム（DeepSeek 103/120）よりも優れていますが、もし時間制限がなければ人間や他のシステムがどの程度のスコアを出せたかは不明です。しかしながら、プットナム試験はその難易度で伝説的な地位を築いており、通常は中央値の得点が 0 または 1 点に過ぎません。これ単独で見れば、これは AI の功績の一つとしてさほど大したものではありません。カスパロフを破ったディープブルー（Deep Blue）から始まる、人間とのエリート競技における AI システムの一連の成果のうちのひとつに過ぎないからです。

時を 2026 年半ばまで進めると、Claude Code や Codex が世界を席巻しています。2024 年当時、コードと企業向け市場への Anthropic の賭けは、より優れたモデルと巨大な消費規模を持つ OpenAI と比較すると、より現実的なニッチ戦略のように見えました。今日では、アモデイ（Amodei）が画像や動画などをお構いなしにコードを通じた加速に全賭けしている姿が、先見の明があったように思えます。

しかし Anthropic の勢いが拡大する中でも、Axiom の CEO である Carina Hong は、コーディング能力は AGI（人工一般知能）への道における必要不可欠ではあるが不十分なマイルストーンであると捉えています。コードは、コーディング以外のいくつかの領域において、その荒々しいフロンティアをスーパーインテリジェンス（超知能）のレベルまで押し上げる可能性がありますが、Carina はそこに AI の進展をボトルネックにする驚くべきギャップが存在すると信じています。（数学ベンチマークに関する統計データあり）

非公式なボトルネック

「検証済み AI」という言葉は、ブロッコリーを食べたり税金を納めたりするようなもののように聞こえるかもしれませんが、Axiom にとっては全く異なる意味を持ちます。「私にとっての検証とは、卓越性の拡大と、その卓越性を複利化することです」と Carina は語りました。

実際には、彼女が何を言っているのかを理解するのに少し時間がかかりました（最初はマーケティング用語にしか聞こえなかったのですが、ふと納得した瞬間がありました）。Carina はこの点を説明するために、伝説の数学者スリニヴァーサ・ラマヌジャン（「無限を知る男」）を取り上げます。G.H. ハーディがついにラマヌジャンを説得して、頼りきりの（しかし恐るべき）直感に依存するのではなく、定理の形式的証明を行うようにさせたとき、それは彼の自身の能力を向上させたと伝えられています。おそらく、何かを形式的に証明することが、ラマヌジャンに新しい思考の道を開くような形で詳細を言語化することを強いたからでしょう。これが数学における「複利化」の方法です——不安定な基盤ではなく、堅固な基盤の上に築き上げるのです……つまり、公理（Axioms）と呼ばれるものです。

しかし、何かを形式的に証明することは、他の人々が彼の直感から恩恵を受けることも可能にしました：証明とは、直感を伝達し、その直感が正しいと他者を説得するための手段です。これが拡大（より多くの人々が結果を利用する）であり、複利化（人々が彼の業績から学び、それを基盤として構築できる）です。

これが、Axiom が取り組んでいるアプローチを理解させる核心的な洞察です。

検証済み生成

検証済み AI は、トレーニングと推論の 2 つの形で現れます。

ただし、少し立ち止まって考えてみましょう：第一近似として、「形式検証」とは、Lean2 などの言語で綿密に指定された数学的証明を、型チェッカー（TypeScript、C++、または Rust のようなものですが、より高度な機能を持つ）を用いて検証することを意味します。"非公式"の証明（ただし、ほとんどの人がそれを「非公式」とは呼ばないでしょう）を Lean による証明に変換するには、多大な労力が必要です。Axiom 自体も、数学的証明を検証・検証・操作するための対話型 Lean アプリケーションであるツールキット AXLE をオープンソース化し、画期的な成果を発表しています。

これは強化学習（Reinforcement Learning）において非常に（そして極めて）有用であることが想像できます：統計に基づく最善の推測（GRPO、RLHF など）に頼るのではなく、Lean 検証器を用いて証明が正しいことを直接確認できるからです。これは明らかに、はるかに強力な報酬信号であり、コードをコンパイルしてテストする行為（コーディングにおける強化学習で通常行われること）に似ています。

しかし、落とし穴があります：LLM は現在、Lean を用いた証明にはあまり得意ではありません。

ここに Axiom が登場します：彼らは 12/12 の Putnam 結果以外について公式にベンチマーク数値を発表していませんが、Carina によると、Verina コード生成ベンチマークにおいて ProofGen で非常に印象的な 99%（187/189）を達成しています。このベンチマークは、一連の問題に対してコードとその正しさの証明を生成するものです。参考までに、OpenAI o3（現時点で知られている最新の OpenAI の実行結果）はこのベンチマークで 4.9% を記録しました。

限定的なベンチマークに基づくと、年間の IMO（国際数学オリンピック）の目標以外で最前線のラボが現在どのように取り組んでいるかを言うのは難しいですが、Carina によれば、彼らはまだ Lean 証明を直接生成するために訓練しているわけではなく、非形式的な証明に依存しているとのことです。

このギャップを埋めるために最前線のラボの現在のアプローチが有効かどうかは、時間の経過によって明らかになるでしょう。

スケーリングと複利効果

Carina のラマヌジャンのアナロジーは非常に直接的です。より良い証明 → より良い Lean 生成 → より良い強化学習（RL）。より強力なシグナルとは、サンプル効率の向上と最大性能の高まりを意味します。素晴らしいことです。

スケーリングについても明確です。一度 Lean で何かを証明すれば、出力の品質は人間から得られた場合とほぼ同等に高くなるため、非形式的なロールアウト・コーパスでは不可能な形で、高品質なトレーニングセットが成長したことになります。私は Lean 証明を信頼できます。

複利効果についても同様です。これからは、将来の推論も訓練も、これらの証明の上に構築されていくことになります。

一方で、強化学習中に GRPO のような統計的シグナルのみを使用して訓練されたモデルは、形式検証を利用するシステムが享受できるサンプル効率、最大性能、そして複利効果をもたらすコーパスを欠いています。

すべての道は検証へと至る

ブロッコリーや税金の問題はさておき、検証というテーマは私たちの会話の多くで登場しています。物理システムの分野では、Applied Intuition の事例を思い出してください。

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

理論物理学の分野では、アレックス・ルプサスカ（Alex Lupsasca）の言葉を思い出します。

「…今や、ChatGPT に同時に数千問の質問を処理させることができるこの段階に至りました。すると、それらのかなりの割合に対して証明が返ってきます。実際、すべての出力を検証する責任は再び人間に戻ってきました。そして、それがボトルネックとなるにつれて、数学の形式化と検証の自動化がより価値を持つようになると思います。」

実際、科学のための AI と計算のための AI の決定的な違いは検証にあります：科学では、物理実験を実行して仮説を実際にテスト（検証）する必要があります。Radical AI や Lila などの「Lab in the loop」システムは、まさにこの前提に基づいて構築されています（これらのチームとのエピソードを録画しており、近日公開予定です！）。

また、飛行制御、原子力発電所、ペースメーカーといった重要なシステムの形式検証も、それらを動かすソフトウェアとハードウェアが複雑化するにつれて、注目を集める分野となっています。

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

生成には高コストがかかるが、検証は安価である

Lean による証明の生成は困難ですが、その正誤を簡単に検証することは可能です。しかし、あなたが作成した証明が、あなたが関心を持つ問題に正確に対応していることをどうやって知るのでしょうか？Carina の言葉で言えば：「指定可能なものはすべて証明可能である。人間は自分が望むものをすべて指定するのが苦手だ。」

私たちは今や仕様のビジネスにいるのでしょうか？Carina の見解を聞くにはエピソードをチェックしてください。また、以下の点についても触れられています：

なぜハードウェア検証がキラーアプリとなるのか

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

Erdos 事件の顛末

OpenAI GPT-f のディアスポラ（離散）

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

タイムスタンプ：

0:00 イントロダクション：2 億ドルシリーズ A と数学スタートアップの仮説

4:52 検証済み AI：輝きのスケーリング、不備の修正ではない

13:42 Axiom のシステム：Lean データ、強化学習（RL）、そしてプットナム満点

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

25:12 ライスの定理、不完全性、および実用的な限界

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 コラボレーション、ポリマット（多面手）、そしてボトルネックとしての人間の注意

1:22:21 創業ストーリー：執念、法科大学院、そして Julie Zhuo

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

1:35:02 ボトルネック、分断、そして分野の未来

1 私は実はブロッコリーが大好きですが、同時にテスト駆動開発（Test Driven Development）を強く信じているので ¯\(ツ)/¯

2 形式検証には、モデル検査（TLA+、SPIN）、SMT ベースのツール（Dafny、F*、Why3）、およびリファインメント型システム（Liquid Haskell）も含まれます。これらは多くの場合、ユーザーの視点からは「証明のタイプチェック」のように見えませんが、その背後には類似した論理的な核が存在します。また、純粋な数学だけでなく、ソフトウェアとハードウェアの正しさにも適用されます。

3 これは控えめな表現です。形式化が非常に困難であるため、ほとんどの定理は非公式のまま残されています。最も重要な証明を形式化しようとする多大な努力が払われてきましたが、その結果は様々でした。

4 証明が LLM の分布内にあるという点から、少し低くなる可能性もあると主張する人もいるかもしれません。