Search for: All records

Optimizing a quantum circuit is hard because it requires exploring a vast space of functionally equivalent circuits, produced by applying local circuit rewrites such as gate cancellation and commutation. Each additional rewrite can exponentially expand the space of equivalent circuits, so existing optimizers can only explore a tiny fraction of this space and often produce suboptimal results. We present Quasar, a new quantum circuit optimizer that can generate astep-limited optimalcircuit: given a bound on rewrite iterations, it returns the lowest-cost circuit reachable within that bound. To achieve this, Quasar constructs two complementary e-graphs for the quantum circuit’s graph and sequence representations. Quasar then infers an atomic rewrite set for application on both e-graphs, which improves optimization performance by orders of magnitude. Finally, Quasar employs a series of new optimization techniques to ensure both soundness and scalability of equality saturation on quantum circuits. Across standard benchmarks, Quasar achieves geometric-mean reductions of 20.2% in 2-qubit gate count, 33.5% in total gate count, and 24.2% in circuit depth, and a 21.4% fidelity improvement over unoptimized circuits, outperforming or matching state-of-the-art rewrite-based optimizers on 75%, 92%, 62%, and 80% of circuits, respectively. 

Abstract: Artifact for PLDI '26 paper "Equality Saturation for Quantum Circuit Optimization". 

Quantum programs are notoriously difficult to code and verify due to unintuitive quantum knowledge associated with quantum programming. Automated tools relieving the tedium and errors associated with low-level quantum details would hence be highly desirable. In this paper, we initiate the study of program synthesis for quantum unitary programs that recursively define a family of unitary circuits for different input sizes, which are widely used in existing quantum programming languages. Specifically, we present QSynth, the first quantum program synthesis framework, including a new inductive quantum programming language, its specification, a sound logic for reasoning, and an encoding of the reasoning procedure into SMT instances. By leveraging existing SMT solvers, QSynth successfully synthesizes ten quantum unitary programs including quantum adder circuits, quantum eigenvalue inversion circuits and Quantum Fourier Transformation, which can be readily transpiled to executable programs on major quantum platforms, e.g., Q#, IBM Qiskit, and AWS Braket. 

Distributed protocols have long been formulated in terms of their safety and liveness properties. Much recent work has focused on automatically verifying the safety properties of distributed protocols, but doing so for liveness properties has remained a challenging, unsolved problem. We present LVR, the first framework that can mostly automatically verify liveness properties for distributed protocols. Our key insight is that most liveness properties for distributed protocols can be reduced to a set of safety properties with the help of ranking functions. Such ranking functions for practical distributed protocols have certain properties that make them straightforward to synthesize, contrary to conventional wisdom. We prove that verifying a liveness property can then be reduced to a simpler problem of verifying a set of safety properties, namely that the ranking function is strictly decreasing and nonnegative for any protocol state transition, and there is no deadlock. LVR automatically synthesizes ranking functions by formulating a parameterized function of integer protocol variables, statically analyzing the lower and upper bounds of the variables as well as how much they can change on each state transition, then feeding the constraints to an SMT solver to determine the coefficients of the ranking function. It then uses an off-the-shelf verification tool to find inductive invariants to verify safety properties for both ranking functions and deadlock freedom. We show that LVR can mostly automatically verify the liveness properties of several distributed protocols, including various versions of Paxos, with limited user guidance. 

Quantum computing technology may soon deliver revolutionary improvements in algorithmic performance, but it is useful only if computed answers are correct. While hardware-level decoherence errors have garnered significant attention, a less recognized obstacle to correctness is that of human programming errors—“bugs.” Techniques familiar to most programmers from the classical domain for avoiding, discovering, and diagnosing bugs do not easily transfer, at scale, to the quantum domain because of its unique characteristics. To address this problem, we have been working to adapt formal methods to quantum programming. With such methods, a programmer writes a mathematical specification alongside the program and semiautomatically proves the program correct with respect to it. The proof’s validity is automatically confirmed—certified—by a “proof assistant.” Formal methods have successfully yielded high-assurance classical software artifacts, and the underlying technology has produced certified proofs of major mathematical theorems. As a demonstration of the feasibility of applying formal methods to quantum programming, we present a formally certified end-to-end implementation of Shor’s prime factorization algorithm, developed as part of a framework for applying the certified approach to general applications. By leveraging our framework, one can significantly reduce the effects of human errors and obtain a high-assurance implementation of large-scale quantum applications in a principled way.