面向数值计算的简洁证明系统（OSDI 2026）
原题：Spain: Succinct proofs for numerical computations
一句话总结：数值计算本来允许舍入误差，但传统 succinct proof 要求有限域约束精确成立；Spain 把约束改为允许有界误差的有理数约束，再用平方误差和 sum-check 证明其整体准确性，在保持通用性的同时将约束数减少 32 倍至 17,000 倍，证明开销降到相对原生执行约 3–5 个数量级。
问题与动机
简洁证明（succinct proof）让验证者确认不可信执行方确实运行了约定计算，却不必重新执行计算。现有系统通常先把程序编译成有限域上的 R1CS。这个过程适合整数和离散逻辑，却不适合固定点或浮点计算：除法、比较、范围检查和浮点语义都需要显式编码位级逻辑，单个数值操作的约束量会随位宽增长。
Spain 针对的不是程序是否满足规格，而是输出是否来自一次允许数值误差的执行。论文设定了三个目标：通用前端、验证成本低于原生执行，以及证明者相对原生执行的开销不超过约 1000 倍。目标并非零知识或非交互式证明。
关键观察 / 隐含假设
- 观察 1：数值程序的正确性本身包含误差预算。 浮点操作遵循相对误差界，固定点操作遵循绝对误差界；要求约束精确等于零会把正常舍入也判为错误（§2.1、§3）。
- 依赖假设：用户能够为每个操作及其组合推导可接受误差，并将其转成约束误差界。
- 可能失效场景：存在强烈误差抵消、条件分支不稳定或中间值接近奇点时，逐操作误差界未必足以推出最终输出质量。
- 观察 2：R1CS 后端的主要成本由约束数和 witness 大小驱动。 传统比较和除法会引入与位宽相关的辅助变量；Spain 认为压缩前端比单纯优化后端更能改变成本（§2.2、§7.1）。
- 依赖假设：数值操作可以用低数量的有理数关系表达，同时不会因范围、分母或溢出问题失去语义。
- 证据强度：强。多组基准中约束数减少 32 倍至 17,000 倍，但后端仍有较高的单位约束成本（§7.1）。
- 假设 1：误差的平方和可以替代最大误差。 Spain 用 (\ell_2) 误差平方和上界 (\ell_\infty) 误差；因此完整性要求证明者使用比验证者保证的误差更高的精度，精度差距约为约束数平方根（§4.1）。
- 证据强度：强，论文给出了范数不等式和协议证明；但这会造成完整性与健全性之间的参数余量。
核心方法
Spain 的前端把约束写在有理数域上，并把精确等式改为近似约束，例如 x·y ≈ε z 表示绝对误差不超过 ε。每个数值操作通常只需一个或少量约束：除法和平方根各用一个关系，比较用平方根和辅助变量表达，max、min、ReLU 以及分段函数也因此不再支付位宽级别的范围检查成本（§5）。
后端不直接证明每个误差的最大值，而是证明误差向量的平方和 (|e|_2^2) 小于阈值。协议结合 Spartan 的 sum-check、DARK 多项式承诺和 Zaratan 的运行时有限域选择。证明者先承诺有理数 witness，再由验证者随机选择大素数，把有理数映射到有限域；分母约定为 2 的幂，并配合分母和分子范围限制，降低不同有理数映射到同一有限域元素的碰撞概率（§4.2.1）。
为了适应 sum-check，Spain 将 R1CS 的每条约束误差平方求和，并把它改写成关于矩阵多线性扩展的多项式声明。验证者只需检查该声明与 witness 承诺的一致性。系统还支持 SIMD-R1CS，用于相同结构的批量输入，以及 I-R1CS，用于证明期间由验证者逐步提供输入或约束（§4.3）。
数值函数使用有理逼近而非只使用多项式逼近。以指数函数为例，Padé 逼近在同样项数下覆盖更宽的输入区间；论文示例中误差 0.01 时，四阶 Taylor 逼近覆盖约 [-1.07, 1.00]，同规模 Padé 逼近覆盖约 [-8.11, 2.84]（§5）。ONNX 前端会改写超越函数、增加辅助输出，并用双精度或四倍精度执行 witness generation。
GPT-2 的矩阵乘法使用近似版 Freivalds 检查，避免把完整乘法结果逐项编码。后端以 Rust 实现约 12,135 行代码；另有 gadget、ONNX 和线性规划前端（§6）。
设计取舍
- 近似约束换取紧凑 arithmetization：除去了位分解和显式浮点逻辑，但用户必须做数值分析，证明者的 witness 需要更高精度；Spain 不提供 IEEE 754 的完整相对误差语义（§5、§8）。
- 平方和换取可证明性：(\ell_2) 平方和适合 sum-check，却比最大误差更严格，造成完整性参数 (ε_{wg}<ε) 的差距；约束很多时，证明者必须把单条约束误差压得更低（§4.1）。
- DARK 换取通用有理数承诺：DARK 支撑运行时选择有限域，但通常是证明者最主要的成本；若改用更新的有理数多项式承诺，可能显著降低端到端时间（§7.2、§8）。
- 通用前端绑定后端：Spain 的近似约束目前依赖其专用后端，无法直接获得 Otti 或 ZKLP 的零知识、非交互和超快验证属性（§7.4）。
实验与结果
- 在 Netlib 线性规划、Softmax、LayerNorm、GELU、GPT-2、二维流体模拟和 Uber H3 地理计算上，Spain 的约束数相对基线减少 32 倍至 17,000 倍（图 4、§7.1）。
- 相对 Otti、ZKLP 及其前端/后端拆分基线，证明者加速约 8–2700 倍；相对原生执行，Spain 的证明开销在不同实验中约为 3–5 个数量级，部分实例达到论文设定的约 1000 倍目标（图 4、§7.1、§7.4）。
- zkGPT 在 GPT-2 上仍比 Spain 更快，但它是针对固定模型结构的专用系统，不能作为通用基线；Spain 在
passes=16的 GPT-2 配置中验证时间略优于 zkGPT（图 4、§7.1）。 - 验证者并非所有单实例都能比原生执行便宜。最大线性规划实例
scsd8达到 break-even；GPT-2 等工作负载需要 SIMD 批处理摊销固定成本（§7.3）。 - GPT-2 最大实验中，证明者内存约为
seq=32, passes=1时 41 GB，passes=16时 267 GB；大多数基准的证明时间由 DARK 主导（§7.2）。
论断—证据表
| 论断 | 证据 | 评测边界 | 置信度 |
|---|---|---|---|
| 近似约束能大幅压缩数值计算的 arithmetization | 约束数减少 32 倍至 17,000 倍（图 4、§7.1） | CPU、单线程；线性规划、ML、流体、地理计算 | 强 |
| 前端压缩能抵消 Spain 后端较高的单位约束成本 | 相对基线证明者加速 8–2700 倍（§7.1） | 对照包含 Otti、ZKLP 及合成前端，部分基线有语义限制 | 强 |
| 验证成本在部分批量场景低于原生执行 | scsd8 单实例 break-even；GPT-2 批处理固定成本可摊销（§7.3） | 验证者与证明者使用不同 CPU；不适用于所有单实例 | 中 |
| Spain 具有通用性 | 覆盖线性规划、ONNX 原语、GPT-2、流体和 geolocation，未因表达能力丢弃基准（§7.4） | 仍依赖近似约束可表达的数值语义；不含零知识和非交互 | 中 |
批判性分析
论证链条
论证链是闭合的：数值执行允许误差，近似约束把误差放入前端，后端证明误差平方和，再由范数关系推出每条约束的最大误差。实验也直接验证了约束规模和证明时间的变化。论文没有把约束误差自动等同于最终输出误差，而是明确把累计误差留给数值分析，这一边界是合理的。
但平方和证明带来的参数差距会随约束数扩大。证明者需运行更高精度 witness generation，且最终输出的数值稳定性仍依赖用户对程序的分析。实验中的相对原生开销仍是 3–5 个数量级，说明“达到 1000 倍以内”只在部分配置成立。
假设压力测试
方案假设中间值、分子和分母都能被预先限制。包含极端动态范围、接近零的除数、分段边界或 NaN/Inf 语义的程序可能需要额外约束。平方根编码允许输入为小负数时仍存在近似满足解；论文建议用额外约束或数值分析排除该情形，但没有给出通用自动化机制（§5）。
验证收益依赖重复相同结构的批处理。一次性、小输入但输出很大的任务可能无法摊销固定成本。证明者内存随 GPT-2 passes 从 41 GB 增至 267 GB，也限制了更大模型和更长序列的直接外推（§7.2–§7.3）。
实验可信度
实验覆盖面比单一应用系统广，且使用至少 5 次运行，标准差不超过均值的 11%。Otti-FE 和 ZKLP-FE 能隔离前端贡献，但 ZKLP-FE 的结构是按操作计数构造的合成 R1CS，不能代表完整语义实现；其 GPT-2 结果还依赖线性外推。因此，约束规模结论较可信，端到端对 ZKLP 的绝对比较应谨慎。
系统性缺陷
DARK 是主要证明成本，后端还需要 256、512 和 786 位整数运算以及运行时有限域转换。系统当前没有零知识和非交互模式，交互轮次、部署协议和网络成本未在主要实验中量化。论文也未系统评估故障恢复、资源隔离、可观测性和生产级 GPU witness generation。近似语义可能使不同实现对边界情况的处理不一致，运维侧需要保存误差参数和数值分析假设。
局限与后续工作
- 局限 1：Spain 保证的是每条约束的绝对误差界，不直接提供 IEEE 754 式相对误差界；动态范围大的模型可能需要重新设计缩放与分析。
- 局限 2：验证者只有在足够大的批量或计算规模下才可能低于原生执行，固定成本和 DARK 开销仍是瓶颈。
- 局限 3：近似约束与当前后端耦合，无法直接复用带零知识或非交互属性的后端。
- 后续工作 1：用更快的有理数多项式承诺替换 DARK，并在相同基准上报告证明时间、内存和验证 break-even 点。
- 后续工作 2：扩展相对误差约束，加入 NaN、Inf、除零和符号平方根的明确语义，再用包含边界输入的数值测试验证健全性。
- 后续工作 3：将近似约束接入 zkVM 或其他 sum-check 后端，测量零知识、非交互化和 GPU witness generation 对总成本的影响。