Existing quantum compilers optimize quantum circuits by applying circuit transformations designed by experts. This approach requires significant manual effort to design and implement circuit transformations for different quantum devices, which use different gate sets, and can miss optimizations that are hard to find manually. We propose Quartz, a quantum circuit superoptimizer that automatically generates and verifies circuit transformations for arbitrary quantum gate sets. For a given gate set, Quartz generates candidate circuit transformations by systematically exploring small circuits and verifies the discovered transformations using an automated theorem prover. To optimize a quantum circuit, Quartz uses a cost-based backtracking search that applies the verified transformations to the circuit. Our evaluation on three popular gate sets shows that Quartz can effectively generate and verify transformations for different gate sets. The generated transformations cover manually designed transformations used by existing optimizers and also include new transformations. Quartz is therefore able to optimize a broad range of circuits for diverse gate sets, outperforming or matching the performance of hand-tuned circuit optimizers.
Existing quantum compilers optimize quantum circuits by applying circuit transformations designed by experts. This approach requires significant manual effort to design and implement circuit transformations for different quantum devices, which use different gate sets, and can miss optimizations that are hard to find manually. We propose Quartz, a quantum circuit superoptimizer that automatically generates and verifies circuit transformations for arbitrary quantum gate sets. For a given gate set, Quartz generates candidate circuit transformations by systematically exploring small circuits and verifies the discovered transformations using an automated theorem prover. To optimize a quantum circuit, Quartz uses a cost-based backtracking search that applies the verified transformations to the circuit. Our evaluation on three popular gate sets shows that Quartz can effectively generate and verify transformations for different gate sets. The generated transformations cover manually designed transformations used by existing optimizers and also include new transformations. Quartz is therefore able to optimize a broad range of circuits for diverse gate sets, outperforming or matching the performance of hand-tuned circuit optimizers.
Existing quantum compilers optimize quantum circuits by applying circuit transformations designed by experts. This approach requires significant manual effort to design and implement circuit transformations for different quantum devices, which use different gate sets, and can miss optimizations that are hard to find manually. We propose Quartz, a quantum circuit superoptimizer that automatically generates and verifies circuit transformations for arbitrary quantum gate sets. For a given gate set, Quartz generates candidate circuit transformations by systematically exploring small circuits and verifies the discovered transformations using an automated theorem prover. To optimize a quantum circuit, Quartz uses a cost-based backtracking search that applies the verified transformations to the circuit. Our evaluation on three popular gate sets shows that Quartz can effectively generate and verify transformations for different gate sets. The generated transformations cover manually designed transformations used by existing optimizers and also include new transformations. Quartz is therefore able to optimize a broad range of circuits for diverse gate sets, outperforming or matching the performance of hand-tuned circuit optimizers.
Quantum circuit optimization - the process of transforming a quantum circuit into an equivalent one with reduced time and space requirements - is crucial for maximizing the utility of current and near-future quantum devices. While most automated optimization techniques focus on transforming circuits into equivalent ones that implement the same unitary, we show that substantial new opportunities for resource reduction can be achieved by (1) allowing approximate local transformations and (2) employing mixed quantum channels to approximate pure circuits. Our novel automated protocol for approximate circuit rewriting is a refined evolution of automated optimization techniques based on the ZX-calculus, where we add a greedy strategy that selectively replaces ZX-diagrams with small phase angles with stochastic mixtures of the identity and carefully chosen over-rotations, which are designed to reduce the overall gate count in expectation while staying within a strict error budget. This approach yields modest two-qubit gate count reduction in random quantum circuits, and achieves a substantial reduction in structured circuits such as the quantum Fourier transform. Fundamentally, our protocol converts experimental noise due to gate applications into deliberately engineered random noise, outperforming many other approximation methods on average. These results highlight the potential of mixed-channel approximations to enhance future quantum circuit performance, suggesting new directions for resource-aware automated quantum compilation beyond pure unitary channels.
Abstract Existing quantum compilers focus on mapping a logical quantum circuit to a quantum device and its native quantum gates. Only simple circuit identities are used to optimize the quantum circuit during the compilation process. This approach misses more complex circuit identities, which could be used to optimize the quantum circuit further. We propose Quanto, the first quantum optimizer that automatically generates circuit identities. Quanto takes as input a gate set and generates provably correct circuit identities for the gate set. Quanto’s automatic generation of circuit identities includes single-qubit and two-qubit gates, which leads to a new database of circuit identities, some of which are novel to the best of our knowledge. In addition to the generation of new circuit identities, Quanto’s optimizer applies such circuit identities to quantum circuits and finds optimized quantum circuits that have not been discovered by other quantum compilers, including IBM Qiskit and Cambridge Quantum Computing Tket. Quanto’s database of circuit identities could be applied to improve existing quantum compilers and Quanto can be used to generate identity databases for new gate sets.
Optimizing and simulating quantum circuits at scale are critical bottlenecks in realizing the full potential of quantum computing. This thesis delivers a comprehensive suite of systems to overcome these limitations, spanning both physical compilation and classical simulation. For quantum circuit optimization, we first automate the discovery and verification of transformation rules by introducing Equivalence Circuit Class (ECC) sets and an efficient generation algorithm for arbitrary gate sets. We deploy these rules within the superoptimizer Quartz, which utilizes a cost-based backtracking search to escape local minima that trap traditional rule-based methods. To eliminate the exponential runtime penalties inherent to pure search, we introduce QALM, a hybrid optimization framework. By unifying search-based exploration with greedy rule-based exploitation in an interleaved control loop, QALM dynamically escapes local minima without exhaustive backtracking. Evaluated across a large benchmark suite of 248 diverse circuits, QALM outperforms existing search-based optimizers in final circuit quality while operating with the computational efficiency of rule-based systems. While the prior two approaches aim for global optimization, this problem is intrinsically QMA-hard, creating a bottleneck for large programs. To circumvent this issue and scale up, we introduce OAC, a cut-and-meld circuit optimization algorithm. OAC cuts a circuit into subcircuits, applies an existing oracle optimizer independently, and seamlessly melds the results. This algorithm operates with a linear number of oracle calls while attaining local optimality. Empirical evaluation shows that OAC significantly improves the efficiency of state-of-the-art optimizers while enhancing overall quality. Beyond physical execution, the scalable simulation of quantum circuits on classical hardware presents another major challenge. To address this, we present Atlas, a distributed GPU-based simulator that hierarchically partitions circuits to exploit data parallelism while minimizing communication overhead. By leveraging integer linear programming to allocate structurally related gates to nearby GPUs and dynamic programming for kernel scheduling, Atlas runs significantly faster than prior state-of-the-art GPU simulators. Together, these frameworks provide a robust toolchain, improving both the execution of quantum circuits on physical devices and their scalable classical simulation.
Compiling quantum algorithms for real devices involves hard optimization problems that can decide whether an algorithm runs at scale. We present a general method for solving such problems with AI agents, with every result certified. It builds on autoresearch loops, in which agents iteratively improve programs against a fixed evaluator and which have recently improved quantum cryptanalysis circuits, and adds two elements: a frozen, exact verifier certifies every result, and this verifier, together with the challenge around it, is built by an agent that formulates the problem with a researcher and validates the verifier against a solved case, deliberately broken solutions and published results before any solution exists. The method applies to any optimization problem whose solutions can be verified exactly and efficiently. We apply it to three compilation problems in quantum simulation, namely fermion-to-qubit encoding, Hamiltonian layout and unitary synthesis. In each, the agents improved substantially on published or standard constructions, reducing the cost being optimized by up to 73% at the largest sizes tested and outperforming a state-of-the-art optimizer for fermion-to-qubit encodings. Every submission is a program accompanied by its agent's notes, so the ideas behind each improvement are recorded in human-readable form; later agents built on them, and we describe them here. These results open the way to automated, certified discovery across quantum circuit design and beyond.
Quantum circuit compilation is a crucial step in the process of executing quantum algorithms on near-term quantum hardware. The challenge lies in translating high-level quantum algorithms, often expressed using universal gate sets, into efficient, gate-level circuits that minimize gate count and circuit depth, thereby reducing error rates and improving execution times. Traditional compilation methods often rely on hand-crafted heuristics or limited search algorithms, failing to fully explore the exponentially large search space of possible circuit transformations. This work proposes an adaptive quantum circuit compilation framework leveraging Bayesian optimization. The system dynamically explores the space of potential circuit transformations, learning to identify optimal compilation strategies through a probabilistic modeling approach. The core claim is that Bayesian optimization can effectively adaptively compile quantum circuits, optimizing for performance and minimizing gate count. The system incorporates a compiler that utilizes Bayesian optimization to explore the vast space of possible quantum circuit transformations, learning to identify the most efficient compilation strategies. The results demonstrate the potential of this approach to significantly reduce the complexity of quantum circuits while maintaining algorithm fidelity.