Jolt Atlas：基于零知识查找论证的可验证推理技术总结

1. 研究背景与问题 (Problem)

零知识机器学习（zkML）旨在在不泄露模型权重、输入数据甚至模型架构的前提下，验证机器学习推理的正确性。尽管前景广阔，但构建实用的 zkML 系统面临以下核心挑战：

• 计算开销巨大：现代神经网络包含数百万至数十亿参数，且涉及大量高维张量运算。通用 SNARK 证明系统通常比原生执行慢 10 万到 100 万倍。
• 非线性操作的处理困难：神经网络依赖 Softmax、ReLU 等非线性激活函数。在低次算术约束系统中实现这些函数会导致约束数量或次数激增，成为主要成本瓶颈。
• 内存限制：许多 SNARK 构造需要将大量见证（witness）和中间多项式载入内存以生成承诺。对于中等规模的模型，峰值内存需求可能达到数 GB，超出了消费级设备或端侧设备的内存预算。
• 现有方案的局限性：
  • zkVM 方法（如基于 RISC-V 的 Jolt）：通过模拟 CPU 指令执行来验证，但神经网络本质上是张量计算，而非标量指令流，导致效率低下。
  • 电路方法（如 EZKL/Halo2）：将非线性操作硬编码为电路，导致非线性和大范围查找表（Lookup Tables）成本高昂，且难以利用稀疏性。

2. 方法论 (Methodology)

Jolt Atlas 提出了一种新的 zkML 框架，将 Jolt 证明系统的核心思想从"CPU 指令执行”迁移到"ONNX 张量运算”，并引入了多项关键优化：

2.1 核心架构：基于查找论证的张量推理

• 从 CPU 到张量：不同于 zkVM 模拟寄存器操作，Jolt Atlas 直接处理 ONNX 计算图。它消除了通用寄存器和随机 RAM 访问的复杂性，专注于确定性的张量数据流。
• 查找论证（Lookup Arguments）：利用 Jolt 的核心理念，将非线性操作（如 ReLU、Softmax、Tanh）转化为“查找表成员资格”问题，而非复杂的算术约束。这极大地降低了非线性操作的证明成本。
• Sumcheck 协议与 DAG 结构：证明过程被组织为 Sumcheck 实例的有向无环图（DAG）。
  • 外层 Sumcheck：验证 R1CS 约束。
  • 内层 Sumcheck：处理具体的张量运算和查找表验证。
  • 虚拟多项式（Virtual Polynomials）：避免直接承诺巨大的稀疏多项式，而是将其定义为少量低次多项式的代数组合，显著降低内存和计算开销。

2.2 关键优化技术

• 小空间查找论证（Small Space Lookup Arguments）：
  • 前缀 - 后缀分解（Prefix-Suffix Decomposition）：将大型查找表（如 64 位输入）分解为多个小块（Chunk）。通过代数分解，将多线性扩展（Multilinear Extension）分解为前缀和后缀组件。
  • 流式证明（Streaming）：允许证明者在内存受限环境下运行。通过 $C$ 次流式遍历，将峰值内存从 $O(|T|)$ 降低到 $O(|T|^{1/C})$，以时间换空间。
• 神经传送（Neural Teleportation）：
  • 针对 Erf、Tanh 等需要全范围查找表的激活函数，引入“神经传送”技术。
  • 通过全局缩放因子 $\tau$ 压缩输入范围（例如将输入除以 4），使查找表大小从 $2^{32}$ 缩减至 $2^{16}$。
  • 由于这些激活函数在饱和区（Saturation Region）占主导，这种近似在保持模型精度的同时大幅降低了证明成本。
• 零知识保护（BlindFold）：
  • 采用 BlindFold 技术（源自 Vega 论文），将 Sumcheck 验证器编码为 R1CS 电路。
  • 通过 Nova 风格的折叠（Folding）机制，将多个 Sumcheck 实例折叠为一个，并使用 Pedersen 承诺隐藏所有中间消息（多项式系数、评估值），从而实现零知识性，而无需额外的昂贵开销。
• 承诺方案升级：
  • 弃用 Jolt 中用于大见证的 Dory，转而使用 HyperKZG（基于 KZG 的多线性多项式承诺方案）。HyperKZG 更适合张量数据的承诺，且支持基于双线性对的简洁验证，适用于链上验证。

2.3 工作流程

1. 输入：ONNX 模型（支持 Add, Mul, ReLU, Softmax, MatMul 等算子）。
2. 执行与追踪：生成张量执行轨迹（Trace），记录操作类型、源/目的地址及值。
3. 证明生成：
   • 将轨迹映射为 Sumcheck 实例的 DAG。
   • 利用前缀 - 后缀分解处理查找表。
   • 应用神经传送压缩激活函数表。
   • 通过 BlindFold 协议折叠所有阶段，生成最终证明。
4. 验证：验证器运行一个轻量级的 R1CS 电路，验证折叠后的承诺和 Sumcheck 约束。

3. 主要贡献 (Key Contributions)

1. 架构创新：首次将 Jolt 的查找论证范式成功应用于 ONNX 张量计算模型，而非通用的 CPU 指令集。这消除了寄存器模拟的开销，直接利用张量运算的代数结构。
2. 内存效率突破：通过前缀 - 后缀分解和流式证明技术，实现了在内存受限设备（如端侧设备）上对大型模型的证明，解决了 zkML 长期存在的“内存墙”问题。
3. 非线性优化：结合“神经传送”技术，有效解决了非线性激活函数（如 GELU/Tanh）查找表过大导致的证明瓶颈，在精度损失可接受的前提下大幅压缩表大小。
4. 零知识实现：成功集成 BlindFold 技术，在保持高效的同时实现了完整的零知识保护，确保模型权重和输入数据不泄露。
5. 性能基准：在 nanoGPT 和 GPT-2 等模型上展示了显著的性能提升，证明了在消费级硬件上进行可验证推理的可行性。

4. 实验结果 (Results)

• 测试环境：MacBook Pro (Apple M3), 16GB RAM。
• nanoGPT 模型（约 25 万参数，4 层 Transformer）：
  • Jolt Atlas：证明生成时间 14 秒，验证时间 0.517 秒。
  • ezkl (Halo2 基准)：证明生成时间 237 秒（不含 400+ 秒的密钥生成）。
  • 对比：Jolt Atlas 在证明生成速度上实现了约 17 倍 的加速。
• GPT-2 模型（1.25 亿参数）：
  • 端到端总时间：约 38 秒。
  • 详细耗时：Witness 生成 (7.5s) + Commitment (3.5s) + Sumcheck 证明 (16s) + 其他 (11.5s)。
  • 这表明 Jolt Atlas 能够处理百万级参数的模型，且总证明时间在分钟级以内。

5. 意义与未来展望 (Significance & Future Work)

5.1 意义

• 端侧可验证 AI：Jolt Atlas 证明了无需专用硬件（如 GPU/TPU）即可在普通设备上运行 zkML 证明，为隐私保护 AI 和去中心化 AI 应用铺平了道路。
• 信任与隐私：通过密码学验证，可以在不泄露模型知识产权（权重）和用户数据（输入）的情况下，确保 AI 推理的准确性。这对于代理商业（Agentic Commerce）和 AI 记忆（AI Memory）等场景至关重要。
• 通用性：基于 ONNX 标准，支持跨框架（PyTorch, TensorFlow, JAX）部署，降低了 zkML 的采用门槛。

5.2 未来工作

• 后量子安全：计划将 HyperKZG 替换为基于格的承诺方案（如 Hachi），以提供后量子安全性，尽管这会带来更大的证明尺寸。
• 链上验证优化：解决 HyperKZG 在以太坊等链上验证时的 GT 操作开销问题，可能通过基于格的方案缓解。
• 自适应优化：研究自适应的“神经传送”因子 $\tau$ 与前缀 - 后缀分解参数的联合优化，以在证明成本、内存占用和模型精度之间找到最佳平衡点。
• 算子扩展：进一步扩展对更多 ONNX 算子的支持。

总结：Jolt Atlas 通过结合查找论证、流式证明和特定的神经网络优化技术，成功解决了 zkML 在可扩展性、内存效率和隐私保护方面的关键瓶颈，为实现大规模、可验证且隐私保护的 AI 推理系统提供了强有力的技术基础。