「ハルシネーションしないAI」の実現に向けて数学的超知能の共同研究をNyx Foudationと開始

Konoe Intelligence株式会社
形式検証と圏論で、AIの出力を数学的に保証するAIモデルの開発




私たちKonoe Intelligence株式会社(旧商号Aladdin Security株式会社)は一般社団法人Nyx FoundationとハルシネーションしないAIの開発に向けて共同研究を開始しました。
概要
答えが正しいかどうかは、答えそのものをいくら眺めても分かりません。正しさを確かめる唯一の方法は、答えに至るまでの論理的な過程、つまり推論を検証することです。今日のAIは高い推論能力を獲得しつつあります。しかし、推論が「強い」ことと、推論が「正しいと保証されている」ことは、同じではありません。AIがハルシネーションなく、説明可能で、人類と調和するために本当に必要なのは、推論の一歩一歩を機械的に検証できる仕組みです。
その検証の言語が、数学です。数学は、人類が宇宙の根本的な真理を発見し、その正しさを証明してきた唯一の手段です。
私たちはハルシネーションしないAI、つまり、数学的超知能を開発します。
検証可能な推論の上に築かれる数学的超知能は、科学技術における人類の進歩を大きく加速させると私たちは確信しています。
私たちはこれまで、AIセーフティ企業として、AIがもたらすリスクと向き合ってきました。その経験から確信していることがあります。出力を事後的に検知しフィルタリングする対症療法では、AIの安全は完成しない。誤りが構造的に起こり得ないAIを作ること――それこそが、AIセーフティの最終形です。本提携は、AIの安全性を「確率の管理」から「数学的な保証」へと引き上げる挑戦です。
その第一歩として、金融、自動車、航空、半導体など、高い品質と信頼性が求められる業界における仕様書やプロトコルの形式化といった形式検証のタスクにおいて、ハルシネーションを構造的に排除した、質の高いモデルを開発してまいります。
背景
日本のAI主権の確保に向けて
AIモデルの開発競争は、いまや米中の2強に収斂しつつあります。基盤モデルを他国に依存するということは、産業データの主権、安全保障、そして言語や文化に根ざした知の在り方そのものを、他国の手に委ねることに他なりません。だからこそ、日本には国産のAIモデルが必要不可欠です。
日本は、決して負けてはいません。経済産業省のGENIACプロジェクトは累計339億円を超える規模で国産基盤モデルの開発を支援し、デジタル庁の政府AI基盤「源内」には7つの国産モデルが採用され、約18万人の行政職員への展開が始まっています。国産モデル開発の土壌は、着実に育っています。
私たちが挑むのは、その次の主戦場です。汎用大規模言語モデルの規模の競争を真正面から追うのではなく、「正しさが保証されたAI」という新しい競争軸で先頭に立つこと。形式手法や品質保証は、日本の製造業・重要インフラが世界最高水準で磨き上げてきた領域です。この土俵であれば、日本には確かな勝ち筋があると私たちは確信しています。
現在のAIの到達点と、残された構造的問題
大規模言語モデルに基づくAIの推論能力は、この2年で劇的に向上しました。推論に特化したモデルが主流となり、2025年には複数のAIが国際数学オリンピック金メダル水準の成績に到達しています。AIは、もはや「推論ができない」存在ではありません。
しかし、ハルシネーションは、依然として解決されていません。近年の研究が示す通り、ハルシネーションは確率的言語モデルの学習の仕組みそのものに由来する構造的な性質であり、モデルの規模を拡大しても消えることはありません。最先端のモデルであっても、予測不可能な形で失敗し得る。そして利用が拡大するほど、その失敗の影響は深刻化していきます。能力は飛躍的に高まったのに、出力の正しさの「保証」は依然として存在しない。
この能力と保証のギャップこそが、安全性が重視される領域へのAI導入を阻む、最後の壁となっています。
なぜハルシネーションは「排除」されなければならないのか
現在のハルシネーション対策。例えば、検索による根拠付け、検証モデル、ガードレールは、いずれも誤りの確率を「下げる」アプローチであり、出力の正しさを「証明」するものではありません。しかし、金融の決済プロトコル、自動車や航空の制御仕様、半導体の設計検証といった領域では、誤り率を下げることと、誤りが起こり得ないことの間に、越えることのできない断絶があります。99.9%正しい答えは、0.1%の誤りが事故につながる世界では使えないのです。
この壁を越える鍵は、AIの外部にある数学的な検証器です。機械的に検証された出力のみを返す仕組みを構築すれば、ハルシネーションは確率的に減るのではなく、構造的に排除することになります。
Nyx Foundationとの共同研究について
Nyx Foundationは、「信頼は、検証から生まれる」を掲げ、AI時代の信頼を検証できる成果としてつくる研究機関です。形式検証（プログラムやプロトコルが仕様どおりに正しく動くことを数学的に証明する手法）とAIセキュリティを専門とし、AIが生成したコードやシステムの正しさを、AIエージェントと数学的手法で機械的に検証する技術を研究しています。これまでに、AIエージェントを用いてEthereumの脆弱性を17件発見し監査コンテストの報告件数で世界1位を獲得、AIバグ発見システム「SPECA」はEthereum Foundationの研究助成に採択されています。
Nyx Foundationのチームは、Ethereum Foundationの研究奨学生を中心に構成され、生成AIと定理証明を研究する京都大学特定准教授・三内顕義氏も参画しています。メンバーの研究はFinancial Cryptography 2026やZKProof、CANS 2025といった国際会議に採択され、Ethereum Foundation・Fenbushi Capital・TL;DRフェローシップから研究助成を受けてきました。ケンブリッジ大学の耐量子暗号ワークショップやコロンビア・ビジネススクールで成果を発表し、SMBC日興証券やアライドアーキテクツ、香港科技大学、東京大学、金融庁とも連携や対話を重ねています。共同創業者はGethやErigonなど広く使われるソフトウェアの脆弱性を実際に発見・報告し、Lean（証明を計算機が機械的に検証できる言語）による形式検証も主導しています。
当社はNyx Foundationが有する先進的なAI、サイバーセキュリティ、数学の知見や技術、研究成果と、当社が培ってきたAIの安全性や数学の知見を組み合わせます。
両社の強みを融合することで、数学的超知能の開発を加速させます。
数学的超知能について
AIの答えを、そのまま信じてよいのか。本共同研究は、この問いに数学で答えようとする試みです。Lean（コンピュータが証明の正しさを検証できる形式言語）をネイティブに出力するLLMと、圏論（異なる数学の構造を統一的に捉える理論）に基づく機械学習を組み合わせ、AIの出力を確率ではなく数学的な証明によって保証する枠組みを構築します。
LeanやCoqといった形式言語で、証明そのものを直接書き出すことで、人間の言葉ではなく、コンピュータがそのまま検証できるコードで答えを返すため、「正しいかどうか」を人の目ではなく機械的なチェックだけで判定できます。
ユースケース
(1) 高信頼産業における仕様・コードの形式検証
半導体設計ではすでに形式検証が標準工程であり、自動車（ISO 26262）や航空（DO-178C）でも形式手法の活用が求められています。しかし現状では、自然言語で書かれた仕様書を数学的な形式仕様へ翻訳する作業が専門家の人手に依存しており、これが普及の最大のボトルネックです。仕様の形式化と証明の生成をAIが担うことで、金融の決済プロトコル、車載・航空の制御仕様、半導体の設計検証といった業務を、桁違いのスピードとコストで実行可能にします。
(2) 形式検証の民主化 ── 「証明付き」が当たり前になる世界
形式検証はこれまで、宇宙・防衛・半導体など、失敗のコストが極端に大きい領域でしか採算が合いませんでした。AIが形式化のコストを劇的に下げれば、この前提が崩れます。金利や保険料の計算ロジック、会計処理、業務システムの数値計算といった、あらゆる企業に存在する「間違えてはいけない計算」を、証明付きで保証できるようになります。これまで形式検証の対象ですらなかった広大な領域に、新しい市場が生まれます。
(3) AIが書いたものを、AIが証明する
ソフトウェア開発の主体がAIエージェントへ移行するにつれ、人間によるレビューはスケールしなくなります。AIが生成したコードや設計の正しさを、別のAIが数学的証明によって機械検証する仕組みは、AI時代の品質保証の基盤そのものです。Nyx FoundationがAIエージェントによる脆弱性発見で実証してきた技術は、この未来に直結しています。
(4) 数学・科学研究の加速
検証済みの推論しか返さないAIは、研究者にとって「誤りのない共同研究者」となります。定理や導出の機械検証、検証済みの関連定理の提示を通じて、数学をはじめとする科学研究のサイクルを加速させます。
目標
6ヶ月後の成果指標
- 標準テストで世界最高クラスに並ぶ。
miniF2F を 100問中 90問（pass@32）解ける状態にします。出発点の弟分モデル(84.6問)を、学習で世界最高の兄貴分(90.4問)まで押し上げます。
- 時間をかければほぼ解ききる。
1問に多く挑戦してよい条件では、100問中 95問まで正答率を上げます。
- まだ誰も高得点を取れていない難関テストで、はっきり上回る。
miniF2F は世界中が高得点に近づいていて差がつきにくいので、より難しい PutnamBench（大学レベルの難問集）で明確な改善を出します。本当の勝負どころはここです。
- AIの「読み違い」を半分に減らす。
AIは問題文を数式に翻訳する段階で意味を取り違えることがあります。これを機械で検出し、Nyx独自技術で今の半分に減らします。ここが他社と差がつく独自性です。
- 成果を論文として発表する。

Nyx Foundationについて



一般社団法人Nyx Foundation（所在地：東京都文京区）は、「信頼は、検証から生まれる」を掲げる私設の研究機関です。形式検証とAIセキュリティを専門領域とし、AIが生成するコードやシステムの正しさを数学的に検証する技術の研究に取り組んでいます。
すべての活動資金は寄付・研究助成金・スポンサーシップによって支えられています。Ethereum Foundationをはじめとする企業・財団や国内外の大学との連携を進め、Financial Cryptography 2026 DeFi Workshopでの論文採択など、国際的な学術成果も上げています。
Konoe Intelligenceについて



Konoe Intelligence は「安全な超知能に最速で到達する」をミッションに掲げるAI セキュリティカンパニーです。
AIリスクの評価技術の研究開発を中核とし、政府機関・企業との連携を通じて、日本のAI主権の確立に貢献することを目指しています。
会社名：Konoe Intelligence株式会社
所在地：京都府京都市上京区甲斐守町97 西陣産業創造會館
代表者：代表取締役 勘佐 圭吾
設立：2025年2月
事業内容：AIセキュリティ事業、サイバーセキュリティサービス
Webサイト：https://www.konoe-intelligence.net/
本件に関するお問い合わせ
Konoe Intelligence株式会社
メール：info@konoe-intelligence.net
Web サイト：https://www.konoe-intelligence.net/contact