「AIの計算が正しいって、どうやって証明するんですか?」—— 有限体の上のニューラルネットワーク入門
研究室のコーヒーブレイクで聞く、ZKML・FHE・オンチェーンAIの全貌
ある金曜の午後。有限体上のニューラルネットワークを研究しているリルル先生の研究室に、3人の学生が遊びに来た。
ユキ(高校2年生。プログラミングが好き。数学はmod計算くらいまで)
カイト(大学2年生。線形代数と群・環・体の基礎を履修済み)
リン(大学院修士1年。代数幾何と計算複雑性理論を勉強中)テーブルにはコーヒーとチーズケーキ。リルル先生がホワイトボードのペンを手に取る。
第1話 「そのAI、本当にちゃんと計算したの?」
リルル先生: まず聞きたいんだけど、ChatGPTって使ったことある?
ユキ: もちろん! 毎日使ってます。
リルル先生: じゃあさ、ChatGPTが出した答え、本当にGPT-4で計算されたって、どうやって確認する?
ユキ: え? ……OpenAIを信用するしかないですよね?
リルル先生: そう。今のAIの世界は「信用してください」で成り立ってる。でもこれ、3つの場面で困ることになる。
一つ目。 銀行のAIがローンを却下したとする。「AIが判断しました」って言われても、本当にそのAIがちゃんと動いたのか、途中で人が結果を差し替えてないか、外からは分からない。EU AI Actみたいな規制は、これを検証可能にしろって言い始めてる。
二つ目。 企業は「うちのAIは精度99%です」って証明したいけど、モデルの中身は企業秘密だから見せたくない。逆にユーザーは医療データをAIに渡したいけど、データが漏れるのは嫌だ。秘密を守りながら正しさを示すっていう、矛盾した要求がある。
三つ目。 ディープフェイク。これからの時代、カメラが撮影した瞬間に「この写真は本物です」っていうデジタル証明書を発行できたら、AI生成コンテンツと区別できるよね。
カイト: その3つ、全部「計算が正しいことを証明する」っていう問題に帰着しますね。
リルル先生: その通り。で、その証明を数学的にやる技術がある。それが ZKML と FHE なんだけど、両方とも核心にある数学は同じ。ニューラルネットワークを有限体の上で動かすってこと。
ユキ: 有限体?
リルル先生: 順番に説明するよ。まずはニューラルネットワークの話から。
第2話 ニューラルネットワークは足し算と掛け算の塊
リルル先生: ユキ、ニューラルネットワークって何をしてるか知ってる?
ユキ: なんか、脳みたいにニューロンが繋がって学習するやつ……?
リルル先生: 名前はそうだけど、中身はもっとシンプル。一個のニューロンがやってるのは、こう。
出力 = w × x + b
入力 x に重み w を掛けて、バイアス b を足す。ただの一次式。ニューラルネットワークは、これを何千何万と並べて、層を重ねただけ。
ユキ: え、それだけ?
リルル先生: それだけ。ニューラルネットワークは巨大な足し算・掛け算の塊なの。ただし一個だけ厄介なやつがいる。ReLU っていう活性化関数。
カイト: $max(0, x)$ ですよね。負ならゼロ、正ならそのまま。
リルル先生: そう。これ、「$x$が正か負か判定する」っていう大小比較を含んでるんだよね。足し算と掛け算は問題ないけど、この大小比較が後で爆弾になる。
リン: 有限体には順序構造がないからですね。
リルル先生: さすが。じゃあ有限体の話に行こう。
第3話 有限体 —— 「余りの世界」の驚くべき力
リルル先生: ユキ、「$7$で割った余り」って計算できる?
ユキ: できますよ。$10÷7$ は余り$3$。
リルル先生: じゃあ「$7$で割った余りだけの世界」を作ってみよう。数は $0, 1, 2, 3, 4, 5, 6$ の$7$個しかない。
3 + 5 = 8 → 8 mod 7 = 1
3 × 4 = 12 → 12 mod 7 = 5
ユキ: ふむふむ、足し算と掛け算は普通にできるんですね。
リルル先生: で、ここがすごいんだけど、割り算もできる。$5$で割りたい? 5の逆数を見つければいい。$5 × 3 = 15 → 15 mod 7 = 1$。だから5の逆数は3。
ユキ: えっ、整数の世界なのに割り算ができるんだ!
リルル先生: そう。素数 $p$ で余りを取る世界では、足し算・引き算・掛け算・割り算、全部できる。これを有限体 $F_p$ って呼ぶ。
カイト: $Z/pZ$ ですね。フェルマーの小定理から、非零元は全部乗法逆元を持つ。
リルル先生: そう。で、暗号の世界では $p$ がめちゃくちゃデカい。BN254っていう楕円曲線だと、$p$ は約2の254乗。77桁の素数。
リン: その巨大な有限体の上でニューラルネットワーク全体を動かすわけですよね。
リルル先生: そういうこと。で、ここで問題が出る。
ユキ: さっきの ReLU?
リルル先生: 正解。有限体では「$5$は正か?負か?」って聞いても意味がない。だって $mod$ $7$ で $5 = -2$ でもある。正と負の区別がそもそも存在しないんだよ。
カイト: だから ReLU の「負ならゼロにする」が直接は書けない。ビット分解して符号ビットを取り出すと $O(log$ $p)$ 個の制約が必要になって、BN254 だと1回の ReLU に約$254$個の制約……。
リルル先生: そう。これがReLU問題。解決法は3つある。
一つ目、ReLUの代わりに $x^2$ みたいな多項式を使う。掛け算だけで書けるから有限体と相性がいい。二つ目、今言ったビット分解。重いけど確実。三つ目、ルックアップテーブル。「入力がこの値ならReLUの出力はこの値」っていう対応表を事前に作っておく。2024年のzkLLM論文の tlookup はこれの発展版で、LLMのSoftmaxとかも漸近的オーバーヘッドなしで証明できるようになった。
第4話 量子化 —— 小数を有限体に持ち込む
ユキ: でも待ってください。普通のニューラルネットワークって小数で計算しますよね? 有限体は整数しかないのに、どうやって?
リルル先生: いい質問。答えは量子化。
重みが $0.75$ だとする。$1000$倍すると $750$。整数になった。全部同じ倍率で拡大して整数にすれば、ネットワーク全体を整数演算で動かせる。
ユキ: あ、それってスマホのAIでもやってるやつ?
リルル先生: そう! $32$ビット浮動小数点を$8$ビット整数に変換するのと同じ発想。ただし有限体版では変換先が254ビットの巨大体の元になる。
カイト: 乗算するとスケールが倍々になるから、再量子化が要りますよね。$F_p$ 上だと $(2^s)^{-1}$ $mod$ $p$ の乗算で割り算を実現して……。
リルル先生: そう、そこが非自明。丸め誤差の管理が大変なんだけど、EZKLっていうツールがこの範囲解析を自動化してくれてる。あと2024年に「固定小数点演算でもReLUやGELUは普遍近似性を維持する」っていう理論的保証も証明されたんだよ。
第5話 ゼロ知識証明って何? —— 中身を見せずに正しさを示す魔法
ユキ: ここまでで、ニューラルネットワークを有限体の上で動かせることは分かりました。でも、それが「証明」とどう繋がるんですか?
リルル先生: 核心に入ろう。ゼロ知識証明の話。
ユキ、こういう状況を想像して。テストの答案を先生に見せずに、自分が正解を知ってることだけを証明したい。普通は無理だよね。
ユキ: 答えを言っちゃったら見せたことになるし……。
リルル先生: ところが、数学の世界ではこれができる。仕組みはこう。
先生がランダムなチャレンジ問題を出す。「正解を知ってる人じゃないと絶対に答えられない問題」を。で、それに正解してみせる。1回だと偶然かもしれないけど、100回連続正解したら?
ユキ: さすがに「こいつ本当に知ってるな」ってなります。
リルル先生: でも先生は答えそのものは一度も聞いてない。これがゼロ知識証明。「中身を見せずに、正しさだけを示す」技術。
ZKMLではこう使う。
- AI企業(証明者): 「モデル $M$ に入力 $x$ を入れて、出力 $y$ を得ました」
- ユーザー(検証者): 「証拠を見せて」
- AI企業: (モデルの中身もデータも見せずに)数学的な証明 $π$ を渡す
- ユーザー: $π$ を高速に検証 → OK!
ユキ: さっきからSNARKとかSTARKとか出てきますけど、そもそもSNARKって何ですか?
リルル先生: SNARKは Succinct Non-interactive ARgument of Knowledge の略。日本語にすると「簡潔で非対話型の知識の論証」。一つずつ分解するとこう。
- Succinct(簡潔): 証明のサイズが、元の計算がどんなに巨大でも、めちゃくちゃ小さい。
- Non-interactive(非対話型): 証明者と検証者がやりとりしなくていい。証明者が証明を一発で作って、渡して、終わり。
- ARgument of Knowledge(知識の論証): 「私はこの計算の答えを知っています」ということの論証。ただし、計算能力に限界がある相手に対してのみ有効。無限の計算力を持つ相手には原理的に破れる可能性があるから、数学の「定理の証明」とは区別して「論証(argument)」って呼ぶ。
カイト: だからさっきの「$100$%じゃない」話に繋がるんですね。proof(証明)じゃなくてargument(論証)。
リルル先生: そう。で、SNARKの実現には楕円曲線暗号が使われてる。具体的にはペアリングっていう特殊な演算が鍵になる。
一方、STARKは Scalable Transparent ARgument of Knowledge の略で、楕円曲線を使わずにハッシュ関数ベースで動く。Transparent(透明)っていうのは、trusted setup——事前に秘密の儀式みたいなセットアップ——が不要ってこと。その代わり証明サイズがSNARKより大きくなる。
じゃあ、その証明$π$の中身を具体的に見てみよう。
ユキ: その $π$ って、具体的にはどんなもの? ファイル? 数字?
リルル先生: すごくいい質問。$π$ の中身はね、有限体の元の組なの。具体的にはだいたいこんな感じ。
SNARKの場合、証明 $π$ は楕円曲線上の点が$2〜3$個。バイト数にすると約$192$バイト。USBメモリどころか、ツイート$1$個に収まるサイズ。
ユキ: たった192バイト!? ニューラルネットワークの計算って何百万回もの掛け算があるのに?
リルル先生: そこがSNARKの魔法。何百万個の制約を全部まとめて、たった数個の楕円曲線の点に圧縮しちゃう。検証者はその数個の点に対してペアリング演算っていうのを数回やるだけ。だから検証がミリ秒で終わる。
STARKの場合は証明がもう少し大きくて、数十〜数百キロバイト。こっちはハッシュ値の列とMerkle木の経路情報が中心。楕円曲線を使わないから耐量子性がある代わりに、証明サイズが大きくなる。
カイト: つまり証明の実体は、楕円曲線の点かハッシュ値の列で、どっちにしても元のデータやモデルの情報は含まれてない。
リルル先生: その通り。証明 $π$ を見ても、入力データもモデルの重みも復元できない。これが zero-knowledge(ゼロ知識)の意味。
第6話 ランダムな値はどこで使われるの?
ユキ: さっき「ランダムなチャレンジ」って言ってましたよね。証明の中にランダムな値がいっぱい入ってるんですか?
リルル先生: いいところに気づいたね。ランダムな値は2つの場面で使われる。
一つ目は、証明を作るとき。 証明者は計算の中身を隠すために、ランダムな値(ブラインディングファクターって呼ぶ)を混ぜる。これがないとゼロ知識にならない。たとえば多項式に意味のないランダムな項を足すことで、多項式の形から元のデータを推測できなくする。
二つ目は、証明を検証するとき。 検証者(または Fiat-Shamir変換でハッシュ関数)がランダムなチャレンジ $r$ を生成する。証明者はこの $r$ を使って多項式を評価した値を返す。
ユキ: なるほど……でも、なんでランダムである必要があるんですか?
リルル先生: ここがキモ。証明の仕組みを超ざっくり言うとこう。
ニューラルネットワークの計算全体を、一つの巨大な多項式の等式に変換する。「正しく計算したなら、この多項式 $H(x)$ は全ての点でゼロになるはず」っていう形。
で、検証者がランダムに点 r を選んで、「$H(r)$ はゼロですか?」って聞く。
もし証明者がズルをしてたら、$H(x)$ は本当はゼロじゃない。ゼロじゃない多項式がたまたまランダムに選んだ点でゼロになる確率は、Schwartz-Zippelの補題で高々 $d/p$($d$ は多項式の次数、$p$ は有限体のサイズ)。
ユキ: あ、だからランダムじゃないとダメなんだ! 証明者が事前に $r$ の値を知ってたら、その点だけゼロになるような嘘の多項式を作れちゃう。
リルル先生: 完璧。ランダムだからこそ、嘘をつけない。
で、もう一つ大事なこと。検証者に渡す証明 $π$ の中にはランダムな値そのものは入っていない。$π$ に入ってるのは、ランダムなチャレンジに対する「応答」——多項式の評価値や楕円曲線の点——だけ。応答からチャレンジ $r$ を逆算することはできないし、もちろん元データやモデルも復元できない。
カイト: 非対話型の場合はFiat-Shamir変換で、チャレンジをハッシュ関数から導出するんですよね。証明者がハッシュの出力を予測できないから、ランダムオラクルと同等のセキュリティが得られる。
リルル先生: そう。まとめると——
- 証明者は「ランダムな目隠し」を混ぜて証明を作る → ゼロ知識を保証
- 検証者は「ランダムなチャレンジ」を出す → 嘘が通らないことを保証
- 検証者に渡るのは「応答」(楕円曲線の点やハッシュ列)だけ → データもモデルも漏れない
第7話 「なぜ100%じゃなくて99.999…%なの?」
ユキ: 一つずっと気になってたんですけど、ゼロ知識証明って「$100$%正しい」わけじゃないんですか?
リルル先生: すごくいい質問。ここ、多くの人が混乱するポイント。
数学の世界には2種類の「証明」がある。
一つ目が、数学の定理証明(形式証明)。
ユキ: 定理証明って何ですか?
リルル先生: 高校の数学で「〜を証明せよ」って問題あるでしょ? 「三角形の内角の和は180度である」とか。あれは論理のルールだけで、一歩一歩、絶対に正しい結論を導く。途中で「たぶん」とか「だいたい」はない。100%。
コンピュータの世界でもこれをやる道具があって、定理証明器(Coq、ACL2、Leanなど)って呼ばれてる。プログラムのコードが仕様通りに動くことを、数学的に100%保証できる。確率的な誤りは一切ない。
ユキ: へー、プログラムの正しさを数学で証明できるんだ。
リルル先生: そう。で、この形式証明は「ZK回路の設計図にバグがないか?」を検証するのに使う。実際、2024年の研究だとSNARKシステムの回路バグの約96%が「制約の書き忘れ」で、形式証明で事前に潰せるやつだった。
二つ目が、ゼロ知識証明(暗号学的証明)。 こっちは「特定の計算が正しく実行された」ことを示すんだけど、原理的にごくごく微小な確率で嘘が通る可能性がある。
ユキ: なんで$100$%にできないんですか?
リルル先生: さっきの話に繋がるんだけど、嘘の証明が通るかどうかが「ランダムに選んだ点で多項式がたまたま一致するか」に帰着するから。
次数 $d$ の多項式が、サイズ $p$ の有限体上でランダムな点で偶然ゼロになる確率は高々 $d/p$。BN254だと $p ≈ 2^{254}$ で、d はネットワークの規模に依存するけどせいぜい数百万。だから嘘が通る確率は——
10^6 / 10^77 ≈ 10^{-71}
カイト: $10$のマイナス$71$乗……。宇宙の全原子の数が$10^{80}$くらいだから、それより遥かに小さい。
リルル先生: そう。実用上は$100$%と同じなんだけど、理論的にはゼロじゃないから「$99.999...$%」って言い方になる。
ユキ: じゃあ、2つの証明は役割が違うんですね。
リルル先生: そう。形式証明が回路の設計図にバグがないことを100%保証し、ゼロ知識証明がその設計図通りに実際に実行されたことを99.999...%保証する。二段構えで安全性を確保するわけ。
ユキ: 形式証明って、暗号化したデータに対してもできるんですか?
リルル先生: 形式証明は「プログラムのコード」に対してやるものなの。データの暗号化とは別の話。回路の設計図は通常公開されてるから、暗号化の必要がそもそもない。一回検証すれば、その回路は永遠に正しい。一方、ゼロ知識証明は毎回の推論ごとに生成するもので、証明者が手元で平文のデータを使って計算し、検証者には証明 π だけが渡る。
リン: つまり形式証明は「オフラインで1回やれば済む設計検証」、ゼロ知識証明は「オンラインで毎回生成する実行検証」。
リルル先生: 完璧な整理。
第8話 「指定したモデルで改竄なく計算された」ことが、なぜ有限体で証明できるの?
ユキ: ここが一番分からないところなんです。なぜ有限体の上でニューラルネットワークを動かすと、「このモデルを使って、改竄なく最初から最後まで計算しました」ってことが証明できるんですか?
リルル先生: よし、これが本丸だ。順を追って説明するね。
まず、ニューラルネットワークの計算は足し算と掛け算の塊だよね。これを有限体 $F_p$ の上で書き直すと、大量の多項式の等式になる。
たとえば「$z = x × y$」は「$z - x·y = 0$」っていう制約。ネットワーク全体で数十万〜数百万個の制約ができる。
ユキ: ふむふむ。
リルル先生: で、ゼロ知識証明がやってるのは——
「これらの制約を全部同時に満たすような値の組(witness)を、私は知っています」
ということを、witnessを見せずに証明すること。
witnessにはモデルの重み、入力データ、中間計算値、出力が全部含まれてる。制約を全部満たすってことは、正しいモデルで正しいデータから正しく計算したってこと。
カイト: 制約を$1$個でも満たさなかったら、証明が通らないわけですね。
リルル先生: そう。途中で値を1箇所でも改竄したら、そこの制約が壊れて、証明全体が成立しなくなる。
ユキ: モデルが別のやつにすり替えられてないことは?
リルル先生: モデルの重みのハッシュ値(コミットメント)を事前に公開しておく。証明の中で「私が使った重みはこのコミットメントに対応するものです」っていう制約も含める。別のモデルにすり替えたら、コミットメントが合わなくなって証明が通らない。
リン: 多項式コミットメント(KZGなど)の binding 性ですね。
リルル先生: そう。全体をまとめると——
- ネットワークの計算を有限体上の多項式制約に変換する
- 正しい計算のwitnessは全制約を満たす
- 改竄した計算は制約を破るので証明を作れない
- 検証者はランダムチャレンジで多項式がゼロかどうかを確認
- 嘘が通る確率は $d/p ≈ 10^{-71}$
- モデルのすり替えはコミットメントで防止
だから有限体上のNNの計算を使って、改竄なく指定モデルで計算されたことを数学的に保証できる。
第9話 完全準同型暗号って何? —— 暗号化したまま計算する魔法
ユキ: ZKMLの話はだいぶ分かってきました。でも、さっきから「FHE」っていうのも出てきてますよね?
リルル先生: うん、FHEは完全準同型暗号。ZKMLとは別の技術だけど、同じ数学的基盤を共有してる。
ユキ、こういう状況を想像して。あなたが病気の検査データを持ってる。AIで診断してほしいけど、データを他人に見られたくない。
ユキ: クラウドにアップロードしたら、AI企業がデータを見ちゃいますよね。
リルル先生: 普通はそう。でもFHEを使うとこうなる。
- あなたがデータを暗号化してAI企業に送る
- AI企業は暗号化されたままのデータでニューラルネットワークの計算をする
- 暗号化されたままの結果があなたに返ってくる
- あなたは自分の秘密鍵で結果だけを復号する
AI企業はデータの中身を一度も見ていない。
ユキ: ええっ!? 暗号化されたまま計算できるんですか!?
リルル先生: できる。それがFHEのすごいところ。
ユキ: でも、暗号化された数字を足したり掛けたりって、どうやるんですか?
リルル先生: いい質問。普通の暗号だと、暗号化された値同士を足しても意味不明な値にしかならない。でもFHEは特殊な暗号方式で、暗号化されたまま足し算と掛け算ができるように設計されてる。
イメージとしては、鍵のかかった箱の中で計算する感じ。箱を開けなくても、外から特定の操作をすると、中の数字が足されたり掛けられたりする。で、最後に鍵を持ってる人だけが箱を開けて結果を見られる。
カイト: 数学的には、CKKSスキームだと円分多項式環上の演算ですよね。「暗号化されたまま足し算」は暗号文の加算、「暗号化されたまま掛け算」は暗号文の乗算に対応する。
リルル先生: そう。で、FHEでもニューラルネットワークの線形演算(行列積やバイアス加算)は暗号化されたまま実行できる。問題はReLUみたいな非線形関数。CKKSスキームでは多項式近似(チェビシェフ多項式とか)で対応するし、TFHE/CGGIスキームではプログラマブル・ブートストラップで任意の関数をルックアップ的に計算する。
ユキ: FHEとZKMLって何が違うんですか?
リルル先生: 良い質問。守ってるものが違う。
- FHE: データのプライバシーを守る。計算する人がデータの中身を見れない。
- ZKML: 計算の正当性を証明する。計算が正しかったことを第三者が確認できる。
理想的には両方欲しいよね。データも秘密、計算も正しい、っていう。だから最近はFHE+ZKPの合わせ技が研究されてる。FHEで暗号化したまま計算して、ZKPでその計算の正しさを証明する。
リン: Chimera(Boura et al.)のCGGI/CKKS/BFV間のスキーム変換ですね。
リルル先生: そう。まだ研究段階だけど、組み合わせの方向性はかなり有望。
ユキ: FHEでもニューラルネットワークが有限体みたいな構造の上で動くんですか?
リルル先生: 鋭い。CKKSスキームは「多項式環の剰余環」の上で動くんだけど、中国剰余定理(CRT)を適用すると各スロットが有限体 F_p の元に対応する。だから本質的には有限体上の並列演算として理解できる。「有限体の上のニューラルネットワーク」はZKMLとFHEの両方に共通する数学的基盤なんだよ。
第10話 計算にどれくらい時間がかかるの?
ユキ: で、実際にやるとどれくらい時間がかかるんですか? リアルタイムでできるレベル?
リルル先生: 正直に言うと、まだ重い。でもどんどん速くなってる。具体的な数字を出すね。
ZKML(AIの推論に対するZK証明):
| 処理内容 | 証明生成時間 | 検証時間 |
|---|---|---|
| 小さなモデル(画像分類など) | 2.5秒〜 | ミリ秒以下 |
| 中規模(レコメンドモデル等) | 数分〜数十分 | 数秒 |
| GPT-2(蒸留版) | 約1時間 | 数秒 |
| LLaMA-2-13B | 約13分/プロンプト | 0.006秒未満 |
ユキ: 検証がめちゃくちゃ速い!
リルル先生: これがZKPの核心的な非対称性。「証明を作るのは重いけど、確認するのは一瞬」。AWSが1時間かけてGPUで証明を作って、あなたのスマホが50ミリ秒で検証する。このモデルが成立するんだよ。
FHE(暗号化したまま推論):
| 処理内容 | 推論時間 |
|---|---|
| MNIST(小さなNN、GPU加速) | 0.04秒/画像 |
| CIFAR-10画像分類 | 約47秒〜2000秒/画像 |
| ResNet-110 | 約3.6時間/画像 |
| BERT-base(Transformer) | 約18分/推論 |
カイト: FHEは深いネットワークだとブートストラップが支配的で一気に重くなるんですよね。
リルル先生: そう、ブートストラップが推論時間の75〜84%を占める。ただしGPU加速でMNISTの0.04秒みたいにリアルタイムに近い速度も出始めてる。
まとめると、今のところチャットAIみたいなリアルタイム応答には厳しいけど、融資審査・医療診断・監査みたいなバッチ処理なら十分実用的。2026年にかけてGPU最適化で5-10倍、分散証明でさらに高速化の見込み。
第11話 誰が使ってるの? —— 企業の製品とサービス
ユキ: 実際にこの技術を使ってるサービスってあるんですか?
リルル先生: いくつかあるよ。
Worldcoin(現World)。 あの目をスキャンする球体デバイス「Orb」で有名なところ。虹彩スキャンとZKPを組み合わせた本人確認システム「World ID」を運用してる。虹彩からアイリスコードを生成する過程をZK証明で保護して、「この人は一意の人間である」ことをプライバシーを守りながら証明する。World Appユーザー約3300万人、うちOrb認証済み約1500万人(2025年9月時点)で、実世界で最も大規模なZKML応用の一つ。
EZKL(Zkonduit社)。 PyTorchモデルをONNXで出力して、Halo2ベースのZK-SNARKに自動変換するオープンソースライブラリ。Trail of Bitsのセキュリティ監査済み。DeFiの信用スコアリングからゲームAIまで広く使われてる。BitTensor(分散AIネットワーク)のコンセンサスにも採用が進んでる。
Modulus Labs。 オンチェーンAIの検証基盤。1800万パラメータのモデルのオンチェーン検証を実証。AIトレーディングボット「RockyBot」で、取引戦略がZK証明で保証される。Ion Protocol、Lyra Financeと提携。
Giza。 StarkNet上でMLモデルの検証可能実行を提供。Yearn Finance v3のリスク評価エンジンをZKMLで構築。
Zama。 FHEライブラリ「Concrete ML」を提供。暗号化したままの推論を開発者フレンドリーなAPIで実現。
ユキ: Worldcoinってあの目をスキャンするやつ! ZKMLだったんだ。
リルル先生: あとSpectralはWeb3クレジットスコアリングにEZKLを使ってるし、AI Arenaはゲーム内AIの経済モデルにzkMLを導入してる。a16zやPolychainがModulus Labs、Worldcoin、Ingonyama(ZKPハードウェア)に大型投資してて、2030年までにWeb3だけで900億件のZK証明が必要、市場規模約100億ドルって推計もある。
第12話 研究の歴史 —— 8年で「不可能」が「実用」になった
カイト: この分野って、いつ頃から始まったんですか?
リルル先生: 意外と最近だよ。
2017年。 SecureML(Mohassel & Zhang)が「暗号でMLのプライバシーを守る」方向を示した。ただしZKPじゃなくMPC(秘密分散計算)ベース。
2020年。 ZhangらがZKPでNN推論を証明する問題設定を明確化。vCNN発表。
2021年。 zkCNN、ZEN、Mystique が立て続けに登場。zkCNNはGKRプロトコルを畳み込みに特化させた画期的な研究。
2022年。 WorldcoinチームがZKMLコミュニティを組織。EZKL(Zkonduit社)が実用ワークフローを確立。
2024年。 Kang et al.がEuroSysで、Twitter(X)のレコメンドモデルや蒸留GPT-2のZK-SNARKを実証。zkLLM(CCS 2024)がLLMアテンション機構の専用プロトコルを提案。
2025年。 DeepProve-1がGPT-2の完全推論のZK証明を初めて生成。「検証可能な生成AIの Hello World」。
リン: DeepProveのGKRアプローチはEZKL比で50-150倍高速化。TeleSparse(PETS 2025)のニューラルテレポーテーションによるZKフレンドリーモデル設計、zkPyTorchのLLaMA-3対応も注目ですね。
リルル先生: 8年でここまで来た。しかもまだ加速中。
第13話 今後の展望
リルル先生: 最後に、これからどうなるか。
ユキ向け: ブロックチェーン上でAI推論を誰でも検証できる世界がすぐそこ。暗号化したまま医療診断する時代。カメラがZK証明を発行してディープフェイクに対抗。
カイト向け: ZKフレンドリーなモデル設計(多項式活性化、ニューラルテレポーテーション)。再帰的証明(IVC, Nova)で深いNNを層ごとに証明・集約。FHEコンパイラ(Concrete, HEaaN, SEAL)の成熟。
リン向け: LLMスケールZKPはストリーミング証明(2026年)と分散証明が鍵。検証可能な訓練はSGDランダム性が根本課題で未踏。AG符号によるSTARK効率改善。格子暗号ベースSNARKとハッシュベースSTARKのポスト量子安全性。形式検証とZKPの自動化パイプライン。
おわりに
リルル先生: 全部繋げるとこうなる。
「ニューラルネットワークを有限体の上で動かす」——この一見奇妙な問題設定が、AIの信頼性・プライバシー・検証可能性という現代の最も差し迫った課題の解決策になってる。
銀行のAIが融資判断するとき、その計算が正しかったことを暗号学的に証明できる。企業がモデルの秘密を守りながら性能を証明できる。カメラが撮影の瞬間にデジタル証明書を発行して、ディープフェイクに対抗できる。
その奥にある数学——有限体、多項式理論、楕円曲線、代数幾何、計算複雑性理論——は美しくて、驚くほど実用的。
ユキ: 有限体って最初「余りの世界」って聞いてピンと来なかったけど、こんなにすごい応用があるんですね。
カイト: 代数と暗号とAIが全部繋がるの、面白すぎません?
リン: AG符号のSTARK応用、テーマにしたいかも。
リルル先生: いいね。この分野は数学が美しくて、しかも実用的。今後10年でAIと暗号の交差点で最も重要なトピックの一つになるよ。
さて、チーズケーキもう一切れいる?
参考文献(主要なもの)
- Mohassel, P. & Zhang, Y. (2017). "SecureML." IEEE S&P.
- Liu, T., Xie, X. & Zhang, Y. (2021). "zkCNN." CCS.
- Feng, B. et al. (2021). "ZEN." Cryptology ePrint.
- Coglio, A. et al. (2023). "Formal Verification of Zero-Knowledge Circuits."
- Kang, D. et al. (2024). "ZKML." EuroSys.
- Sun, H., Li, J. & Zhang, H. (2024). "zkLLM." CCS.
- South, T. et al. (2024). "Verifiable evaluations of ML models using zkSNARKs." arXiv.
- Lagrange Labs. (2025). "DeepProve-1."
- Maheri, M. et al. (2025). "TeleSparse." PETS.
- Peng, Z. et al. (2025). "Survey of ZKP Based Verifiable ML." arXiv.
- Hong, C. (2025). "FHE-based privacy-preserving ML." Security and Safety.
- Ebel, A. et al. (2025). "Orion: FHE for Deep Learning." arXiv.