认证但私密:面向神经网络保证的可扩展零知识证明
摘要
PANDA 是一个可扩展的系统,使用零知识证明来验证神经网络的鲁棒性和公平性,无需揭示模型参数,从而能够对具有多项式复杂度的大型网络进行认证。
arXiv:2608.17070v1 公告类型:新
摘要:随着机器学习模型的广泛部署,这些模型的鲁棒性和公平性的形式化保证在安全关键和法律合规环境中变得越来越重要。然而,模型参数通常是商业秘密,不能泄露给审计师或最终用户。为此,我们提出了 PANDA,一个可扩展的系统,它使用零知识证明 (ZKPs) 来证明模型的鲁棒性和公平性属性,无需揭示其私有参数。PANDA 构建在 CROWN 之上,CROWN 是一个高效的鲁棒性认证框架,被许多用于神经网络的最新形式化验证工具所采用。PANDA 的核心贡献是一种新颖的算法,用于证明非线性激活层的线性松弛界,产生简单、轻量的证明。值得注意的是,我们的系统可以在5分钟内为超过290万参数的神经网络生成局部鲁棒性证明,并在10秒内验证它们。先前的基于 ZKP 的鲁棒性系统依赖于指数时间算法,无法扩展到非平凡网络。相比之下,PANDA 在网络神经元数量上呈多项式扩展,使我们能够支持比先前方法大4个数量级的神经网络,同时显著减少证明者的开销。
查看缓存全文
缓存时间: 2026/08/19 10:20
# 认证但保密:可扩展的神经网络保证零知识证明
来源:https://arxiv.org/html/2608.17070
###### 摘要
随着机器学习模型的广泛部署,其鲁棒性和公平性的形式化保证在安全关键和法律合规场景中变得愈发重要。然而,模型参数通常是商业机密,无法向审计员或最终用户披露。为此,我们提出PANDA,一个可扩展的系统,利用零知识证明(ZKP)在不泄露模型私有参数的情况下,证明模型的鲁棒性和公平性属性。PANDA基于CROWN构建,后者是一个高效的鲁棒性认证框架,被许多尖端神经网络形式化验证工具所采用。PANDA的核心贡献在于提出了一种新颖的算法,用于证明非线性激活层的线性松弛界,从而生成简洁、轻量级的证明。值得注意的是,我们的系统能够在5分钟内为拥有超过290万参数的神经网络生成局部鲁棒性证明,并在10秒内完成验证。此前的基于ZKP的鲁棒性系统依赖于指数时间算法,无法扩展至非平凡网络。相比之下,PANDA的时间复杂度与网络中神经元数量呈多项式关系,使我们能够支持比之前方法大4个数量级的神经网络,同时显著降低了证明者的开销。
## 1 引言
机器学习(ML)模型若在输入发生微小扰动时,其输出不会产生巨大或不可预测的变化,则该模型被认为是*鲁棒的*。随着ML系统在医疗、自动驾驶、金融决策等安全关键场景中日益普及,可扩展的形式化验证鲁棒性方法变得至关重要。除模型所有者自身对可靠性的关注外,监管机构和下游客户也越来越多地要求形式化的鲁棒性保证[15 (https://arxiv.org/html/2608.17070#bib.bib22), 10 (https://arxiv.org/html/2608.17070#bib.bib23)]。例如,医院可能训练一个临床模型,根据报告的症状预测患者风险水平。决定是否部署该模型的用户自然需要确信模型是鲁棒的:对患者报告症状的微小扰动(如拼写错误或同义词替换)不应改变预测风险水平。形式化地,考虑一个分类模型,其输入为向量\(\boldsymbol{x}\)(可编码图像),并输出预测标签。标准的*局部鲁棒性*概念要求,对于给定输入\(\boldsymbol{x}_0\),所有足够接近(相对于参数\(\varepsilon\))的输入应获得相同的预测。该属性可形式化为:
\(\forall \boldsymbol{x}.\ \|\boldsymbol{x} - \boldsymbol{x}_0\| < \varepsilon \Rightarrow \mathrm{Classification}(\boldsymbol{x}) = \mathrm{Classification}(\boldsymbol{x}_0)\)。 (1)
证明局部鲁棒性属性的一种方法是向用户或第三方审计员提供对模型参数的完全访问。然而,现代ML模型是宝贵的知识产权。网络在专有数据集上训练,暴露模型参数可能导致复杂的白盒攻击[20 (https://arxiv.org/html/2608.17070#bib.bib27)]并泄露训练数据信息[9 (https://arxiv.org/html/2608.17070#bib.bib28)]。在上述医疗场景中,医院不能泄露模型权重,因为这可能揭示受保护的患者健康信息并违反HIPAA法规。
验证性与模型机密性之间的紧张关系可以通过*零知识证明*(ZKP)[8 (https://arxiv.org/html/2608.17070#bib.bib12)]这一密码学原语来解决。该原语使证明者能够使验证者确信某个陈述成立,且不泄露除陈述有效性之外的任何信息。一个不断发展的研究方向——zkML——已使用ZKP隐藏ML相关计算中的模型参数[22 (https://arxiv.org/html/2608.17070#bib.bib16), 6 (https://arxiv.org/html/2608.17070#bib.bib29)]。然而,其中大多数聚焦于隐私保护的ML推理和训练完整性,局部鲁棒性相对研究不足。考虑相关*公平性*概念的现有工作[31 (https://arxiv.org/html/2608.17070#bib.bib17)]仅能支持参数约≈100的模型,规模过小,无法用于现实应用。
形式化验证的最新进展使得深度神经网络(DNN)的快速鲁棒性认证成为可能,但这些工具会泄露模型信息[4 (https://arxiv.org/html/2608.17070#bib.bib2), 7 (https://arxiv.org/html/2608.17070#bib.bib1)]。一个自然的想法是将鲁棒性认证算法与ZKP结合,以隐藏模型参数并继承底层算法的高效性和可扩展性。然而,这种组合引入了若干技术挑战:ZKP原生处理线性函数,必须适配以处理非线性激活函数。此外,ZKP通常不兼容浮点运算。最后,在ZKP内执行计算会在证明时间上引入显著开销,可能阻碍其扩展至大型现实DNN。这引出了以下问题:我们能否在零知识环境下验证大型神经网络的局部鲁棒性属性?
我们对此问题给出了肯定回答。在本文中,我们提出PANDA(基于自动神经网络派生仿射边界的证明),该系统将ZKP与CROWN验证算法[32 (https://arxiv.org/html/2608.17070#bib.bib3)]相结合,生成可公开验证的神经网络局部鲁棒性证明。CROWN是一种高效的线性边界传播方法,是许多尖端神经网络验证系统[30 (https://arxiv.org/html/2608.17070#bib.bib5), 29 (https://arxiv.org/html/2608.17070#bib.bib4), 3 (https://arxiv.org/html/2608.17070#bib.bib6)]的基础。通过将CROWN集成到零知识框架中,PANDA使模型所有者能够在保持底层模型参数私有的同时认证鲁棒性属性。据我们所知,PANDA是迄今为止证明私有神经网络局部鲁棒性最高效、最可扩展的ZKP系统。PANDA支持多达290万参数的网络,超过先前方法4个数量级以上,证明时间为5分钟,验证时间为10秒。此外,证明者运行时间与网络中神经元数量呈多项式关系,使得对比之前可能大得多的模型进行实际认证成为可能。PANDA也是首个支持具有超越激活函数(如sigmoid和tanh)的DNN的隐私保护局部鲁棒性认证系统。
我们引入了一种新方法,通过评估四个点态不等式来验证激活函数在连续区间上的线性松弛,从而生成ZK友好的检查。
**技术亮点**。我们提出了一种*认证算法*,能够在ZKP内不执行完整计算轨迹的情况下验证计算正确性,极大提升了PANDA的效率。具体而言,CROWN算法需要寻找一对线性下界和上界,使激活函数在给定区间内被夹住。CROWN通过代价高昂的迭代搜索[32 (https://arxiv.org/html/2608.17070#bib.bib3)]选择合适的边界。我们观察到,此搜索可在ZKP外执行以降低证明者开销,然后计算得到的上下界可通过简单的约束系统进行验证,我们称之为*四点松弛小工具*(第5节[https://arxiv.org/html/2608.17070#S5])。这一原则贯穿PANDA:证明者首先在ZKP外执行CROWN算法,然后在ZKP内通过简化的约束系统对其结果进行认证。
我们没有使用通用ZKP后端,而是设计了*定制化后端*,利用不同的密码学原语来证明不同操作。这使得PANDA能够实现比先前工作更高的证明者效率,并扩展到更大规模的网络。
## 2 预备知识
*零知识证明*(ZKP)允许证明者\(\mathcal{P}\)使验证者\(\mathcal{V}\)确信一个公共陈述\(x\)成立,且不泄露关于其成立原因的进一步信息。解释“原因”的私有信息称为*见证*\(w\)。例如,公共陈述\(x\)可能是ML模型在给定点具有局部鲁棒性,而私有见证\(w\)包含私有模型权重和计算中产生的辅助值。\(\mathcal{P}\)使用\(x\)和\(w\)输出证明\(\pi\),\(\mathcal{V}\)连同\(x\)一起验证\(\pi\),并接受或拒绝。
*承诺并证明*ZKP系统使\(\mathcal{P}\)能够首先为见证\(w\)生成承诺\(c_w\),该承诺具有*隐藏性*(\(c_w\)不泄露任何关于\(w\)的信息)和*绑定性*(\(\mathcal{P}\)无法找到不同的见证\(w' \neq w\)对应于\(c_w\))。承诺\(c_w\)是公共陈述\(x\)的一部分,\(\mathcal{P}\)的主张是\(\mathcal{P}\)知道一个见证\(w\),其承诺为\(c_w\),且\(w\)是\(x\)的有效见证。
PANDA是一个承诺并证明的ZKP系统,使用三种底层密码学原语:
1. **多项式承诺方案**\(\Pi_{\textsc{com}}\),包含三个算法:
* **承诺**(由\(\mathcal{P}\)运行):输入多项式\(f\),输出对\(f\)的承诺\(c_f\),该承诺是隐藏且绑定的。
* **求值**(由\(\mathcal{P}\)运行):输入\(f\)、点\(x\)和值\(y\),输出证明\(\pi\)(也称为*开放*),声称\(y = f(x)\)。
* **验证**(由\(\mathcal{V}\)运行):输入\(c_f, x, y, \pi\),接受或拒绝。
\(\Pi_{\textsc{com}}\)是*完备的*,如果当\(c_f \leftarrow \textsc{Commit}(f)\),\(y = f(x)\),且\(\pi \leftarrow \textsc{Eval}(f, x, y)\)时,\(\textsc{Verify}\)接受。
我们说\(\Pi_{\textsc{com}}\)是*求值绑定的*,如果恶意的\(\mathcal{P}\)不能在\(y \neq f(x)\)的情况下为\(x, y\)生成可接受的证明\(\pi\)。
我们说\(\Pi_{\textsc{com}}\)是*零知识的*,如果\(\pi\)不泄露关于\(f\)的任何信息。
2. **用于矩阵算术的ZKP** \(\Pi_{\textsc{arith}}\)。我们可以使用插值将矩阵或向量编码为多项式,然后使用\(\Pi_{\textsc{com}}\)对矩阵或向量进行承诺。
* 私有见证\(w\)是矩阵列表(例如 \(\mathbf{A, B, C, D}\))。
* 公共陈述\(x\)是对这些矩阵的承诺列表(例如 \(c_A, c_B, c_C, c_D\))以及它们之间声称的算术关系(例如 \(\mathbf{A = BC + D}\))。
* \(\mathcal{P}\)向\(\mathcal{V}\)证明\(\mathcal{P}\)知道\(w\)中的矩阵,其承诺与\(x\)中的匹配,并满足该矩阵算术等式。
3. **用于表查找的ZKP** \(\Pi_{\textsc{lookup}}\)(也称为*查找论证*)。
* 私有见证\(w\)是查找向量\(\boldsymbol{a}\)。[1](#fn1)
* 公共陈述\(x\)是对\(\boldsymbol{a}\)的承诺\(c_a\)以及一个表向量\(\boldsymbol{t}\)。
* \(\mathcal{P}\)向\(\mathcal{V}\)证明\(\mathcal{P}\)知道一个向量\(\boldsymbol{a}\),其承诺为\(c_a\),且\(\boldsymbol{a}\)的每个条目都在表\(\boldsymbol{t}\)中。
\(\Pi_{\textsc{arith}}\)和\(\Pi_{\textsc{lookup}}\)各包含两个算法:
* **证明**(由\(\mathcal{P}\)运行):输入\(w\)和\(x\),输出证明\(\pi\)。作为子程序,\(\mathcal{P}\)通过\(\Pi_{\textsc{com}}.\textsc{Eval}\)生成见证掩码版本的开放。
* **验证**(由\(\mathcal{V}\)运行):输入\(x\)和\(\pi\),接受或拒绝。作为子程序,\(\mathcal{V}\)调用\(\Pi_{\textsc{com}}.\textsc{Verify}\)检查开放证明(包含在\(\pi\)中)。
我们说ZKP是*完备的*,如果每当\(w\)是\(x\)的有效见证时,\(\textsc{Verify}\)接受由\(\textsc{Prove}\)生成的证明\(\pi\)。ZKP是*可靠的*,如果每当\(x\)是无效陈述时,任何计算有界的证明者都无法伪造使\(\textsc{Verify}\)接受的证明\(\pi\)。ZKP是*零知识的*,如果\(\pi\)除了泄露\(w\)存在这一事实外,不泄露关于\(w\)的任何信息。
\(\Pi_{\textsc{lookup}}\)可用于*范围证明*ZKP,证明向量\(\boldsymbol{a}\)的每个元素位于区间\([l, r]\)内。这只需设置表向量\(\boldsymbol{t} = (l, l+1, \dots, r)\)即可实现。我们常将单边范围证明写为\(\boldsymbol{a} \geq 0\),其中\(l=0\),\(r\)隐式选择为\(\boldsymbol{a}\)中元素可达的最大值(取决于量化)。
\(\Pi_{\textsc{lookup}}\)还可证明*非线性函数求值*;即对于一组点\(\{(x_i, y_i)\}_{i \in [n]}\)和一个非线性函数\(f\),\(\Pi_{\textsc{lookup}}\)证明对于每个\(i \in [n]\),\(f(x_i) = y_i\)。这通过设置\(\boldsymbol{a} = \left\{(x_i, y_i)\right\}_{i \in [n]}\)和\(\boldsymbol{t} = \left\{(z, f(z))\right\}_z\)实现,其中\(z\)在定义域中取所有可能值。
**量化**。大多数现有ZKP不兼容浮点计算。遵循先前zkML论文[22 (https://arxiv.org/html/2608.17070#bib.bib16), 6 (https://arxiv.org/html/2608.17070#bib.bib29)]的先例,我们执行*量化*,将所有计算转换为有限域算术。我们遵循[11 (https://arxiv.org/html/2608.17070#bib.bib24)]中介绍的量化方法,其中每个实数\(x\)由\(Q\)位整数\(q_x \in [0, 2^Q)\)表示,满足\(x \cdot S_x \approx q_x\),其中缩放因子\(S_x \gg 1\)经过优化选择。神经网络中的每层矩阵和张量通常共享单个缩放因子,模型权重和偏差均用其初始化。要对两个值\(x\)和\(y\)求和,我们首先重新缩放它们以共享相同的缩放因子,然后对量化整数\(q_x\)和\(q_y\)求和。要对两个值\(x\)和\(y\)相乘,我们对量化整数\(q_x\)和\(q_y\)相乘,并将乘积的缩放因子设置为\(S_x S_y\)。要将\(q_x \approx x \cdot S_x\)重新缩放至某个新缩放因子\(S_z\),我们计算\(q_z = \left\lfloor S_z q_x / S_x \right\rfloor\)。
## 3 CROWN 算法
本节回顾CROWN算法[32 (https://arxiv.org/html/2608.17070#bib.bib3)],它是我们的PANDA零知识协议的关键构建模块。我们以与ZKP系统兼容的方式呈现算法的每个步骤。CROWN算法的完整细节见附录A.1 [https://arxiv.org/html/2608.17070#A1.SS1]。
### 3.1 设定与目标
我们考虑一个\(m\)层前馈网络\(f: \mathbb{R}^{n_0} \to \mathbb{R}^{n_m}\),由以下递归定义:
\[
\boldsymbol{z}^{(k)} = \mathbf{W}^{(k)} \boldsymbol{h}^{(k-1)} + \boldsymbol{b}^{(k)} \in \mathbb{R}^{n_k}, \quad
\boldsymbol{h}^{(k)} = \sigma(\boldsymbol{z}^{(k)}) \in \mathbb{R}^{n_k}
\]
其中\(\mathbf{W}^{(k)}\)和\(\boldsymbol{b}^{(k)}\)是第\(k\)层的权重矩阵和偏差向量,\(\sigma\)是激活函数。相似文章
神经网络的安全保障真的安全吗?如何计算可信的鲁棒性认证
本文介绍了用于计算神经网络可信鲁棒性认证的瓣心距度量(apothem measure),证明了体积最优认证的难解性,并提出了ParallelepipedoNN系统,在MNIST和Fashion MNIST数据集上实现了最小边长两倍的提升。
揭示神经网络证明共享的极限
本文对基于模板的神经网络鲁棒性验证加速进行系统性研究,并介绍了FastCert,一种自动分配模板以提高性能的技术。
可证明安全的智能体护栏
本文提出了一种新的AI智能体安全范式,采用带有神经符号隔离的可执行证明约束动作(ePCA)框架,实证评估中实现了零攻击成功率。
Verified SHAP: 神经网络精确Shapley值的可证明边界
提出了一种基于验证的算法,用于计算神经网络精确SHAP值的可证明边界,可扩展到比先前精确方法大得多的搜索空间。
在最小过参数化下,从示例中认证对电路和Transformer是困难的
本文研究神经网络的精确认证问题,表明即使在最小过参数化下,认证对于深度≥2的阈值电路和对数精度Transformer也可能变得指数级困难。它还描述了近似认证,揭示了允许多项式级错误仍然需要指数级规模的证书。