大規模言語モデル(LLM)が世界を席巻する中、その根源的な課題である「推論の不確実性」に正面から挑むスタートアップが、静かにその姿を現した。数学に特化したAIの研究開発を行うAxiom Quant(通称:Axiom Math)である。同社は2025年10月2日、B Capitalが主導するシードラウンドで6,400万ドル(約96億円)の資金調達を完了し、企業評価額が3億ドル(約450億円)に達したことを発表した。このニュースは、AIの進化が次に目指すべきフロンティア、そして「知性」そのものの未来を占う、極めて重要な意味を持つ物と言える。なぜ今、「数学」がAI開発の最前線なのか。Axiomは、OpenAIやGoogleといった巨人たちと何が決定的に違うのだろうか。

AD

突如現れた「AI数学者」、Axiomが示した巨大なポテンシャル

今回発表された資金調達は、その規模と参加した投資家の顔ぶれから、Axiomへの期待の高さがうかがえる。リードインベスターのB Capitalに加え、Greycroft、Madrona Ventures、Menlo Venturesといった有力ベンチャーキャピタルが名を連ねた。

Axiomが目指すのは、単に計算が得意なAIではない。「AI数学者」とでも言うべき、自律的に思考し、新たな知識を創造するシステムの構築である。 具体的には、世界の数学の教科書、学術論文、科学ジャーナルを統合した高度なソフトウェアを開発し、それを用いて人間がまだ解き明かしていない、あるいは存在すら知らない「新しい数学の問題」を自ら生成し、その解を「検証可能な証明」と共に提示することを目指している

これは、現在のAI技術の延長線上にあるようでいて、実は全く異なるパラダイムへの挑戦だ。ChatGPTのような生成AIは、膨大なテキストデータから統計的な正しさに基づき、もっともらしい文章を生成することはできる。しかし、その推論プロセスはブラックボックスであり、論理的な破綻や事実に基づかない情報(ハルシネーション)を生み出すことが少なくない。Axiomが目指すのは、思考のすべてのステップを厳密な論理で検証し、「絶対に正しい」と証明できるAIなのである

なぜ今「数学」なのか? 巨大ITが直面するLLMの根源的課題

このAxiomの挑戦を理解するためには、まず現在のLLMが抱える根本的な課題に目を向ける必要がある。LLMは言語の領域で驚異的な能力を発揮したが、その成功の裏で「信頼性」という壁に突き当たっている。

投資家であるB Capitalのパートナー、Ida Girma氏は、「言語モデルは驚くべき結果を生み出すが、その推論プロセスにおけるエラーのために依然として極めて予測不可能である」と指摘する。 特に、金融、航空宇宙工学、半導体設計、創薬、ソフトウェア検証といった、わずかなエラーも許されないクリティカルな領域において、現在のLLMを全面的に信頼することはできない。ブラックボックス化されたAIが導き出した結論を、我々は鵜呑みにするしかないからだ。

ここで「数学」が重要な意味を持つ。数学は、曖昧さを排した厳密な論理と証明によって成り立つ、人類の知の体系である。Axiomの共同創業者であるCarina Hong氏は、「数学は、超知性を構築するための完璧なサンドボックス(実験場)だ」と語る。 つまり、絶対的な正しさが定義できる数学の領域で「証明可能な推論能力」を持つAIを開発できれば、その技術を他のあらゆる科学・工学分野に応用できる可能性があるのだ。数学は、AIが信頼性を獲得するための、いわば究極の訓練場なのである。

AD

創業者Carina Hong氏の異才と、ドリームチームの結成

Axiomのビジョンを牽引するのは、共同創業者兼CEOのCarina Hong氏、24歳。彼女の経歴は、まさに「天才」と呼ぶにふさわしい。

マサチューセッツ工科大学(MIT)で数学と物理学の学士号を取得し、在学中に9本以上の研究論文を執筆。その後、オックスフォード大学で修士号を取得した。2023年には、優れた数学研究を行った学部生に贈られる、極めて権威ある賞「Frank and Brennie Morgan Prize」を受賞している。 整数論、組み合わせ論、理論計算機科学、確率論といった幅広い分野で実績を残す、世代を代表する数学者の一人と目されている。

もう一人の共同創業者でCTOを務めるのが、Shubho Sengupta氏だ。彼はMeta Platforms(旧Facebook)のAI研究者として、同社のLLM「Llama」の開発やソフトウェアテストに貢献した人物である。 それ以前はGoogle Brainの分散学習システムや、NVIDIAでの初期のCUDA開発にも携わっており、AIと大規模計算技術の最前線でキャリアを積んできた。

二人の出会いは、スタンフォード大学近くのコーヒーショップだったという。AIと数学の交差点について何時間も語り合った末に、彼らは専門分野に特化したAIモデルを自ら作ることを決意。これがAxiomの原点となった。

さらに、Axiomには世界トップクラスの才能が集結している。2019年からトランスフォーマーを複雑な数学問題に応用する研究の先駆者であり、最近100年来の未解決問題を解決したFrançois Charton氏や、コンパイラやGPUコード生成に初めてLLMを応用するなど、深層学習を用いたコード生成の第一人者であるHugh Leather氏もチームに加わっている。 まさに、数学とAIの頂上知性が融合したドリームチームと言えるだろう。

Axiomの独自アプローチ:「証明」を学習するAIは如何にして可能か

では、Axiomは具体的にどのようにして「証明可能なAI」を実現しようとしているのか。その鍵は、彼らのユニークなアプローチにある。

B Capitalのブログによれば、Axiomは「Lean」と呼ばれる特殊なプログラミング言語と、高度な数学的証明を、AIの訓練データとして活用する。 Leanとは、数学的な定理を形式的に記述し、その証明が論理的に正しいかをコンピューターが厳密に検証できる「証明支援システム」の一種だ。

従来のAIが、ウェブ上の玉石混交のテキストデータを学習するのとは対照的に、Axiomは人類の知の結晶であり、かつ論理的に完璧であることが保証された「数学的証明」そのものを学習させる。これにより、AIは単語の並びの確率を学ぶだけでなく、厳密な論理構造と推論の進め方を根本から理解することが可能になる。

このアプローチから生まれるのは、「検証済みの定量的推論」の基盤である。 AIが導き出した答えのすべてのステップが、数学的に「証明可能」となる。結果として、自己改善能力を持つ推論エンジン、すなわち「AI数学者」が誕生するというのがAxiomの構想だ。

AD

巨人たちとの競争:OpenAI、Google DeepMindとの決定的な違い

数学AIの分野では、Axiomが初めてではない。OpenAIやGoogleのDeepMindといった巨大IT企業も、この分野で驚異的な成果を上げている。両社は、数学の才能を持つ人間でさえ苦戦する国際数学オリンピック(IMO)において、6問中5問を解決できるAIシステムを開発したと報じられている。

しかし、Axiomのアプローチがこれらの巨人たちとは戦略的に一線を画すと見ている。OpenAIやGoogleの目標が、主に「人間が作成した既存の難問を“解く”」というパフォーマンスの向上にあるのに対し、Axiomはさらにその先を見据えている。彼らの目標は、「AIが自ら新しい理論を提唱し、それを“証明”することで、全く新しい知識を“創造”する」ことにあるのだ。

これは単なる性能競争ではない。AIを知的作業の「ツール」として使うのか、それとも未知の領域を探求する「パートナー」へと昇華させるのかという、AIの役割そのものを問うパラダイムの競争である。Axiomが成功すれば、AIは人間の知識を整理・応用する存在から、人間の知性の限界を突破し、新たな発見をもたらす存在へと変貌を遂げる可能性がある。

「数学の証明」から始まる産業革命:Axiomが見据える未来

Axiomの挑戦は、アカデミアの世界に留まるものではない。彼らの技術が確立されれば、その応用範囲は計り知れない。

  • 金融サービス: 定量的取引(クオンツトレーディング)において、市場の非効率性を見つけ出す新たなアルファ(収益機会)を発見・証明するアルゴリズムを開発する。
  • 工学・設計: 航空機や次世代半導体の設計において、シミュレーションの精度を極限まで高め、最適な設計を導き出す。
  • ソフトウェア開発: ソフトウェアやプロトコルの論理的な正しさを形式的に検証し、潜在的なバグや脆弱性を根絶する。
  • 科学研究: 物理学、生物学、化学などの分野で、複雑な現象を支配する数理モデルを構築し、新たな科学的発見を加速させる。

これらの分野に共通するのは、「絶対的な信頼性」と「論理的な正しさ」が不可欠であるという点だ。B CapitalのGirma氏が述べるように、「ブラックボックスの推論は、いかに説得力があっても、これらの領域における重大な意思決定を方向づけるために完全には信頼できない」。 Axiomが開発する「証明可能なAI」は、まさにこのニーズに応えるものであり、数兆ドル規模の市場に破壊的な変革をもたらすポテンシャルを秘めている。

Axiomが投じる一石は、AIの未来をどう変えるか

Axiom Mathの登場は、AI開発の歴史における一つの転換点となるかもしれない。これまでのAIが「帰納的」にデータからパターンを学習してきたのに対し、Axiomは「演繹的」に論理から結論を導き、その正しさを証明しようとしている。

この挑戦は、AIを単なる「博識なアシスタント」から、真に新しい知識を発見し、人類の知の地平を切り拓く「創造的なパートナー」へと進化させる壮大な試みである。成功への道のりは決して平坦ではないだろう。しかし、もしAxiomがそのビジョンを実現したならば、科学技術の進歩は非連続的な加速を遂げ、これまで人類が何世紀もかけて解き明かしてきた難問が、次々と解決される時代が到来するかもしれない。

Axiomが投じた一石は、静かに、しかし確実にAI業界全体に波紋を広げている。「証明可能な知性」という概念は、今後のAIのあり方を定義する上で、中心的なテーマとなっていくに違いない。


Sources