🔬スケーリングを超えて：インフォーマルAIの先へ - Carina Hong, Axiom Math

2025年12月、創業からわずか7カ月のスタートアップAxiomが、米国の大学学部生向け最高峰の数学競技であるWilliam Lowell Putnam Mathematical Competition（パトナム競技）で満点（120点中120点）を獲得した。このスコアは、最高の人間の成績（110点）や、DeepSeekの103点を上回るものであり、AIが「超人的」数学能力を示した画期的な瞬間として業界に衝撃を与えた。AxiomのCEOであるCarina Hong（カリーナ・ホン）は、この成果を「検証されたAI（Verified AI）」というビジョンの第一歩と位置づける。彼女の主張は明確だ。AIの推論能力を真にスケールさせ、複雑な問題に対して信頼性の高い回答を生成するためには、単なる統計的な強化学習（RL）ではなく、Leanのような形式検証言語を用いた「証明」が不可欠であるという。これは、AIの「幻覚（hallucination）」を防ぐための消極的な対策ではなく、AIの「 brilliance（ brilliance ）」を増幅し、蓄積するための積極的な戦略である。

本エピソードでは、Carina Hongが、Axiomの技術的優位性、形式検証がもたらす「サンプル効率」と「性能向上」のメカニズム、そしてこの技術がコード検証からハードウェア検証、さらにはAGI（汎用人工知能）に至るまで、どのように応用されうるのかを詳細に語った。彼女は、伝説的な数学者ラマヌジャンの逸話を引き合いに出し、直感だけに頼っていた天才が「証明」という形式を身につけることで、その能力が飛躍的に「スケール」し「複利」のように成長したと説明する。Axiomのビジョンは、AIにこの「証明」の力を与えることにある。同社はシリーズAで2億ドル（約300億円）を調達し、評価額は16億ドルに達した。この巨額の資金は、形式検証という「地味で面倒な」分野に革命を起こそうとする同社への市場の期待の大きさを示している。

0:00検証されたAI：ブロッコリーではなく、 brilliance のスケーリング

Carina Hongは、形式検証（Formal Verification）に対する一般的な認識を真っ向から否定する。多くのエンジニアや企業は、形式検証を「面倒なブロッコリー」や「税金の支払い」のように捉え、安全性が求められる一部の閉じた産業（航空宇宙、軍事など）のためのものだと考えている。しかし、彼女にとってそれは全くの誤解である。「検証とは、 brilliance（ brilliance ）をスケールさせ、複利のように成長させることだ」と彼女は断言する。彼女は、この考え方を説明するために、数学者ラマヌジャンの物語を用いる。ラマヌジャンは驚異的な直感で数々の公式を発見したが、ケンブリッジでG.H.ハーディのもとで正式な証明を書くことを学んだ後、さらに強力な数学者へと成長した。証明を書くという行為は、彼自身の思考を明確にし、新しい発想を生み出す助けとなった（複利効果）。そして、証明された定理は他の数学者によって利用され、その上に新しい理論が構築されることで、彼の brilliance は時間と空間を超えてスケールした。

このラマヌジャンのアナロジーは、Axiomの技術戦略を完璧に体現している。Axiomが目指すのは、AIが生成した証明をLeanのような形式言語で検証し、その正しさを保証することだ。この「検証された生成（Verified Generation）」は、AIのトレーニングと推論の両方において革命的な意味を持つ。トレーニングにおいては、RLHF（人間のフィードバックからの強化学習）やGRPO（グループ相対方最適化）のような統計的な報酬信号の代わりに、Leanの検証器が「正しいか間違っているか」という決定的な報酬を提供する。これは、コードをコンパイルしてテストするのと同様に、はるかに強力でサンプル効率の高い学習を可能にする。Carinaはこれを「検証された生成による性能向上」と呼び、少ない計算リソースとデータで、フロンティアラボに匹敵する、あるいは凌駕する性能を達成できると主張する。

12:34Leanという言語：証明であり、コードであり、コラボレーションツール

Leanは、数学の証明を記述するための形式言語であり、同時にチューリング完全な関数型プログラミング言語でもある。Carinaは、Leanの真の価値は、その二面性にあると説明する。数学者にとってLeanは、低レベルの計算や退屈な推論を自動化する「tactic（タクティク）」を提供し、人間がより高次の直感的な思考に集中することを可能にする。これは、証明の正しさを保証するだけでなく、数学者の創造性を拡張するツールとして機能する。さらに、Leanはコラボレーションのプラットフォームとしても重要だ。著名な数学者テレンス・タオも指摘するように、Leanを使えば、数学者は互いの証明を正確に理解し、大規模なプロジェクトで協力することができる。Axiomは、この「コラボレーションのためのツール」という側面を強く重視している。

Axiomは最近、Leanのための検証・操作ツール群「Axle（Axiom Lean Engine）」をリリースした。Axleは、証明の検証（Verify Proof）を100倍高速化するだけでなく、壊れたLeanコードの修復など、14のツールを提供する。Carinaは、このツールをClaude Codeと組み合わせて使うユーザーが増えていると述べ、形式検証の民主化を推進している。彼女は、Leanが「コード」と「証明」を統合する言語である点を強調する。Axiomが取り組んでいる「コード検証」ベンチマーク（Verina）では、99%（189問中187問）という驚異的なスコアを達成した。これは、OpenAI o3の4.9%を大幅に上回る。この結果は、Leanを用いたコードと証明の同時生成が、従来の手法よりもはるかに効果的であることを示している。

24:00理論的限界と現実的な戦略：ライスの定理と「sorry」の活用

形式検証には、ライスの定理やゲーデルの不完全性定理といった理論的な限界が存在する。すべてのプログラムを検証することは不可能であり、検証可能な問題と不可能な問題が存在することは理論的に証明されている。しかし、Carinaはこの理論的限界に対して実践的な立場をとる。「理論が何を教えてくれるか？それは、私たちが限界まで挑戦することを止めさせないということだ」と彼女は語る。Axiomの目標は、すべてのプログラムを検証することではなく、有用なプログラムの大部分を検証できるようにすることだ。彼女は、MITのマスコットが言ったという逸話を引用し、理論的な制約に臆することなく、可能な限り押し進めることの重要性を強調する。

Axiomの戦略は、問題を「検証可能な小さな部品」に分解することにある。これは、Leanの「sorry」というタクティクを戦略的に活用することで実現される。「sorry」は、証明の一部を未証明のまま仮定として受け入れるための命令だ。例えば、複雑なシステム全体を一度に検証するのではなく、「このモジュールが正しいと仮定すれば、システム全体は正しい」という形で、検証の範囲を限定することができる。そして、その「sorry」とされた部分を、Axiom Proverが後から証明する。このアプローチにより、理論的に検証が不可能な巨大なシステムであっても、実用的なレベルで信頼性を高めることが可能になる。Carinaは、この「分解と証明」のサイクルこそが、将来のコーディングの姿だと予測する。AIがコードの大枠を生成し、Axiomがその重要な部分を検証するという分業体制が、ソフトウェア開発の新しい標準になると彼女は考えている。

45:55ビジネスモデルと市場：ハードウェア検証からエージェントまで

2億ドルのシリーズAを調達したAxiomのビジネスモデルは、形式検証の「TAM（Total Addressable Market）」をいかに拡大するかにかかっている。Carinaは、第一の市場として「ハードウェア検証」を挙げる。特にASIC（特定用途向け集積回路）の設計検証は、業界標準として「設計：検証」の人員比が1:3から1:4にも上る巨大な市場だ。GPUのような複雑なハードウェアでは「ほぼ正しい」では許されず、完全な検証が必須である。Axiomの検証技術は、この分野で大きなコスト削減と期間短縮をもたらす可能性がある。第二の市場は「ソフトウェア検証」だが、Carinaはすべてのコードが検証を必要とするわけではないと認める。個人のウェブサイトや簡単なアプリケーションには、形式検証は過剰だ。

しかし、彼女は「エージェントの時代」において、検証の重要性が飛躍的に高まると予測する。自律的に行動するAIエージェントが、企業の重要な業務や規制対象のプロセスを実行するようになれば、その行動の正しさを保証する必要が出てくる。例えば、AIエージェントが誤った取引を実行したり、機密情報を漏洩したりするリスクを、形式検証によって軽減できる可能性がある。Carinaは、Axiomの究極のビジョンは「すべてのAI生成コードに対する第一拒否権（right of first refusal）」を持つことだと語る。つまり、AIがコードを生成した際に、そのコードを検証するかどうかの選択権をAxiomが持つという立場だ。これは、検証が単なるコストではなく、品質と信頼性を保証するための不可欠なサービスになるという彼女の確信に基づいている。

1:00:41不確実性との戦い：エルデシュ問題の教訓とプロvenanceの重要性

Axiomは、その輝かしい成果の一方で、痛恨のミスも経験している。同社は、競合他社が解いたと主張する未解決問題（エルデシュ問題）を自社のシステムで再現しようと試みた。そして実際に解くことに成功したが、後にその問題が過去に既に解決済みであったことが判明した。これは、文献調査の不備によるものであり、Carinaは「私たちの落ち度だ」と率直に認める。この経験は、AIが生成した結果の「provenance（来歴、出典）」を確認することの難しさと重要性を浮き彫りにした。数学の世界では、問題が本当に未解決なのか、あるいは別の形で既に解決されているのかを判断することは、驚くほど難しい。特に、エルデシュ問題のように数多くの問題が存在する場合、検索と知識ベースの整備が極めて重要になる。

このエピソードは、Axiomの技術的な優位性だけでなく、その限界と向き合う誠実さも示している。Carinaは、AIが証明を生成したとしても、その証明が本当に求めている問題を解決しているのかを人間が確認するプロセス（「仕様策定」の問題）が、依然として大きな課題であると認める。特に、金融監査や法規制のような分野では、何を「正しい」と定義するか自体が難しい。彼女は、この「仕様策定」の部分では、従来のテストや、突然変異テストに基づくLLMユニットテスト生成のような「インフォーマルな推論」が重要な役割を果たすと指摘する。つまり、形式検証とインフォーマルな推論は対立するものではなく、相互補完的な関係にあるというのがAxiomの現実的な立場だ。

1:14:05フロンティアラボとの差別化：フォーカスとデータのフライホイール

なぜ、OpenAIやAnthropicのような巨大なフロンティアラボではなく、スタートアップのAxiomが形式検証で先行できているのか。Carinaは、その理由を「フォーカス」と「組織のアラインメント」に求める。彼女は、フロンティアラボでは研究の方向性が経営陣の交代や政治的な駆け引きによって頻繁に変わると指摘する。例えば、OpenAIにはかつて形式数学に取り組むチーム（GPT-fなど）が存在したが、主要メンバーは全員退社してしまった。DeepSeekも同様に、形式検証チームを一度解散している。スタートアップは資金調達のプレッシャーにさらされる一方で、一つの問題に長期間集中できるという利点がある。Axiomのチームは、数学のオリンピアンや研究数学者、Mathlib（Leanの数学ライブラリ）の主要コントリビューター、そしてMetaやGoogleからの応用MLの専門家など、異分野のトップ人材が一つのミッションの下に結集している。

このチームの結束力が、Axiomの最大の「moat（参入障壁）」を生み出している。それは、膨大な量の「Leanデータ」である。Axiomのシステムは、自ら生成した証明を検証し、その正しさが保証されたデータを蓄積し続ける。この「検証されたデータ」は、次のトレーニングサイクルで使用され、さらに高性能な証明生成を可能にする。これがCarinaの言う「データのフライホイール」だ。フロンティアラボが持つような無限の計算資源はなくとも、この高品質なデータとサンプル効率の高い学習アルゴリズムによって、Axiomは限られたリソースで超人的な性能を達成できる。Carinaは、フロンティアラボはAxiomと競争するよりも、検証APIとしてAxiomと提携する方が合理的だと提案する。これは、検索APIを提供するPerplexityのようなスタートアップとフロンティアラボの関係に類似している。

結びに

このエピソードは、AIの「推論」と「信頼性」をめぐる議論に、全く新しい視点をもたらした。Carina Hongの「検証とは、 brilliance をスケールさせ、複利のように成長させることだ」というフレーズは、単なるキャッチーな言葉ではない。それは、AIの能力を飛躍的に向上させるための具体的なエンジニアリング戦略であり、同時に、AIが生成する知識に対する人間の関わり方の哲学でもある。彼女は、AIの「幻覚」を防ぐための消極的な手段としてではなく、AIの能力を増幅し、その成果を確実なものとして積み上げていくための積極的な手段として形式検証を位置づけた。この視点の転換は、AIエンジニアにとって非常に示唆に富む。

Axiomの成功は、AIの進化における「データ」と「アルゴリズム」の次に来る重要な要素が「検証」であることを示唆している。特に、コード生成やエージェントシステムが実用化されるにつれて、出力の正しさを保証する仕組みの重要性はますます高まるだろう。Carinaは、この分野が「断片化（fragmentation）」の危険性に直面していると警告する。優秀な人材が小さなスタートアップに分散し、同じ問題に取り組むのではなく、互いに競争している現状を憂慮する。しかし、Axiomのように、明確なビジョンと強力なチームが結集すれば、理論的な限界を超えて、AIの新たなフロンティアを切り開くことができる。このエピソードは、AIの未来は、より多くの計算資源を投じることではなく、より賢い学習と検証の仕組みを構築することにあるという、一つの確固たる信念を私たちに残した。

要点

• Axiomは2025年12月のパトナム競技で満点（120点）を獲得し、最高の人間（110点）やDeepSeek（103点）を上回った。これは形式検証を用いたAIシステムの優位性を示す画期的な成果である。
• CEOのCarina Hongは、形式検証を「面倒な義務」ではなく、AIの「brillianceをスケールさせ複利効果を生む」ための積極的な戦略と定義する。これは、ラマヌジャンが証明を学ぶことでより強力な数学者になった逸話に例えられる。
• Axiomの技術的優位性は、Lean形式言語を用いた「検証された生成（Verified Generation）」にある。これにより、統計的な報酬信号よりもはるかに強力な信号で強化学習を行うことができ、サンプル効率と最終的な性能が大幅に向上する。
• Axiomはコード検証ベンチマーク「Verina」で99%（189問中187問）を達成し、OpenAI o3の4.9%を圧倒した。これは、コードと証明を同時に生成するAxiomのアプローチの有効性を示している。
• 同社はシリーズAで2億ドルを調達し、評価額は16億ドルに達した。主な市場として、ハードウェア検証（ASIC設計など）と、将来的なAIエージェントの行動検証を見込んでいる。
• Carinaは、フロンティアラボが形式検証に本格的に取り組めない理由を「組織のフォーカスの欠如」と説明する。研究の方向性が頻繁に変わる大組織に対し、スタートアップは一つの問題に集中できる利点がある。
• Axiomの最大の参入障壁は、自社システムが生成・検証した膨大な「Leanデータ」の蓄積にある。このデータが次の学習を強化する「フライホイール」を形成し、限られた計算資源でも超人的な性能を可能にしている。
• 同社はLean検証ツール群「Axle」をオープンソース化し、コミュニティとの協業を推進している。Carinaは、検証技術の民主化が、人間とAI、そしてAI同士の新しいコラボレーションを促進すると考えている。