8月17日、IEEE Spectrumが「AI-Generated Math Proof Hints at a Path to Safer Automated Code」と題した記事を公開した。AIが素数に関する「246定理」の証明を自動検証することに初めて成功し、AI生成コードの正しさを数学的に担保する道筋を示した取り組みについて詳しく紹介している。
AIが書いたコードの正しさは誰が保証するのか
Axiom Mathの創設数学者Ken Onoは元記事の中で、AIが生成するコードが社会インフラ・金融システム・セキュリティ基盤に組み込まれつつある現状に言及し、そのコードが本当に正しいかどうかを検証する手段の不足を問題提起している。ハルシネーション、バグ、意図しない脆弱性への懸念は拭えないままだ。Axiom Mathが今回示したのは、数学的証明の形式検証技術がその問題に応用できるという構想だ。
246定理とは何か
そもそも今回検証した「246定理」について整理する。
素数には「双子素数（twin primes）」と呼ばれる、差が2の素数ペアが存在する（例：3と5、11と13、17と19）。双子素数は数直線上の遠くに行っても現れ続けるというのが「双子素数予想」だが、19世紀にフランスの数学者Alphonse de Polignacが定式化して以来、未証明のままだ。
この問題への最初の突破口は2013年、張益唐（Yitang Zhang）が「差が7000万以内の素数ペアが無限に存在する」ことを証明したことで開いた。その数ヶ月後、オックスフォード大学のJames Maynardが別の手法でこのギャップを7000万から600に一気に縮めた。この功績はMaynardの2022年フィールズ賞受賞に大きく貢献している。
その後、MaynardとUCLAのTerence Tao（2006年フィールズ賞受賞者）らによる「Polymath8b」と呼ばれる数学者の共同研究グループが、ギャップを246まで縮めた。目標の「2」にはまだ遠いが、これが現時点での人類の素数知識の限界点だ。
Axiom Mathが開発した自律型マルチエージェントAIシステム「AxiomProver」は、この246定理の証明を機械検証可能な形式（フォーマル証明）に変換し、正しさを確認することに初めて成功した。
形式検証（Formal Verification）とは
「形式検証」とは、数学的証明をコンピュータが読める形式に変換し、機械的に正しさをチェックする手法だ。人間による査読よりも格段に厳密な確認手段として機能する一方、検証ツール自体の実装バグが偽の証明を受理してしまうリスクも完全にはゼロではなく、万能な保証ではない点には留意が必要だ。
今回の取り組みで特筆すべき点は、「一発勝負の証明検証」に留まらなかったことだ。Axiom Mathは証明の各コンポーネントを他の形式化タスクや数学研究に再利用可能な形で設計したと元記事は伝えている。246定理はそのライブラリの中核をなす成果として位置づけられている。
CMU（カーネギーメロン大学）の博士課程学生で、競合のMath, Inc.によるViazovska証明の形式化を主導したSidharth Hariharanは、現在Axiom Mathのインターンとして246定理の形式化に深く関与している。彼は「Viazovska証明の形式化と比べ、今回の成果はより包括的で実用的な達成だ」と述べている。
コード検証への道筋
Onoが強調するのは、この技術の数学的意義よりも、AI生成コードの正しさを検証する基盤としての可能性だ。
数学的証明の形式検証とソフトウェア検証はもともと密接に関連している。コードの性質——「このアルゴリズムは必ず終了するか」「任意の入力に対して出力は正しいか」——は精密な数学的命題として記述できる。そうした命題を機械的に証明・検証する技術は、数論の定理を扱うAxiomProverと同じ基盤の上に成り立つ。つまり、AIが書いたコードをAIが数学的に検証するという構造を、今回の246定理の形式検証は実証的に示している。
今回の形式検証が対象とした246定理の技術基盤は数論（number theory）に属する。数論は現代の暗号技術やサイバーセキュリティの根幹をなす分野であるため、将来的には暗号プロトコルの正しさの検証にも直接関係してくる可能性がある。数論からコード検証へという流れは飛躍に見えるかもしれないが、形式検証という共通の方法論がその橋渡しをしているという点は押さえておきたい。
Onoはこう締めくくっている：「証明の形式化は、AIから私たちが直面する最も重要な課題を解決するための試験台だ。」
詳細はAI-Generated Math Proof Hints at a Path to Safer Automated Codeを参照していただきたい。
