Sound removal of extra checks speeds zero knowledge neural proofs
Sound Debloating of Redundant Checks in Zero-Knowledge Machine-Learning Circuits
Cryptography and Security
Summary
Zero-knowledge proofs let computers prove they did a task correctly without revealing details. When these proofs check neural network computations, many internal checks are repetitive and slow things down. The authors created a tool that safely removes these extra checks without weakening security, so proofs run faster and use fewer resources. They tested their tool on large neural network proofs and cut the work almost in half.
What this means in practice
- •For blockchain developers: Build zero-knowledge proofs for neural network inference that run faster and securely by safely removing redundant checks to reduce prover computational cost.
- •For security engineers: Evaluate and optimize verification circuits in cryptographic protocols to prevent vulnerabilities from unnecessary checks while improving efficiency.
Authors
Zhantong Xue, Pingchuan Ma, Zhaoyu Wang, Yuguang Zhou, Huaijin Wang, Shuai Wang
Abstract
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.