AIの出力を数学的証明で保証する枠組み構築へ
イーサリアム（Ethereum）に特化した日本の私設研究機関ニックス・ファウンデーション（Nyx Foundation：以下、Nyx）が、AIセーフティを専門とするコノエ・インテリジェンス（Konoe Intelligence）と、「ハルシネーションしないAI」の実現を目指す共同研究を開始したと8月3日に発表した。
AIは金融やソフトウェア開発など重要な判断にも活用され始めている一方、誤った情報を出力する「ハルシネーション」が課題となっている。両者は、AIの回答を確率的に評価するのではなく、数学的な証明によって正しさを保証する仕組みの構築を目指すという。
Nyxによると、現在は「リーン（Lean）」や「コック（Coq）」などの形式言語を用いて数学の証明を生成するAIの研究が進んでいるという。Google DeepMindの「AlphaProof」やByteDanceの「Seed-Prover」、DeepSeekの「DeepSeek-Prover」などが代表例として挙げられる。
これらのAIは、人間向けの文章ではなく、コンピュータが直接検証できる形式言語で数学の証明を出力することが特徴だ。そのため、人が内容を確認するのではなく、機械的に正しさを検証できるとのこと。両者も今回の共同研究で、数学的な証明をコンピュータが直接検証できる形式言語「リーン」を出力する大規模言語モデル（LLM）を活用する。
一方で、Nyxは既存の証明AIについて、数学の各分野で共通して現れる考え方を十分に再利用できず、似たような証明でも定理ごとに一から探索し直していることが課題になっているという。
両者は、異なる数学分野で共通する考え方を再利用できるようにすることで、AIが同じような証明を何度も作り直す必要がない仕組みの構築を目指す。具体的には、証明探索の中間表現として「圏論」を導入する。圏論は、異なる数学分野に共通する構造を扱う理論であり、異なる数学を結び付ける「翻訳辞書」のような役割を担う。一度抽象的な性質を証明すれば、その証明を複数の数学的構造へ適用できるため、証明探索を効率化できるとのこと。
両者は、この手法により証明探索の分岐削減や、抽象的な定理を複数の具体的な問題へ適用する転移学習、証明過程の可視化を目指す。また、リーンを直接出力するLLMを開発し、証明の生成から検証までを自動化する方針だ。
同研究では、Nyxが形式検証やリーン4（Lean 4）の形式化に関する知見や研究基盤を提供する。一方、コノエ・インテリジェンスは、AIセーフティの実践的知見や攻撃者視点による脆弱性評価を担うとのこと。
コノエ・インテリジェンスは、AIへの疑似攻撃を通じて安全性を検証するAIレッドチーミングを手掛ける。同社は旧社名のアラジン・セキュリティ（Aladdin Security）時代に、オープンAI（OpenAI）が主催した「レッド・チーミング・チャレンジ（Red-Teaming Challenge – OpenAI gpt-oss-20b）」で上位20に入賞した実績を持つ。
Nyxは、イーサリアムやブロックチェーンの形式検証とセキュリティを専門とする研究機関だ。同団体は、仕様書から「守るべき条件」を抽出し、AIが実装コードとの整合性を検証する監査システム「スペカ（SPECA：Specification-to-Checklist Agentic Auditing）」を開発するなど、AIと形式検証を組み合わせた研究を進めてきた。
またNyxとコノエ・インテリジェンスは7月、AIが大量生成する脆弱性レポートの検証から修正までの自動化を目指す業務提携を発表していた。今回の共同研究では、その取り組みに加え、AIの出力自体を証明可能な形式で生成し、その正しさを機械的に検証する枠組みの構築を目指す。
なお、同研究は開始段階であり、具体的な成果は今後の進展にあわせて順次公開される予定とのこと。両者は、数学と組み合わせた安全なLLM構築の枠組みづくりを進める方針だ。
【お知らせ】 「ハルシネーションしないAI」の実現を目指す研究を、Konoe Intelligence と共同で開始しました。 Leanをネイティブに出力するLLMと、圏論に基づく機械学習を組み合わせ、AIの出力を確率ではなく数学的な証明によって保証する枠組みを構築します。https://t.co/Ni76RhCMgd
— Nyx Foundation (@NyxFoundation) August 3, 2026
参考：プレスリリース
画像：PIXTA