零知识机器学习电路中冗余检查的可靠精简

中文摘要 AI 辅助

零知识（ZK）证明系统用于神经网络推理时，会将模型编译为算术约束系统。其中许多约束是冗余检查：范围证明、符号查找和位分解，这些检查通过跨越不同组件的推理链，被电路其余部分全局蕴含。移除这些检查可缩小电路并加速证明，但移除必须谨慎论证：不健全的精简电路会变得可伪造，接受原始电路会拒绝的见证，从而允许证明者声称，例如，神经网络产生了其从未实际计算的输出。此类健全性漏洞并非假设性：已部署ZK系统中约束不足的电路已使攻击者能够伪造交易并完全绕过验证。我们提出一个自动化框架，在可证明保持健全性的同时移除冗余检查。对于每个候选移除项，我们的工具首先检查电路其余部分是否能独立排除被移除检查所排除的每个值。通过全电路抽象解释，分析搜索此类替代论证并将其记录在溯源图中；仅当图中存在替代路径仍能推导出该检查所验证的事实时，才移除该检查。这确保精简后的电路不会为对手开辟新的伪造策略。我们评估了由两个生产框架（ezkl和zkml）生成的涵盖MLP、CNN、RNN和Transformer架构的电路，规模高达2530万个约束。我们的工具最多移除48.7%的约束，并将证明者时间最多减少72.8%，且不削弱安全性。

英文摘要

Zero-knowledge (ZK) proof systems for neural-network inference compile the model into a system of arithmetic constraints. Many of these constraints are redundant checks: range proofs, sign lookups, and bit decompositions who are globally entailed by the rest of the circuit through chains of reasoning that span distant gadgets. Removing them shrinks the circuit and accelerates proving, but the removal must be carefully justified: an unsoundly debloated circuit becomes forgeable, accepting witnesses the original would have rejected and so allowing a prover to claim, for example, that a neural network produced an output it never actually computed. Such soundness vulnerabilities are not hypothetical: under-constrained circuits in deployed ZK systems have enabled attackers to forge transactions and bypass verification entirely. We present an automated framework that removes redundant checks while provably preserving soundness. For each candidate removal, our tool first checks whether the rest of the circuit, on its own, can still rule out every value the removed check was excluding. Using whole-circuit abstract interpretation, the analysis searches for such alternative justifications and records them in a provenance graph; a check is then removed only when an alternative path through the graph still derives the facts that it is checking. This ensures that the debloated circuit opens no new forging strategy to an adversary. We evaluate circuits spanning MLP, CNN, RNN, and transformer architectures generated by two production frameworks (ezkl and zkml), with up to 25.3 million constraints. Our tool removes up to 48.7\% of constraints and reduces prover time by up to 72.8\%, without weakening security.

发表机构

• Hong Kong University of Science and Technology（香港科技大学）
• Zhejiang University of Technology（浙江工业大学）
• Shandong University（山东大学）

机构由 AI 辅助整理，请以论文原文为准。