本文提出一个名为 Distiller 的通用框架，旨在优化概率证明系统（包括交互式证明 IP、简洁非交互式论证 SNARK、概率可检验证明 PCP 等）的前端开销。在过去十年中，概率证明的实现虽受广泛关注，但由于前端需要将抽象计算转换为等价的算术约束，导致实现规模难以扩展。Distiller 的关键思想是：用户不需要将原始计算直接编码为约束，而是可以翻译一个抽象规格说明（abstracted specification），并在此基础上进行约束生成。该框架首次在此领域实现了可证明安全的转换，即转换过程本身具有形式化保证。此外，Distiller 将“在约束中编码检查”的思想推向逻辑极限，从而发现更多减少约束数量的机会。在基准测试中，Distiller 实现了 1.3 到 50 倍的成本降低，部分场景下获得了更好的渐近复杂度。这篇论文主要面向研究概率证明系统、零知识证明、SNARK 编译器及形式化验证方法的研究人员与高级工程人员，核心贡献在于提供了一种可证明安全的通用约束简化方法，为提升证明系统的可扩展性提供了新思路。