发表机构
Zhejiang University of Technology; The Hong Kong University of Science and Technology; Nanyang Technological University（浙江工业大学; 香港科技大学; 南洋理工大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
Quelle反编译器从量子汇编中恢复结构化程序，通过精确重写与假设检查保证等价性，在816个程序上实现100%等价与94%完全反编译，性能优于LLM方法1.7倍。
AI 中文摘要
量子编译器将程序翻译为原生门，插入SWAP门以将交互路由到设备上，并优化结果。输出是量子汇编，一个隐藏算法结构（QFT、Grover迭代、QAOA层）的扁平门列表。理解、审计、移植或重用此类汇编需要恢复暴露此结构的程序。我们提出Quelle，一个反编译器，从路由和优化的量子汇编（OpenQASM）中恢复结构化程序（库调用、循环、函数、符号角度），并检查每个输出与其输入的等价性。Quelle建立在一个不变式上：每一步要么是精确重写，在应用处检查，要么是假设，在使用前对照输入检查。它首先通过移除编译伪影（特别是取消路由）将汇编提升为电路，恢复路由插入的SWAP，包括合并到其他门中的那些。然后恢复算法模板（草图），其参数从编译保留的量中求解，对于没有模板的算法，通过反合一恢复库调用和循环。失败的假设被拒绝；相应的操作保持门级形式。在来自22个算法家族和随机电路控制的816个汇编程序上，以四种路由和优化级别编译，使用原生双量子比特门CX、ECR或CZ，Quelle的输出对100%的输入与输入等价，并完全反编译其中94%；在相同输入上比较，它完全反编译的数量是最佳基于LLM的反编译器的1.7倍，后者每个输入花费15K个令牌。对于没有模板的九个算法家族，它无模板恢复的结构解释了60%的门。它检查多达230万个门的输入，并在237个真实世界的QASMBench汇编文件上不产生不等价输出。
英文摘要
Quantum compilers translate programs into native gates, insert SWAP gates to route interactions onto a device, and optimize the result. The output is quantum assembly, a flat gate list that hides the algorithm's structure (QFT, Grover iteration, QAOA layers). Understanding, auditing, porting, or reusing such assembly requires recovering a program that exposes this structure. We present Quelle, a decompiler that recovers structured programs (library calls, loops, functions, symbolic angles) from routed and optimized quantum assembly (OpenQASM) and checks every output for equivalence with its input. Quelle is built on one invariant: every step is either an exact rewrite, checked where it is applied, or a hypothesis, checked against the input before use. It first lifts the assembly into a circuit by removing compilation artifacts, notably un-routing, which recovers the SWAPs that routing inserted, including those merged into other gates. It then recovers algorithm templates (sketches) whose parameters are solved from quantities preserved by compilation, and, for algorithms without a template, library calls and loops by anti-unification. Failed hypotheses are rejected; the corresponding operations remain in gate-level form. On 816 assembly programs from 22 algorithm families and a random-circuit control, compiled at four routing and optimization levels with native two-qubit gates CX, ECR, or CZ, Quelle's output is equivalent to the input for 100% of the inputs, and it fully decompiles 94% of them; compared on the same inputs, it fully decompiles 1.7x as many as the best LLM-based decompiler, which spends 15K tokens per input. On nine algorithm families for which it has no template, the structure it recovers without templates explains 60% of the gates. It checks inputs of up to 2.3 million gates and emits no inequivalent output on 237 real-world QASMBench assembly files.
