Sound Debloating of Redundant Checks in Zero-Knowledge Machine-Learning Circuits
Automated framework soundly removes up to 48.7% of redundant constraints in ezkl and zkml ZK-ML circuits, cutting prover time by up to 72.8%.
The framework uses whole-circuit abstract interpretation and a provenance graph to verify that each removed redundant check (range proofs, sign lookups, bit decompositions) remains entailed by the rest of the circuit, provably preserving soundness. It was evaluated on MLP, CNN, RNN, and transformer circuits generated by ezkl and zkml, with up to 25.3 million constraints. It removes up to 48.7% of constraints and reduces prover time by up to 72.8% without weakening security. Under-constrained circuits in deployed ZK systems have previously enabled attackers to forge transactions and bypass verification.