先月、シリコンバレーのAI業界に衝撃を与えた人物がいる。広州市出身の25歳のホン・ルートンさん（洪楽潼、Carina Hong）が創業したAIスタートアップアクシオム（Axiom）が、2億ドル（約318億4,100万円）規模のシリーズA投資を獲得した。
最大手ベンチャーキャピタルのメンロ・ベンチャーズが今回の投資を主導し、グレイクロフト・マドロナ・ベンチャー・Bキャピタル・トヨタベンチャーズなどの既存株主も追加投資に参加した。会社設立から1年足らずで企業価値は16億ドル（約2,547億3,400万円）に達し、世界最年少のユニコーン企業の一つとなった。
6日、中国メディアのフェンメン新聞によると、広州生まれのホンさんは一般家庭で生まれ育ったという。幼少期から数学に並外れた才能を示し、2018年、17歳でMITに入学、数学・物理学の二重専攻を選び、わずか3年で両方の学位を取得した。学部在学中に9本の学術論文を発表し、全米女性数学者最高栄誉のアリス・T・シェーファー数学賞、北米数学学部生最優秀研究賞のAMS-MAA-SIAMモーガン賞を相次いで受賞した。
2021年には世界で最も権威ある国際奨学金の一つ、オックスフォード・ローズ奨学金を受賞し、その年の中国人受賞者4人の一人となった。オックスフォードで神経科学の修士課程中、UCLギャツビー計算神経科学ユニットでディープラーニング研究を始め、AI分野に足を踏み入れた。その後スタンフォードで数学・法学の博士課程を履修中に中退し、起業に踏み切った。
ホンさんが捉えたAI業界の矛盾は明確だった。大規模言語モデルの性能は爆発的に成長するが、信頼性は依然として「闇の中」だという点だ。ホンさんは「日常的な誤りは大きな問題ではないかもしれないが、金融・国防・重要インフラ分野での確率に基づく誤りは災害になり得る」と考えたのだ。
数学用語「公理（Axiom）」から名付けられたこの会社の目標は、AIがコンピュータコードを自動的に検証できるシステムを構築することだ。中核技術は形式化検証で、Leanプログラミング言語を通じて数学的証明を実行可能なプログラムに変換し、結果の正確性を根本的に保証する。大規模モデルが確率で答えを「推測」する代わりに、コードを厳密な数学論理に変換し、全ての推論ステップを決定論的検証器で検証する方式だ。
このシステムの実力はすでに証明されている。2025年12月、米国の大学生数学競技大会であるウィリアム・ローウェル・パトナム数学競技大会でアクシオムの中核システムが12問全てを正解する満点を記録した。100年近い大会の歴史で満点を取った人はわずか5人しかいない。その後、このシステムは複数の未解決整数論の推測も独自に証明した。
会社の始まりは2024年秋、スタンフォード近くのカフェだった。ホンさんはそこで当時、MetaのAI研究統括を務めていたシュボ・セングプタ氏と出会い、数時間の会話の末に起業を決意し、セングプタ氏は現CTOとなった。ホンさんのMIT時代の指導教授である数学界の巨匠ケン・オノ氏もバージニア大学の終身教授職を辞して合流した。現在アクシオムのチームメンバーは20人余りで、その半数がMetaのAI研究所出身だ。
投資家たちの確信も明確だ。メンロ・ベンチャーズのパートナー、マット・クレイニング氏は「AIがほぼ全てのソフトウェアを作成する世界が来ているが、誰も言及しない問題がある。それはそのコードが全く検証されていないということだ」と述べ、「AIがコードを作成し、数学がそのコードの正しさを検証する」と語った。
ホンさんは今後、アクシオムの製品がヘッジファンドやクオンツ運用会社で資産価格の評価、株価予測など複雑な数学問題を迅速に解決するのに活用されると見込んでいる。同分野の競合ハーモニックが最初の数学的マイルストーンを達成するのに2年以上かかったのに対し、アクシオムはそれよりもはるかに早く成果を上げたと自負している。
博士課程も、将来約束された道も捨て、証明の世界から起業の世界に飛び込んだこの天才が数学でAIの信頼性問題を解決できるか、業界の注目が集まっている。
コメント0