AI数学スタートアップのAxiomが、数年から100年以上未解決だった数学の難問4つを解決したと発表。大規模言語モデルと証明検証システムを組み合わせた独自AI「AxiomProver」を開発。数学研究だけでなく、ソフトウェアの信頼性検証など商業分野への応用も期待されています。
AI数学スタートアップAxiom、100年超の未解決問題含む4つの難問を解決
2025年1月、アメリカのAIスタートアップ企業Axiomが、数学の未解決問題4つをAIで解決したと発表しました。解決された問題には、数年前から専門家を悩ませていたものから、伝説的なインド人数学者ラマヌジャンが100年以上前に残した数式に関するものまで含まれています。
Axiomが開発した「AxiomProver」というAIシステムは、大規模言語モデルと数学的証明を検証する専門システムを組み合わせたものです。このシステムは、単に既存の文献を検索するだけでなく、まったく新しい方法で問題を解決し、その証明が正しいかどうかを自動的に検証できます。
数学の分野では、近年AIの能力が急速に向上しています。2024年にはGoogleが同様のシステム「AlphaProof」を発表しましたが、Axiomはさらに進んだ技術を取り入れたと主張しています。この技術は数学研究だけでなく、ソフトウェアの信頼性を証明するなど、サイバーセキュリティ分野への応用も期待されています。
専門家たちは、AIが数学者の「知的パートナー」として新しい発見の地平を開く可能性に注目しています。ハーバード・ビジネス・スクールのスコット・コミナーズ教授は、「完全に自動化され、即座に検証された証明を生み出しただけでなく、その数学の優雅さと美しさにも驚かされる」と評価しています。
解決された4つの未解決問題
Axiomが解決したと発表した問題のうち、最も注目されているのがフェルの予想です。この予想は、シジジーと呼ばれる代数における数式の並びに関するもので、100年以上前にインドの伝説的数学者スリニヴァーサ・ラマヌジャンがノートに残した数式が関係しています。AxiomProverは、この問題について最初から最後まで完全に独力で証明を構築しました。
2つ目の問題は、チェン・ジャンドロン予想と呼ばれるものです。数学者のダウェイ・チェンとクエンティン・ジャンドロンが5年前に代数幾何学の研究中に遭遇した問題で、微分に関する定理を証明する過程で、数論の奇妙な公式が必要になったものの解決できず、予想として論文を発表していました。チェンは何時間もChatGPTに問いかけましたが解決できませんでした。しかし、Axiomの共同創業者である著名数学者ケン・オノに相談したところ、翌朝にはAxiomProverが証明を提示しました。
3つ目の証明は、数論における「行き止まり」の確率モデルに関するものです。4つ目は、数学界で最も有名な難問の一つだったフェルマーの最終定理を解決するために開発された数学的ツールを活用したものです。これらの証明はすべて、学術論文の公開リポジトリであるarXivに投稿されています。
AxiomProverの仕組みと技術的特徴
AxiomProverは、大規模言語モデルとLeanという専門的な数学言語を使った証明検証システムを組み合わせています。Leanとは、数学的証明が論理的に正しいかどうかを厳密にチェックするためのコンピュータ言語です。これにより、AIが生み出した証明が本当に正しいかどうかを自動的に確認できます。
従来のAIチャットボットは、既存の文献を検索して答えを探すことしかできませんでした。しかしAxiomProverは、問題を論理的に推論し、まったく新しい解決方法を考え出すことができます。例えば、チェン・ジャンドロン予想の証明では、19世紀に初めて研究された数値現象との関連性を発見し、それを使って証明を構築しました。オノ教授は「AxiomProverが見つけたのは、すべての人間が見逃していたものだった」と述べています。
2024年にGoogleが発表したAlphaProofも同様のアプローチを取っていましたが、Axiomの最高経営責任者カリーナ・ホンは、AxiomProverにはいくつかの重要な進歩と新しい技術が組み込まれていると説明しています。具体的な技術の詳細は企業秘密ですが、より高度な推論能力と検証能力を持つとされています。
できること・できないこと
AxiomProverにより、専門の数学者でも何年も解けなかった問題を、場合によっては一晩で解決することが可能になります。例えば、チェン教授の問題は5年間未解決でしたが、Axiomに相談した翌朝には証明が提示されました。また、フェルの予想のように、最初から最後まで完全に自動で証明を構築することもできます。数学者は、自分の研究の中で行き詰まった部分をAIに任せたり、新しいアイデアを探索したりする使い方が考えられます。
一方で、AxiomProverはまだ数学界で最も有名な難問や、解決すると賞金が出るような超難問は解けていません。また、AIが生成した証明を人間の数学者が理解し、論文として発表するためには、依然として専門家の協力が必要です。チェン教授もAxiomと協力して証明を論文にまとめました。現時点では、AIは数学者を完全に置き換えるのではなく、強力な補助ツールとして機能しています。
数学以外への応用可能性
Axiomが開発している技術は、高度な数学研究だけでなく、商業的に重要な分野への応用が期待されています。最も有望な応用先の一つがサイバーセキュリティです。ソフトウェアのコードが信頼できるかどうかを数学的に証明することで、特定の種類のサイバー攻撃に対してより強固なシステムを構築できる可能性があります。
現在のソフトウェア開発では、バグや脆弱性がないことを完全に保証することは困難です。しかし、Axiomの証明検証技術を使えば、コードが意図した通りに動作することを数学的に証明できます。これは、金融システムや医療機器、自動運転車など、絶対的な信頼性が求められる分野で特に重要になります。
ホンCEOは「数学は現実世界の偉大な試験場であり、サンドボックスです。商業的価値の高い重要な使用例がたくさんあると信じています」と述べています。Axiomは今後、数学研究での実績を基盤に、こうした実用的な分野への展開を目指しています。
数学研究への影響と専門家の反応
オノ教授は、AxiomProverが単に問題を解くだけでなく、新しい発見がどのように生まれるかという根本的な問いにも光を当てると考えています。「ひらめきの瞬間を予測可能にできるかどうかを理解しようとしています。そして、自分自身がどのように定理を証明してきたかについて多くを学んでいます」と語っています。
実際に自分の予想がAIによって解決されたチェン教授は、AIが数学に与える影響について楽観的です。「電卓の発明後も数学者は九九を忘れませんでした。AIは新しい知的ツール、あるいは『知的パートナー』として、数学研究により豊かで広い地平を開くと信じています」と述べています。
ハーバード・ビジネス・スクールのコミナーズ教授は、「何年もAI数学ツールの進化を注意深く見守り、自分でも使ってきた者として、これは非常に驚くべきことです」と評価しています。特に、完全自動化された証明が即座に検証されるだけでなく、その数学の優雅さと美しさにも感銘を受けたと語っています。
私たちへの影響
このニュースは、数学研究者だけでなく、テクノロジーに関心のある一般の人々にも重要な意味を持ちます。AIの推論能力が急速に向上していることを示す具体的な証拠だからです。
短期的には、数学や科学の研究が加速する可能性があります。これまで何年もかかっていた問題が数日で解決されれば、新しい発見のペースが速まります。また、Axiomのような企業が成功すれば、AI研究への投資がさらに増え、技術開発が加速するでしょう。
中長期的には、ソフトウェアの信頼性向上を通じて、私たちの日常生活に影響が及ぶ可能性があります。銀行のシステムや医療機器、自動運転車などが数学的に証明された安全なコードで動作すれば、セキュリティ事故や誤動作のリスクが減少します。また、AIが専門家の「知的パートナー」として機能する時代が到来すれば、教育や仕事のあり方も変わっていくかもしれません。
ただし、AIが生成した証明や解決策を理解し、適切に活用するためには、依然として人間の専門知識が不可欠です。AIは強力なツールですが、それを使いこなすための教育や訓練の重要性は、むしろ高まっていくと考えられます。