zkLLM:不公开模型参数,怎样证明一次推理算对了?——论文阅读笔记
论文:zkLLM: Zero Knowledge Proofs for Large Language Models
作者:Haochen Sun、Jason Li、Hongyang Zhang
发表:ACM Conference on Computer and Communications Security(CCS),2024
关键词:可验证推理、模型参数隐私、tlookup、zkAttn、sumcheck、多项式承诺
原文:作者公开的会议版 · DOI
1. 背景与动机:为什么需要证明一次 LLM 推理?
1.1 Background:看到 API 回答,看不到它怎样产生
假设一家服务商说,它部署了模型 A。用户输入问题,API 返回一段回答。仅凭这些文字,检查者无法确认:服务商是否真的运行了 A,是否换成成本更低的模型 B,或者是否在返回前修改了结果。
在普通使用中,这可能只是服务可信度问题;在模型审计中,它会影响证据本身。如果要通过指定提示观察某个模型的行为,首先必须确认收到的确实是该模型按规定计算产生的结果。
1.2 Motivation:核实计算来源,又不能直接公开权重
公开模型参数、让检查者重新运行,是一种直接路径,但与模型所有者保护知识产权的需求冲突。大型模型的重新执行也需要资源。因此,本文要解决的矛盾是:检查者需要核实推理计算,模型所有者又不希望公开权重。
零知识可验证计算为二者提供一条兼容路径:模型所有者执行推理,并证明它遵循了指定关系;验证者检查证明,而不需要取得秘密权重。但通用证明工具能表达这件事,不等于能以可承受的成本处理 LLM。
这就是本文的两层动机:首先,需要保护参数的计算验证;进一步,需要适合大模型结构与规模的证明方法。tlookup、zkAttn 和并行实现分别回应后面这层挑战。
从上周的 Hawk 到这里,可以看到相似的问题意识:持有秘密的一方执行计算,另一方通过证明核查关系。Hawk 还涉及资金与协议公平性;zkLLM 则把主线集中在推理真实性、参数隐私和证明成本上。
1.3 Goal:论文到底要实现什么?
在不公开模型参数的前提下,让验证者确认给定输入的推理结果与已承诺模型一致,并使证明在 LLM 规模上具有可行的时间、内存和验证成本。
这里的“计算正确”有明确范围。模型按自身参数严格执行,仍可能回答错误事实。因此,本文目标是核查执行关系,不自动证明回答符合事实、训练数据合法、模型公平或整体合规。原文以审计为动机,但协议解决的是其中可形式化的计算真实性问题。
图 1:根据论文 §1–§7 整理的主线示意。下面每部分都要回到图中的同一个目标。
2. Desired properties:达成目标,需要哪些性质和设计要求?
2.1 先列要求,再看作者选了什么方法
只说“论文采用零知识证明”还不足以解释设计。需要进一步问:证明到底要保证什么,又为什么必须引入这些具体构件?
下表将安全性质与系统要求放在同一目标下组织;二者不是同一种保证。它是对原文的阅读归纳,不是作者列出的同名清单。tlookup 和 CUDA 是实现手段,不是与隐私性并列的安全性质。
| Desired property / requirement | 为什么实现 Goal 需要它 | 论文怎样回应 | 后文如何判断是否达成 |
|---|---|---|---|
| P1 计算可靠性 | 错误推理不能轻易被当作真实结果 | sumcheck、tlookup、zkAttn 检查相应关系 | §7.2 的可靠性分析及其假设 |
| P2 参数隐私 | 不能以验证为代价公开知识产权 | 隐藏承诺与零知识版本的协议 | §3.6 的设置、§7.2 的零知识论证 |
| P3 模型绑定与连接一致性 | 不能换权重,或把互不相干的合法模块拼成一次推理 | 模型与中间量承诺、求值证明、前后连接约束 | §3.4、§6.2 的数据绑定与证明拼装 |
| P4 非算术可验证且适合并行 | 激活、指数等若展开得昂贵或串行,整网证明就难以扩展 | 保留张量结构的 tlookup,结合专门算术证明与 CUDA | §4 的构造、§7.3 的开销与并行分析;实际耗时需实验 |
| P5 内存、通信与验证负担可承受 | 大表或要求验证者重做大量计算,会削弱方案价值 | zkAttn 的结构分解、小表、相应承诺与批处理 | §7.3 的条件与增长规律,§8 的特定配置结果 |
| P6 数值误差受控 | 不能为了容易证明而任意改变模型计算 | 明确量化规则、分段精度与归一化容差 | §7.1 的局部误差界;整网行为还需更具体证据 |
完备性是另一项基本协议要求:诚实执行应能通过;本文也分析了坏随机点带来的极小失败概率。P1–P6 用来组织主要设计矛盾,不取代完整安全定义。
2.2 从要求找到障碍,再得到作者的 idea
障碍一:非算术操作难以廉价地进入算术证明。 作者的 idea 是先把规定精度下的函数行为表示成合法表,再设计适合张量、可并行的查表证明 tlookup。它主要支撑 P1、P4,但实际隐私与绑定仍需 P2、P3 的基础构件。
障碍二:有了查表,Softmax 仍可能需要无法承受的大表。 作者进一步利用 Softmax 的结构改写任务,采用分段小表与受控近似,并证明它们之间的关系。这就是 zkAttn 的核心路线,重点支撑 P5、P6,同时保持 P1 所需的检查。
障碍三:局部正确还不等于整网正确。 系统按矩阵乘法、激活、归一化、Attention 分工,再沿同一计算图连接证明,最终归约到输入与模型承诺。它使 P3 落实到完整推理,并将前两项技术转为能运行的系统。这里的“第三个 idea”是系统层思路,不是声称作者重新发明了所有拼装技术。
后文按这三个障碍依次展开。本文的一句话贡献可以概括为:以张量查表处理通用非算术关系,以结构化 zkAttn 控制 Attention 的表规模与近似,再将算术与非算术证明连接起来,形成保护参数的 LLM 推理验证系统。
3. 第一个障碍:非算术难证明,为什么想到查表?
这一部分先解释作者 idea 1 的出发点:为了实现 P4,需要让复杂函数进入可以高效核查的关系表示;查表提供这种转换,但还不是完整的证明协议。
3.1 把函数计算改写为合法输入输出关系
用一个简单例子理解。假设只允许整数输入 −2、−1、0、1、2,要计算 ReLU,即负数变为 0,非负数保持不变。可以提前列出:
| 输入 x | 合法输出 y |
|---|---|
| −2 | 0 |
| −1 | 0 |
| 0 | 0 |
| 1 | 1 |
| 2 | 2 |
那么“证明 y 是 x 的正确输出”,就可以转化为“证明 (x,y) 属于这张合法表”。这是教学例子,主要用来说明关系;并不意味着 ReLU 在所有设置下都应优先使用查表。
一个容易忽略的点是:必须检查输入输出配对。 (−1,2) 中,−1 在输入列里,2 也在输出列里,但它们没有组成合法的一行。分别检查输入、输出的取值范围,不能代替函数关系检查。
普通程序查表,是为了取得答案;这里的 lookup argument 则是为了让验证者相信:秘密计算中使用的值符合双方认可的表。实际中间值可以保持秘密,表和规定的运算规则则需要一致。
表本身不会带来零知识性。保密依赖完整协议里的隐藏承诺和零知识处理,不能仅凭“使用查表”就认为数据不会泄露。
3.2 为什么查表有用,又为什么不能无限造表?
对复杂函数直接展开底层证明约束可能很贵。如果输入已经被限定为有限个离散值,就可以提前描述合法结果,再批量证明实际计算符合它。
但这也带来代价:输入范围越大、精度越高,表通常越大。不能为所有实数列一张表,必须先确定量化、编码与有效范围。证明符合离散表,也不自动等于无限精度实数计算,需要另外分析近似误差。
若函数依赖多个输入,情况更明显。每个输入有 N 种可能,n 个输入的直接联合枚举可能达到 N 的 n 次方种组合。一百万次独立的单输入计算可以共享一张表;几个相互依赖的输入,却可能需要枚举它们的组合。 关键在依赖结构,不只是变量总数。
4. Idea 1:tlookup 怎样把查表变成张量证明?
上一节只解决了“合法计算怎样描述”。本节继续回答“秘密值怎样被批量核查”,并把合法性检查连接到 P1 的可靠性、P2 的隐私与 P3 的绑定。
图 2:查表证明的职责示意,不是完整协议时序。输入输出配对编码与约束合并有各自的随机挑战。
4.1 用计数把许多成员关系汇总起来
tlookup 的基础任务是:给定一批秘密值 S 和一张合法表 T,证明 S 的每个元素都来自 T。
例如 T=(2,5,9),S=(5,2,5)。每个表项被使用的次数就是 m=(1,2,0)。按实际值逐个汇总,与按合法表项和次数汇总,应该描述同一批数据。
论文将这个直觉写成有理函数恒等式,再通过随机点检查、sumcheck 和承诺求值证明进行核查。这里不展开长公式,只抓住它的作用:把许多成员检查编码为一项全局代数任务,同时保留张量结构,便于并行处理。
计数不记录顺序,因此它只服务成员合法性。某个值在网络的哪个位置、是否对应前一步输出,仍需其他关系约束。
对于函数关系,论文进一步将输入输出对用随机线性组合编码,再检查它们是否属于同样编码的合法表。这样可以复用成员检查工具,而不是只判断输出值有没有出现在表中。
4.2 随机点检查,不是随机抽一个数组元素
这是阅读中最容易混淆的地方。若有 1000 个结果,其中只有一个错,随机抽一个位置检查,发现错误的概率只有 1/1000。
随机点检查的思路不同:先把整批关系编码成一个多项式,再随机选一个域元素作为输入。例如三个位置的误差是 ,构造教学用的多项式:
若全部正确,误差全为零,E 恒为零;若误差是 (1,−1,0),则 E(t)=1−t,只在 t=1 时为零。在一个 q 元有限域均匀取 t,碰巧通过的概率为 1/q。
这不是论文全部安全概率的公式,只是在解释原理:随机数是编码函数的输入,不是原数组的位置。 非零多项式的根数受次数约束,因此在足够大的域内,可以控制错误关系碰巧通过的概率。
还必须满足两项条件:多项式的次数受约束;证明者不能看到挑战后随意换数据。否则这个概率直觉就失去前提。
4.3 sumcheck 与承诺各自负责哪一段?
张量经过多线性扩展,可以表示为在域内求值的多项式。sumcheck 将大规模求和声明逐轮归约为较少的求值声明,但最后的值仍不能由证明者随口报告。
承诺求值证明负责确认:这些求值确实对应原先承诺的数据。
| 工具 | 主要任务 |
|---|---|
| 多线性扩展 | 把张量编码为可在随机点求值的多项式 |
| sumcheck | 将大规模求和关系归约成较少的求值声明 |
| 承诺的绑定性 | 防止中途更换数据 |
| 承诺的隐藏性 | 防止承诺本身暴露秘密 |
| 承诺求值证明 | 核查求值声明与已承诺数据一致 |
| 零知识处理 | 防止协议额外泄露受保护信息 |
tlookup 先固定 S 与计数 m,之后验证者发送随机挑战;证明者再计算依赖挑战的辅助量,并证明相关关系。先后顺序是安全逻辑的一部分,不是随意安排的实现细节。
4.4 这一部分解决了什么,还留下什么?
tlookup 将许多非算术检查转为保留张量结构的算术证明任务,是 P4 的关键设计回应。与此同时,实际输入输出仍要被绑定,缩放与取值范围仍要检查;合法表必须可承受,不能任意变大。
因此,下一个问题自然出现:如果一个输出依赖整行输入,单靠“能够证明查表”还不够,必须先找到足够小的表。这正是 Attention 带来的第二个障碍。
5. Idea 2:zkAttn 怎样让 Attention 的证明可承受?
5.1 困难集中在 Softmax 的整行依赖
Attention 可以先理解为:Q 与 K 产生打分,Softmax 将每行打分变成权重,再用权重对 V 加权。两端矩阵乘法已有相应的算术证明手段,中间 Softmax 更难处理。
Softmax 的一个输出不仅依赖自己的分数,还依赖整行分数。直接枚举整行输入组合,会遇到表规模爆炸。因此,有了 tlookup,并不意味着已经找到能承受的 Attention 查表方案。
图 3:聚焦 Softmax 核心,依据 §5 与 §7.1 简化。Attention 两端的矩阵乘法另外使用专门证明。
5.2 作者做了哪些转化?
不追具体数值推导,可以把 zkAttn 的设计理解为三个想法。
首先,用同行移位重新表达归一化。 作者利用 Softmax 的移位性质,将复杂关系集中到一个行偏移和逐元素指数。偏移不是直接展开验证,而是通过指数关系及输出归一化条件间接约束。
其次,把大范围指数拆成多个小范围映射。 利用指数对加法的性质,把输入分段,再查各段的小表并组合输出。它避免为整个输入范围直接建立一张大表,但需要检查分段和重组是否正确。
最后,根据数值贡献分配精度与成本。 某些高位使负指数结果已经接近 0;某些低位对应因子接近 1。作者在规定参数条件下简化这些部分,把精度留给更需要它的分段。
这不是说所有输入都可以任意截断。节省成本的前提,是这些近似带来的误差可以被分析和约束。
5.3 为什么“小表都正确”仍然不够?
作者还需要同时证明:分段能重组原输入,每段映射符合相应表,各段输出能重组最终结果。
否则,证明者完全可能选一组与原输入无关的合法分段,每个小表检查都通过,结果却不是原计算。
归一化也一样。仅证明一个向量非负、和为 1,不能说明它就是指定输入的 Softmax;指数关系、共享行偏移和数据连接必须同时成立。量化后,行和对应输出缩放因子,并带有规定容差,而不是机械要求整数和等于 1。
zkAttn 的贡献,是把 Attention 改写成一组可以承受、又彼此相连的证明任务,而不是简单地给 Attention 增加一个查表步骤。
5.4 这一部分怎样支撑论文目标?
结构改写避免直接联合枚举,小表与分段回应 P5 的内存要求,精度分配和误差界回应 P6。三者都需要分解、查表、重组、归一化关系共同成立,才能保持 P1 的计算可靠性。
到这里仍只获得了处理某类运算的能力。要证明模型输出真实,还必须覆盖其他操作,并保证所有局部证明属于同一次推理。于是主线进入系统拼装。
6. 系统层 idea:怎样从模块正确走向整网正确?
图 4:依据 §6 整理的整体职责图,省略额外承诺与交互轮次。连接约束将各构件绑定成同一次推理。
LLM 不只有 Attention,还包含线性层、激活和归一化。zkLLM 根据操作类型复用不同构件:矩阵乘法采用专门的 sumcheck;激活函数中的非算术部分使用查表或复用 zkAttn 的结构;归一化还需检查降尺度与量化复合运算。
值得注意的是,论文对 GELU 的处理包含 Sigmoid 形式的近似,并非原函数的严格恒等替换。数值近似不是证明过程之外的无关细节,而是需要明确的计算规则。
接着要解决连接问题。假设有两份证明,分别说明某次 Attention 正确、某次前馈网络正确,但前馈网络接收的不是那次 Attention 的输出,它们就不能共同证明一次完整推理。
因此,整网证明需要保证前一步输出就是后一步输入,使用同一个提示和同一份模型参数。作者从输出声明沿计算图反向归约,最终落实到提示 X 与已承诺权重 W。这不是反向传播,不计算梯度,也不训练模型;反向的是证明声明的归约顺序。
整套系统可以概括为:先承诺模型 → 对输入执行推理并生成证明 → 相对于输入、输出与模型承诺验证。
承诺固定的是一份参数。外部如何确认它就是服务商宣称的某个发布模型,还需要相应的身份关联;证明不能凭空建立这种现实联系。
这部分让 P3 从一个承诺性质变成整网的一致性要求:不仅模型不能变,局部计算之间也不能换一套中间值。它把 tlookup、zkAttn 与算术证明收拢到同一个目标,而不是简单堆叠几个独立算法。
7. 回到 Desired properties:哪些保证成立,边界在哪里?
方法章节解释“怎样做”;现在回头检查它究竟提供了什么。P1/P2 需要安全论证,P5/P6 需要成本和误差条件;它们不能互相替代。
7.1 数值近似、完备性与可靠性是三件事
| 问题 | 含义 | 本文中的例子 |
|---|---|---|
| 数值误差 | 规定的离散计算与理想计算有多接近 | 行偏移及各段指数因子的舍入 |
| 完备性错误 | 诚实证明为什么可能被拒绝 | 随机挑战碰巧使分母为零 |
| 可靠性错误 | 错误声明为什么可能被接受 | 错误代数关系碰巧通过随机检查等小概率事件 |
论文 §7.1 在指定参数选择下给出 zkAttn 的误差上界,并用它指导参数配置与归一化容差。它不能直接推广为任意深度模型、任意生成任务的最终行为都不变。
§7.2 则讨论完备性、可靠性和零知识性。诚实证明偶尔遇到坏随机点,与错误计算侥幸通过,是不同方向的失败事件,不能混在一起。
7.2 零知识不等于“什么信息都得不到”
本文结构公开,权重保密。验证者本来就会获得模型输出;零知识目标是证明过程不额外泄露受保护参数,不能消除回答本身携带的信息。
§3.6 使用半诚实验证者设置:验证者遵循协议,但试图从收到的信息中了解更多秘密。定理 7.4 用模拟视图表述零知识保证。理解正式保证时,仍需结合所用子协议与模拟器权限,不能仅凭定理中出现某个量词就声称支持任意恶意交互。
本文中的“计算正确”也有数值规则与范围前提。超出查表范围、采用不同量化配置,不能无条件沿用原来的保证。
7.3 高效结论也有条件
tlookup 的线性开销分析依赖合法表大小不超过待检查数据规模的同阶数量级。表若远大于数据,就不能忽略造表和处理大表的成本。
zkAttn 的分段数也不是越少越好。只分一段会回到巨大单表;分得太多又增加检查、重组和精度分配的负担。真正要平衡的是表大小、检查数量与数值误差。
8. 目标达成到哪里:只记录必要的作者实验结果
本次阅读没有逐项精读实验图表,也没有进行代码复现。这里只记录作者报告的一组结果,帮助理解本文达到的规模,不据此展开性能优劣判断。
论文 §8 的实验使用 OPT 与 LLaMa-2、C4 样本、默认序列长度 2048,硬件包括 A100 40GB、12 个 CPU 核与 124.5GB 主存。Table 1 中,LLaMa-2-13B 的证明者时间为 803 秒、证明大小 188 kB、验证时间 3.95 秒;模型承诺另需 986 秒,承诺大小 11.0 MB。
这些数字说明作者在特定配置下展示了大模型推理证明的可行性。不能把它们直接写成任意聊天、多轮生成、任意硬件的成本,也不能将证明大小与模型承诺大小混为一谈。
9. 理解与收获:从设计边界寻找能继续做的 idea
这一节切换到读者的研究假设。前面的 idea 是作者用来实现目标的设计,下面的 idea 是根据未完全覆盖的要求提出的问题,二者不能混在一起。
对我而言,这篇文章最有启发的地方,是利用计算结构重新组织证明任务:通用查表处理非算术,专门结构处理 Attention,连接约束保证它们属于同一次推理。
但要从理解论文走向研究,还需要把疑问写成可以验证的假设。下面两个方向由论文的方法和分析引出,尚未完成后续文献查新,也没有实验结果,不能当作已经成立的新贡献。
9.1 从 P6 出发:局部误差界怎样连接到审计结论?
证据起点: §7.1 给出 zkAttn 的局部数值误差分析,§6.1.2 的激活处理也涉及近似。这里的缺口是“这些保证是否足以回答某个具体应用问题”,不是已经发现协议安全性错误。
原文对 zkAttn 给出误差分析,激活处理中也存在近似。但局部数值接近,与某个最终行为判断保持一致,不是同一句话。
可以进一步问:某些层或运算是否更容易使误差放大?是否值得在这些位置分配更高精度,而在其他位置节省证明成本?
最小验证思路是固定模型和输入,比较原始执行与离散执行的输出偏差、贪心 token 一致率或具体判定的翻转情况,同时记录证明时间与内存。这只能作为研究计划,不能仅凭存在近似就断言原方案不可靠。
9.2 从 P5 与 P6 的冲突出发:能否按层分配证明资源?
证据起点: §7.1 指出精度与表开销的权衡,§7.3 的线性结论又以表大小受控为条件。研究问题是能否在这些约束下找到更合适的配置,而非简单地把分段数调大或调小。
§7 表明,分段数量、表尺寸和缩放配置共同影响误差与成本。不同层的数据范围、敏感程度未必相同,因此可以考虑在明确范围和误差约束下采用不同配置。
一个起点是对单层做参数扫描,再看局部收益能否保留到整网。需要防止只在某张 GPU 上得到小幅调参收益,却缺少可推广的方法;也要先核对后续工作是否已经解决类似问题。
9.3 把问题写成可检验的计划,而不是一句“可以优化”
| 候选 idea | 改进假设 | 最小验证 | 可能失败的原因 |
|---|---|---|---|
| 让局部精度服务最终行为稳定性 | 识别敏感层或运算,将较高精度优先分配给它们,在同等成本下减少输出或审计判定变化 | 固定模型、输入和生成设置;比较统一精度与分层精度的输出偏差、token 一致率、特定判定变化,再测证明成本 | 局部敏感性不能预测整网行为;提高精度的证明成本抵消收益 |
| 在范围、误差与内存约束下选择分段 | 按层尺寸与输入范围选择分段和缩放,比统一配置得到更好的时间—内存—精度组合 | 先测单层配置,再评估选择策略和参数确定的开销;验证整网收益及范围检查正确性 | 单层最优拼起来未必整网最优;收益仅限特定硬件;后续研究可能已覆盖 |
继续推进前,需要查阅后续文献,说明相对已有量化、参数配置和证明系统优化方法究竟新增了什么。若要使用实际输入分布,还需说明配置如何选定和固定,避免未经分析的自适应过程破坏原有正确性或隐私条件。
这两个问题都指向同一条研究思路:让精度预算与证明资源的分配,更多地由实际计算需求决定。 是否能形成新论文,取决于查新、机制设计、安全论证和可重复实验,而不是问题听起来是否合理。
10. 再把全文接成一条论证
API 输出需要核实,但参数不能公开;零知识证明提供验证路径,LLM 的规模与非算术操作又带来成本障碍。tlookup 先建立通用张量查表能力,zkAttn 再利用 Attention 结构控制表规模,最后将不同操作的证明连接到输入与模型承诺。
本文证明的是规定计算关系,并在相应条件下分析近似与安全边界。它没有把计算真实性、回答真实性和训练合法性合并成一个目标。
| 论证阶段 | 本文最终的回答 |
|---|---|
| 背景与动机 | API 输出缺少可核查的计算来源,模型参数又需保密 |
| 目标 | 保护权重,同时核查输入与已承诺模型上的推理关系,并控制成本 |
| 所需性质 | 可靠性、隐私、绑定;并行、可承受资源与受控数值误差 |
| 作者的 idea | tlookup 提供张量查表;zkAttn 改写 Attention;系统拼装保证整网连接 |
| 结论边界 | 保证依赖对手、编码、范围与参数条件;实际性能仅由对应实验配置支持 |
| 读者的研究问题 | 怎样把局部数值精度和证明资源分配,更直接地连接到整网与应用目标 |
相比记住每一条公式,更值得保留的是三个阅读问题:当前这一步检查什么?它怎样接到前后计算?结论依赖哪些条件? 这三问能将零散工具连成一篇论文的论证,也能帮助辨认哪些地方仍有继续研究的空间。
参考资料
- Sun, H., Li, J., & Zhang, H. zkLLM: Zero Knowledge Proofs for Large Language Models. ACM CCS, 2024, pp. 4405–4419. DOI。
- 作者公开的会议版 PDF:§2 与 Fig.1 为技术总览;§4 为 tlookup;§5–6 为 zkAttn 与整网组装;§7 为误差、安全和开销分析;Table 1 位于 PDF 第 12 页。
- arXiv 记录:完整技术版本与版本信息应以该记录及作者提供材料为准。
写作说明:本文依据会议版原文与本次分批导读整理。ReLU 表、误差多项式与四张流程图为便于理解的教学简化;没有复现系统或逐项评阅实验。研究方向属于待查新、待实验的读者思考。严格定义、参数条件与完整证明应回到原文及完整技术版本核对。