Certified but Private: Scalable Zero-Knowledge Proofs for Neural Network Guarantees
Youwei Zhong, Ben Merbaum, Timos Antonopoulos, Ning Luo, Charalampos Papamanthou, Katerina Sotiraki, Ruzica Piskac
cs.LG, cs.CR, cs.LO
2026-08-18
耶鲁团队把 CROWN 鲁棒性认证搬进零知识证明：290 万参数网络 5 分钟出证明、10 秒验证，比此前 ZK 方案大 4 个数量级，模型权重全程不泄漏。
监管和商业场景越来越要求模型给出鲁棒性的形式化保证：输入做微小扰动，预测不能翻转。可形式化验证工具要拿到模型权重才能跑，而权重恰恰是模型方最不能交出去的：既是商业机密，还可能通过白盒攻击反推出训练数据（医疗场景下这直接违反 HIPAA）。此前的出路只有 FairProof 一类的零知识证明方案，靠枚举所有神经元激活组合来验证，复杂度随网络规模指数增长，实测只能跑约 100 参数的玩具网络。这篇让模型方在不出示权重的前提下向任何人证明「模型在给定扰动半径内鲁棒」，证明可公开验证、可存档。
PANDA 的底座是 CROWN，2018 年提出的线性界传播鲁棒性认证框架，α-CROWN 等 SOTA 验证器的内核。CROWN 的思路：对每层激活函数找一对线性上下界夹住它，然后逐层反向传播线性界，最后把线性界在扰动球上取最大值，得到输出差的上界；上界不超过零即认证通过。多项式时间，但不完整：过近似的方法能证真不能证假。
把 CROWN 搬进零知识证明，最贵的一步是「选松弛线」。CROWN 原版要解一个方程迭代搜索最优切线，这个搜索在 ZK 电路里做代价极高。PANDA 的核心原则是「明文里算，电路里验」：证明者在电路外跑完整 CROWN，把选好的松弛系数作为见证（witness）提交，电路里只验证这些系数满足一组简化约束。验证一个神经元激活函数的线性界，原本要检查整个连续区间（无穷多点），PANDA 把它化成四个点上的不等式，即四点松弛 gadget：对 sigmoid、tanh、arctan 这类 S 形激活，端点两个、切点两个，查这四处就足够可靠。为避免在电路里暴露「切点在不在区间内」这类分支信息（会泄漏权重），判据设计成无条件版本。
工程上三件配套：实数运算全部量化成有限域整数（沿袭 zkML 惯例，14 比特），取整余数也进电路证明；不用通用 ZK 后端，自组 Hyrax 多项式承诺、Thaler 矩阵乘法证明、LogUp-GKR 查找证明三件套，按操作类型分别调最合适的原语；ReLU 网络单独一套更便宜的判据（割线加过原点的线，查两个点即可）。证明者时间与神经元数多项式相关，继承 CROWN 的 O(m²n³)。
MNIST 上 4×[1024]（四层、每层 1024 神经元、290 万参数）：证明 5.5 分钟，验证 14 秒，证明文件 31-32 MB。此前 ZK 鲁棒性验证的最大规模约 100 参数，扩大 4 个数量级。
| 模型 | 激活 | 证明 (s) | 验证 (s) | 证明大小 (MB) |
| 2×[20] | ReLU | 22.8 | 0.97 | 3 |
| 3×[1024] | ReLU | 101.6 | 4.6 | 9 |
| 4×[1024] | Sigmoid | 327.5 | 14.1 | 31 |
| 4×[1024] | Tanh | 333.9 | 14.3 | 32 |
对照数据：比明文 CROWN 慢约 100-1000 倍（验证慢 20-50 倍），这是隐私的价格；换 sigmoid/tanh 比纯 ReLU 贵 1.5-2.6 倍。与 FairProof 唯一可跑的对照（Adult 数据集两层 8/2 神经元小网）：PANDA 证明 34.89 秒对 FairProof 全程 66.0 秒；FairProof 在 MNIST 2×[20] 上五个测试四个超时（>1 小时）、一个内存爆掉（>512 GiB）。量化漂移方面，PANDA 能验证 CROWN 验证的所有断言，数值漂移最大 12.6%（那个 Adult 小网），MNIST 大网在 0.5% 以内。
AI 法规（欧盟 AI Act 一类）正在把「可证明的鲁棒性」变成高风险场景的准入条件，医院、车厂、金融风控都需要向第三方证明模型可靠，但谁也不会交权重。PANDA 第一次让这两件事同时成立，且规模到了实用区间，290 万参数对 MNIST 级分类器是真实尺寸，虽然离 LLM 还很远。对做模型审计平台的人，这是一条可直接抄的路线：验证算法在电路外跑、电路里只查约束，这个「算验分离」原则适用于任何想把现有验证器 ZK 化的团队。
渐进属性也要说清：它没有发明新的验证算法，CROWN 的认证能力原样继承，贡献全在 ZK 化的工程与算法设计上。
作者自述三条：只能证量化后的模型，不能直接证浮点模型；架构、层维度、激活函数类型都是公开信息，只藏权重（可加假层混淆，但代价自付）；继承 CROWN 的不完整性：过近似验证器能证真能力有限，证不了「不鲁棒」，认证通过率低于完整验证器。
读下来还有几点。实现用的是三个底层协议的非零知识变体，「泄漏只剩小常数因子」是估计不是实测，安全攸关场景要等零知识变体的实测数据。FairProof 的离线阶段没有官方发布，对比实验是作者自己重实现的，公平性依赖重实现质量。最关键的是规模天花板没破：290 万参数是全连接网，卷积、Transformer、任何 LLM 都没有碰，zkML 社区真正卡着的推理验证（DeepProve、zkGPT 那条线）做的是另一件事，这篇的方法能不能搬过去没有讨论。