AI業界が生成AIの流暢な「会話力」に沸く一方で、その根源的な課題である「ハルシネーション（幻覚）」、すなわちAIがもっともらしい嘘をつく問題に正面から挑むスタートアップがある。カリフォルニア州パロアルトを拠点とするHarmonic AIだ。同社は2025年7月10日、シリーズBラウンドで1億ドル（約145億円）の資金調達を実施したと発表した。これにより、同社の評価額は8億7500万ドル（約1290億円）に達した。
これは、現在のAI開発の主流である大規模言語モデル（LLM）とは一線を画す、「数学的真実」に基づくAIの可能性に、シリコンバレーのトップ投資家たちが大きな賭けをしたことを意味する。Harmonicが掲げる「Mathematical Superintelligence（数学的超知能）」は、AIの未来を左右するもう一つの重要な潮流となるのだろうか。
評価額9億ドル、シリコンバレーの賢者が賭ける「数学の力」
今回のシリーズBラウンドを主導したのは、GoogleやAmazonへの初期投資で知られる名門ベンチャーキャピタル、Kleiner Perkinsだ。さらに、暗号資産分野に強いParadigm、FinTech分野のRibbit Capitalに加え、既存投資家であるSequoia CapitalやIndex Venturesといった錚々たる顔ぶれが参加した。
Harmonicは、オンライン証券プラットフォームRobinhoodの共同創業者兼CEOであるVlad Tenev氏と、AIエンジニアのTudor Achim氏（現Harmonic CEO）によって2023年に設立された。設立からわずか2年足らず、2024年9月のシリーズA（7500万ドル）に続く今回の大型調達は、同社のビジョンと技術に対する市場の並外れた期待を物語っている。
調達した資金は、同社のフラッグシップモデルである「Aristotle」の開発加速と商業化に充てられる。Aristotleは、確率論的な推測に頼るLLMとは根本的に異なり、数学的な「形式的検証」を用いて、その出力が絶対に正しいことを保証するAIだ。
Kleiner Perkinsのパートナーであり、元物理学者のIlya Fushman氏は、「Harmonicは、信頼性が絶対的に求められる環境で信用できる、検証可能でスケーラブルな推論のための新しい基盤を創造した」と述べ、Harmonicの取締役にオブザーバーとして加わる。物理学のバックグラウンドを持つ投資家が参画することは、Harmonicの技術がソフトウェアの世界に留まらず、科学や工学といった基礎分野の進歩を加速させる可能性を秘めていることへの強い期待の表れと言えるだろう。
なぜ今「数学」なのか？LLMの致命的欠陥とAristotleの誕生
今日のAIブームを牽引するのは、OpenAIのGPTシリーズやGoogleのGeminiに代表される大規模言語モデル（LLM）だ。これらは人間のように自然な文章を生成し、要約や翻訳、創造的なテキスト作成までこなす。しかし、その能力の源泉は「確率」にある。膨大なテキストデータを学習し、次に来る単語として最も確率の高いものを予測し続けることで、流暢な文章を紡ぎ出しているに過ぎない。
この仕組みが、LLMの避けられない欠陥「ハルシネーション」を生む。事実と異なる情報を、あたかも真実であるかのように生成してしまうのだ。一般的なチャットや文章作成では許容されるかもしれないが、その応用範囲が広がるにつれて、この問題は致命的となる。
Harmonicが挑戦しているのは、まさにこの点だ。同社が開発する「Mathematical Superintelligence（MSI）」は、確率的な「もっともらしさ」ではなく、数学的な「証明可能性」に立脚する。
HarmonicのCEO、Tudor Achim氏は次のように語る。
「AristotleのMSIは、エラーの余地が全くないミッションクリティカルなアプリケーションに独自に適しています。例えば、検証済みのソフトウェアを生成したり、既存のコードを形式的に検証したりすることです。これはブロックチェーン、金融サービス、航空宇宙、その他安全性が重視されるシステムにとって画期的なことです」
つまり、曖昧さを許容する「言語」の世界ではなく、真偽が明確に定まる「数学」の世界でAIを思考させることで、100%の信頼性を担保しようというアプローチなのである。
Aristotleを支える技術：自己進化する「証明マシン」
では、Harmonicはどのようにしてこの「数学的超知能」を実現しようとしているのか。その核心には、二つのユニークな技術戦略がある。
一つは、「Lean 4」という証明支援系の活用だ。証明支援系とは、数学的な定義や定理、そしてその証明過程を、コンピュータが厳密にチェックできる形式で記述するためのプログラミング言語のようなものである。Aristotleは、自然言語で書かれた数学の問題をこのLean 4の形式に翻訳し、その証明を生成・検証する。これにより、出力された解が論理的に一貫し、数学的に正しいことを保証できる。
もう一つは、その訓練データの生成方法だ。LLMがインターネット上から無差別に収集したデータに依存するのに対し、Harmonicは異なる道を選んだ。Aristotleは「合成データ」を自ら生成して学習するという。具体的には、形式的に正しい「問題と証明のペア」を自律的に作り出し、それを解くことで能力を高めていく。この「自己対戦（self-play loop）」のような再帰的な自己改善プロセスにより、単純な問題から始め、徐々に国際数学オリンピックレベルの高度な定理の証明まで、その能力をスケールさせることが可能になるという。
このアプローチは、Webスクレイピングに起因するノイズやバイアス、著作権といった問題を回避できるだけでなく、AI自身が純粋な論理空間の中で無限に学習を続けられる可能性を示唆している。実際に、Aristotleは標準的な数学推論ベンチマーク「MiniF2F」において、既に90%という極めて高い成功率を達成していると報告されている。
狙うは「信頼性」が命の市場：金融から物理学の未解決問題まで
HarmonicがAristotleで見据える市場は明確だ。それは、わずかなエラーが致命的な結果を招く「高信頼性」が求められる領域である。
- ブロックチェーン: スマートコントラクトのバグは、巨額の暗号資産の盗難に直結する。Aristotleを使えば、コントラクトのコードに脆弱性がないかを形式的に検証できる可能性がある。
- 金融サービス: 金利計算やリスク評価モデルにおけるわずかなミスも許されない。検証済みのアルゴリズムは、金融システムの安定性に大きく貢献するだろう。
- 航空宇宙・防衛: 航空機の制御システムやミサイルの誘導システムなど、人命に関わるソフトウェアの信頼性確保は最優先課題だ。
これらは、現在の生成AIが最も苦手とする分野であり、Harmonicの明確な差別化戦略と商業的可能性がここにある。
さらに、共同創業者であるVlad Tenev氏は、その先にある壮大なビジョンを語る。「数学を加速させることで、理論物理学や工学といった、数学に依存する複数の分野でブレークスルーを推進する扉が開かれる」。未解決の数学の定理を証明するだけでなく、物理学やコンピュータサイエンスの根本的な問題にまで挑む。これこそが「Mathematical Superintelligence」が目指す最終地点なのかもしれない。
Tenev氏の「AIモデルを構築する上で、すべての出力と推論のすべてのステップが検証可能に正しいことを保証できる。これこそが、将来主流となるアプローチだと私は考えている」という言葉は、現在のAI業界の熱狂に対する、冷静かつ力強い宣言と言えるだろう。
AIはどこまで「思考」し、どこまで「信頼」できるのか。HarmonicとAristotleの挑戦は、その根源的な問いに、「数学」という人類で最も厳密な言語で答えようとする、壮大な実験の始まりなのである。
Sources