2026年8月3日、国内の一般社団法人Nyx Foundationは、Konoe Intelligenceと共同で「ハルシネーションしないAI」の実現を目指す研究を開始したと発表した。Lean（※1）をネイティブ出力するLLMと圏論（※2）を組み合わせ、AIの回答を確率ではなく数学的な証明で保証する新たな枠組みの構築を目指す取り組みである。
AIの回答を数学的証明で保証へ
今回の共同研究は、AIが誤った情報を生成する「ハルシネーション」という根本課題に対し、形式検証と数学を用いて解決を図る試みだ。Nyxが持つLean 4形式化や形式検証の知見と、Konoe IntelligenceのAI Safety分野における実践的な評価技術を組み合わせ、証明の生成から検証までを機械的に完結させる仕組みの実現を目指している。
背景には、AIが金融取引や半導体設計、航空宇宙など、高い信頼性が求められる領域へ急速に広がっている現状がある。一方で、従来の証明生成AIは数学の構造ごとに個別の証明探索を繰り返す必要があり、探索空間が膨大になるという課題を抱えていた。
そこで両社は、証明探索の中間表現として圏論を導入する。異なる数学的構造に共通する「同じ形」を抽象化し、一度証明した内容を複数の分野へ転用できるようにすることで、探索効率の向上を狙う。また、Leanをネイティブに出力するLLMを組み合わせることで、AIの回答を機械が直接検証できる環境の構築を進める考えだ。
※1 Lean：コンピュータが数学的証明の正しさを自動検証できる形式言語。証明をプログラムとして記述し、機械的に正誤を確認できるため、高い信頼性が求められる研究やソフトウェア開発で活用が進んでいる。
※2 圏論：異なる数学分野に共通する構造や関係性を統一的に扱う数学理論。複数の対象に共通する性質を抽象化できるため、異なる問題へ証明を効率的に転用する枠組みとして注目されている。
AIの信頼性向上へ 安全なLLM開発の基盤となる可能性
このアプローチが実現すれば、AIは「もっともらしい回答」を返すだけでなく、その正しさを数学的に証明できる存在へ近づく可能性がある。両社は、圏論を活用することで証明探索の分岐を削減し、抽象的な定理を複数の問題へ転用する転移学習や、証明過程を人間が追跡しやすい形で可視化できるとしている。
役割分担も明確だ。Konoe IntelligenceはAI Safetyの知見を生かし、攻撃者視点からAIの脆弱性評価を担当する。一方のNyxは、形式検証やLean 4形式化に関する研究基盤を提供し、数学的な正当性を支える役割を担う。異なる専門性を組み合わせることで、「AIが誤った情報を出さない」という要求に数学的な裏付けを与えることを目指している。
もっとも、本研究は開始段階にあり、具体的な成果は今後順次公開される予定だ。数学による保証が実用レベルまで到達するには検証の積み重ねが欠かせず、研究成果が実際のLLMへどのように組み込まれるかも今後の焦点となる。
それでも、AIの信頼性を確率論ではなく証明によって担保するという発想は、安全性が重視される次世代AIの開発に新たな方向性を示す取り組みと言えそうだ。
