一句话：提出合成辅助编译器 Tabby，从高层程序自动生成高性能 ZK 电路，提升证明效率并保证语义等价。
零知识证明应用需将高层程序转换为算术电路，既要正确又需高效，但现有 DSL 生成的电路常非最优，手工优化难以构造和验证。Tabby 提出一种合成辅助编译器，引入面向符号推理的领域特定中间表示，利用 sketch 程序合成生成优化后的低层实现，并通过组件分解和基于 SMT 的语义等价验证保证正确性。作者在真实 ZKP 应用上评估，结果显示相比主流 ZK 编译器，证明生成时间和电路规模均显著降低。
Zero-knowledge proof (ZKP) applications require translating high-level programs into arithmetic circuits–a process that demands both correctness and efficiency. While recent DSLs improve usability, they often yield suboptimal circuits, and hand-optimized implementations remain difficult to construct and verify. We present Tabby, a synthesis-aided compiler that automates the generation of high-performance ZK circuits from highlevel code. Tabby introduces a domain-specific intermediate representation designed for symbolic reasoning and applies sketch-based program synthesis to derive optimized low-level implementations. By decomposing programs into reusable components and verifying semantic equivalence via SMT-based reasoning, Tabby ensures correctness while achieving substantial performance improvements. We evaluate Tabby on a suite of real-world ZKP applications and demonstrate significant reductions in proof generation time and circuit size against mainstream ZK compilers.
@article{paperbot2896,
title = {Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits},
author = {Junrui Liu and Jiaxin Song and Yanning Chen and Hanzhi Liu and Hongbo Wen and Luke Pearson and Yanju Chen and Yu Feng},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763110}
}