Nyx Foundation、「ハルシネーションしないAI」の実現を目指す共同研究をKonoe Intelligenceと開始

2026.08.03 10:00

PR TIMES

Nyx Foundation
形式検証と圏論で、AIの出力を数学的に保証する枠組みへ

一般社団法人 Nyx Foundation（所在地：東京都文京区、以下「Nyx」）は、Konoe Intelligenceと共同で、「ハルシネーションしないAI」の実現を目指す研究を開始したことをお知らせいたします。

AIの答えを、そのまま信じてよいのか。本共同研究は、この問いに数学で答えようとする試みです。Lean（コンピュータが証明の正しさを検証できる形式言語）をネイティブに出力するLLMと、圏論（異なる数学の構造を統一的に捉える理論）に基づく機械学習を組み合わせ、AIの出力を確率ではなく数学的な証明によって保証する枠組みを構築します。Nyxが持つ形式検証・Lean 4形式化の知見と、Konoe IntelligenceのAI Safetyにおける実践知見を掛け合わせ、AIが誤った情報を出力するという根本問題に取り組みます。

背景：AIが下した判断の正しさを誰が保証するのか
AIが誤った情報を出力する「ハルシネーション」は、チャットボットの誤答にとどまりません。2024年、DeepMindのAlphaProofは国際数学オリンピック（IMO）で銀メダル相当の成績に到達しました。2025年にはHarmonic AIのAristotleがIMO 2025で6問中5問を解き、金メダル相当に達しています。AIの数学的推論は、この2年で急速に人間のトップ層へ近づきました。同時にAIは、金融取引・半導体チップ設計・航空宇宙など、判断ミスがそのまま人命や資産の損失につながる領域にも入り始めています。AIが下した判断の正しさを、誰が、どうやって保証するのか。この問いは、もう避けて通れません。

「ハルシネーションしないAI」への有力なアプローチとして注目を集めているのが、LeanやCoqといった形式言語で、証明そのものを直接書き出すLLMです。人間の言葉ではなく、コンピュータがそのまま検証できるコードで答えを返すため、「正しいかどうか」を人の目ではなく機械的なチェックだけで判定できます。DeepMindのAlphaProof、ByteDanceのSeed Prover、DeepSeekのDeepSeek-Prover、Princeton発のGoedel-Prover、そして累計調達額約2.95億ドルのHarmonic AIが手がけるAristotleなど、世界の主要な研究機関から資金潤沢なスタートアップまでが、この領域に参入しています。

見過ごされてきた根本問題：具体の証明を、一つずつ力任せに解いている

しかし、この力任せのアプローチには、見過ごされてきた限界があります。数学には、群（対称性を扱う世界）、位相空間（つながり方を扱う世界）、環（足し算とかけ算を扱う世界）など、いくつもの「世界」があります。たとえば、ある性質を保ったまま要素を別の場所に移す方法はただ一つに決まる、という性質があります。専門的には「直積への準同型の一意性」と呼ばれるこの性質は、群でも位相空間でも環でも、形を変えて繰り返し現れます。しかし今のLean証明AIは、この「同じ形」に気づく手立てを持たず、そのたびに一から証明を探索し直しています。証明すべき定理の数は、数学的な構造の数だけ膨らみ続け、モデルを大きくしても、探索に計算資源を積んでも、追いつくことができません。

本共同研究は、この証明探索の中間表現に圏論を導入し、異なる数学的構造をまたぐ「同じ形」を機械が扱える対応関係として書き下すことで、探索空間そのものを圧縮することを目指します。あわせてLeanをネイティブに出力するLLMを研究開発し、証明の生成から検証までのパイプライン全体を機械化します。

解決策：証明の中間表現への圏論の導入

本共同研究では、この証明探索の中間表現に圏論を導入します。圏論は、代数・幾何・論理といった異なる数学の分野をまたいで「構造が同じである」ことを扱う数学です。いわば、異なる数学の「世界」を、数学的に厳密な形でつなぐ翻訳辞書だと言えます。この辞書を使えば、一つの抽象的な設定で性質を一度だけ証明すれば、関手（世界と世界をつなぐ数学的な変換）を通じて、群・位相空間・環などすべての具体的な構造へ自動的に転用できます。実際、Leanの数学ライブラリmathlib4では、圏論に関する証明の大半が自動化タクティク（証明の組み立てを自動化する仕組み）によってすでに機械的に処理されており、圏論に寄せた部分はそのまま機械に任せることができます。

このアプローチがもたらす効果は3つあります。
- 証明探索の分岐削減：圏論を中間表現とすることで、無闇な探索を大幅に減らせる
- 転移学習：抽象的な定理を1つ証明すれば、対応する具体的な問題がまとめて解ける
- 証明計画の可視化：証明の途中経過（サブゴール）を、人間が追跡できる形で表現できる

両社の強みと役割
本共同研究は、形式検証の理論的基盤と、AIの実践的脆弱性評価という、両社の異なる知見を掛け合わせることで成立しています。

Konoe Intelligence（AIの実践的脆弱性評価）
同社は、OpenAIモデルへのプロンプトインジェクション（AIへの指示に悪意ある入力を紛れ込ませる攻撃手法）の成功により「Red-Teaming Challenge - OpenAI gpt-oss-20b」で入賞するなど、AI Safetyの最前線で実績を積んでいます。本共同研究では、AI Safetyの実践的知見と攻撃者視点での評価を担います。

Nyx Foundation（形式検証の理論的基盤）
Nyxは、ケンブリッジ大学で開催された耐量子ワークショップ「PQ Interop」に招聘を受け、耐量子署名の形式検証結果を発表しました。また、Ethereumの次世代仕様「Lean Ethereum」の形式化を通じて、テストでは検出されていなかった仕様自体の重大なバグを複数発見・修正するなど、形式検証を軸とした実績を積み重ねてきました。本共同研究では、形式検証・Lean 4形式化の知見と研究基盤を提供します。

この2つの知見を掛け合わせることで、「AIが誤った情報を出さない」という要求に、数学的な答えを出します。

今後について
本共同研究は開始段階であり、具体的な研究成果は今後の進展に伴い順次公開してまいります。
AIが社会の重要な判断を担う時代において、その出力の信頼性は、確率ではなく数学的な証明によって保証されるべきだと両者は考えています。本共同研究を起点に、数学と組み合わせた安全なLLM構築の枠組みづくりを推進してまいります。

Konoe Intelligenceについて

https://www.konoe-intelligence.net/

Konoe Intelligence 株式会社は「安全な超知能に最速で到達する」をミッションに掲げ、AI安全性を専門とする研究開発スタートアップです。
解釈可能性手法を統合したAIモデルの安全性評価やモデル開発、AIに対するレッドチーミング等を提供。
OpenAIが主催した「Red-Teaming Challenge - OpenAI gpt-oss-20b」において、Top20に日本人で唯一入賞。
- 所在地: 京都府京都市上京区甲斐守町97西陣産業創造會館
- メール: info@konoe-intelligence.net
- Konoe Intelligence: https://www.konoe-intelligence.net/

Nyx Foundationについて

https://nyx.foundation

一般社団法人Nyx Foundation（所在地：東京都文京区）は、Ethereum・ブロックチェーンに特化した私設の研究機関です。形式検証とセキュリティを専門領域とし、次世代プロトコルの安全性向上に取り組んでおります。

すべての活動資金は寄付・研究助成金・スポンサーシップによって支えられております。Ethereum Foundationやブロックチェーン企業・大学との連携を進め、Financial Cryptography 2026 DeFi Workshopでの論文採択、ICLR 2026 Agents in the Wild Workshop採択、Ethereum次期アップグレード「Fusaka」監査コンテストでの脆弱性発見数世界第1位、イーサリアム財団研究助成金採択など、国際的な学術成果と実績を上げております。

本件に関するお問い合わせ先
一般社団法人 Nyx Foundation
所在地: 東京都文京区
メール: contact@nyx.foundation
Nyx Foundation: https://nyx.foundation/