把神经网络的一次计算写成约束和生成一份零知识证明是两件不同的工作。前者回答“这些数值是否满足关系”后者还涉及证明系统、公开输入、见证、参数和验证器。两者混在一起最容易让一段几十行的检查程序被误读成可部署的 zk-ML 引擎。arkworks 的接口文档将关系描述和 SNARK 构造分开组织这是理解工程层次的好入口。仓库说明 8 月上线的 better.codes 则提供另一个提醒机器检查接收的是精确定义的命题命题写弱了工具通过也没有证明想要的性质。项目介绍从一个整数神经元开始取两个公开输入x03、x14固定权重2、5先求dot26再用平方激活得到y676。这里选平方只是为了得到一个简单的乘法关系并不把它当成 ReLU 或实际模型的替代品。令见证向量为[1,x0,x1,dot,y]。第一条关系是(2*x05*x1)*1dot第二条是dot*doty还要单独把公开输入与见证中的对应位置绑定。下面的代码使用素数模数 65537。示例中所有预期整数都小于模数真实的有符号定点计算还必须加范围和截断约束不能把模意义相等直接当成整数相等。const P: u128 65537; fn dot(a: [u128; 5], w: [u128; 5]) - u128 { a.iter().zip(w).map(|(x, y)| x * y).sum::u128() % P } fn check(w: [u128; 5], public: [u128; 2]) - bool { if w.iter().any(|x| *x P) || w[0] ! 1 || [w[1], w[2]] ! public { return false; } let rows [ ([0,2,5,0,0], [1,0,0,0,0], [0,0,0,1,0]), ([0,0,0,1,0], [0,0,0,1,0], [0,0,0,0,1]), ]; rows.iter().all(|(a,b,c)| dot(a,w) * dot(b,w) % P dot(c,w)) } fn main() { let good [1,3,4,26,676]; assert!(check(good, [3,4])); let mut bad good; bad[4] 1; assert!(!check(bad, [3,4])); assert!(!check(good, [4,4])); println!(3 constraint cases passed; no proof generated); }保存为neuron.rs运行rustc --edition2021 neuron.rs -o neuron ./neuron。三个断言分别检查合法见证、被篡改的输出和不匹配的公开输入。代码仅在这些受控小整数上使用u128它不是可处理任意有限域元素的密码学库。固定权重不一定需要“每个权重一个乘法门”已知常数乘以变量可以进入线性组合。只有当权重也作为需要约束的私有见证、或者计算结构另有要求时门数分析才会变化。把参数量直接当作非线性乘法门数会误导对稀疏化收益和证明时间的估计。进一步实现 zk-ML还需要把量化规则、模型标识和输入输出承诺绑定进关系再使用经过审查的证明系统完成 setup、prove 和 verify。本文没有运行这些步骤也没有测量证明时间、显存或链上 Gas。先把小关系写对、把篡改用例挡住再讨论如何隐藏见证和压缩证明工程次序会清楚得多。 
长河君 · 2026/10/24 23:57:55 · 阅读 1.2k 用 Rust 检查一层神经元约束：R1CS 示例究竟证明什么
把神经网络的一次计算写成约束和生成一份零知识证明是两件不同的工作。前者回答“这些数值是否满足关系”后者还涉及证明系统、公开输入、见证、参数和验证器。两者混在一起最容易让一段几十行的检查程序被误读成可部署的 zk-ML 引擎。arkworks 的接口文档将关系描述和 SNARK 构造分开组织这是理解工程层次的好入口。仓库说明 8 月上线的 better.codes 则提供另一个提醒机器检查接收的是精确定义的命题命题写弱了工具通过也没有证明想要的性质。项目介绍从一个整数神经元开始取两个公开输入x03、x14固定权重2、5先求dot26再用平方激活得到y676。这里选平方只是为了得到一个简单的乘法关系并不把它当成 ReLU 或实际模型的替代品。令见证向量为[1,x0,x1,dot,y]。第一条关系是(2*x05*x1)*1dot第二条是dot*doty还要单独把公开输入与见证中的对应位置绑定。下面的代码使用素数模数 65537。示例中所有预期整数都小于模数真实的有符号定点计算还必须加范围和截断约束不能把模意义相等直接当成整数相等。const P: u128 65537; fn dot(a: [u128; 5], w: [u128; 5]) - u128 { a.iter().zip(w).map(|(x, y)| x * y).sum::u128() % P } fn check(w: [u128; 5], public: [u128; 2]) - bool { if w.iter().any(|x| *x P) || w[0] ! 1 || [w[1], w[2]] ! public { return false; } let rows [ ([0,2,5,0,0], [1,0,0,0,0], [0,0,0,1,0]), ([0,0,0,1,0], [0,0,0,1,0], [0,0,0,0,1]), ]; rows.iter().all(|(a,b,c)| dot(a,w) * dot(b,w) % P dot(c,w)) } fn main() { let good [1,3,4,26,676]; assert!(check(good, [3,4])); let mut bad good; bad[4] 1; assert!(!check(bad, [3,4])); assert!(!check(good, [4,4])); println!(3 constraint cases passed; no proof generated); }保存为neuron.rs运行rustc --edition2021 neuron.rs -o neuron ./neuron。三个断言分别检查合法见证、被篡改的输出和不匹配的公开输入。代码仅在这些受控小整数上使用u128它不是可处理任意有限域元素的密码学库。固定权重不一定需要“每个权重一个乘法门”已知常数乘以变量可以进入线性组合。只有当权重也作为需要约束的私有见证、或者计算结构另有要求时门数分析才会变化。把参数量直接当作非线性乘法门数会误导对稀疏化收益和证明时间的估计。进一步实现 zk-ML还需要把量化规则、模型标识和输入输出承诺绑定进关系再使用经过审查的证明系统完成 setup、prove 和 verify。本文没有运行这些步骤也没有测量证明时间、显存或链上 Gas。先把小关系写对、把篡改用例挡住再讨论如何隐藏见证和压缩证明工程次序会清楚得多。