本文研究的是零知识机器学习（ZKML）电路中的「冗余检查」问题及其可证明安全的去膨胀（debloating）技术。背景是：面向神经网络推理的零知识证明系统会把模型编译成大规模算术约束系统，其中包含大量范围证明、符号查找（sign lookup）、比特分解等约束。作者指出，这些约束中有相当一部分是「冗余检查」——它们所断言的事实在整条电路上已经被其他远处的组件通过一连串推理关系所蕴含，因此单看局部是必要的，但从全局看其约束力是多余的。删除这类冗余约束能显著缩小电路规模、加快证明生成，但删除必须以严格的可靠性（soundness）论证为前提：一旦删得不合理，电路就会变成欠约束（under-constrained），证明者可以构造出原电路本应拒绝的见证，例如谎称某个神经网络产生了它实际上并未计算过的输出。作者强调这不是假设性威胁——已部署的 ZK 系统中出现过的欠约束电路缺陷，曾使攻击者能够伪造交易并完全绕过验证。 核心方法上，作者提出一个自动化框架：对每一个候选删除的约束，工具首先判断「电路其余部分」自身是否仍然能够排除被删约束原本排除的所有取值。为此，工具使用全电路抽象解释（whole-circuit abstract interpretation）来搜索这些替代性论证，并把它们记录在一张溯源图（provenance graph）中；只有当图中存在一条替代路径仍然能够推导出该约束所检查的事实时，才真正删除该约束。这一「先证明替代论证存在、再删除」的流程，从机制上保证去膨胀后的电路不会为敌手开启新的伪造路径，即在不削弱安全性的前提下完成优化。 实验方面，作者在 ezkl 与 zkml 两个生产级框架生成的 MLP、CNN、RNN 与 Transformer 电路上进行评估，电路规模最高达 2530 万条约束。结果显示，工具可移除最高 48.7% 的约束，并把证明者（prover）耗时最多降低 72.8%，同时不削弱安全性。该工作适合零知识证明工程、ZKML 系统开发者、形式化验证与程序分析研究者，以及关注 ZK 电路可靠性漏洞的安全工程师阅读。