Determining whether a target unitary can be implemented within a prescribed quantum circuit architecture is a fundamental problem in quantum information, with direct implications for optimisation and compilation of quantum circuits, and hardware-efficient quantum computation. While existing synthesis and compilation methods are primarily constructive, they generally do not provide rigorous certificates that a unitary cannot be realised using given implementation resources. Here we introduce a general framework to define quantum circuit architecture witnesses, which certify the incompatibility of a unitary transformation with a specified quantum circuit architecture. We formulate the witness construction as a semidefinite program by maximising the fidelity between the Choi state of the target unitary and those of tested circuits. The resulting witnesses provide practical and quantitative certificates of incompatibility, implying lower bounds on implementation resources such as the gate count or circuit depth, and can also be used experimentally to benchmark quantum devices by certifying that an implemented unitary channel goes beyond the capabilities of a given circuit architecture. For Clifford unitaries, we exploit the stabiliser formalism to reduce the construction to linear programming, enabling both more efficient numerical certification for circuits containing on the order of seven two-qubit gates, and analytical witnesses for some families of architectures made of an arbitrary number of gates.
Determining whether a target unitary can be implemented within a prescribed quantum circuit architecture is a fundamental problem in quantum information, with direct implications for optimisation and compilation of quantum circuits, and hardware-efficient quantum computation. While existing synthesis and compilation methods are primarily constructive, they generally do not provide rigorous certificates that a unitary cannot be realised using given implementation resources. Here we introduce a general framework to define quantum circuit architecture witnesses, which certify the incompatibility of a unitary transformation with a specified quantum circuit architecture. We formulate the witness construction as a semidefinite program by maximising the fidelity between the Choi state of the target unitary and those of tested circuits. The resulting witnesses provide practical and quantitative certificates of incompatibility, implying lower bounds on implementation resources such as the gate count or circuit depth, and can also be used experimentally to benchmark quantum devices by certifying that an implemented unitary channel goes beyond the capabilities of a given circuit architecture. For Clifford unitaries, we exploit the stabiliser formalism to reduce the construction to linear programming, enabling both more efficient numerical certification for circuits containing on the order of seven two-qubit gates, and analytical witnesses for some families of architectures made of an arbitrary number of gates.
Certifying high-dimensional quantum channels is essential for ensuring the reliability of quantum communication protocols. Existing certification schemes often rely on fully trusted internal devices, which is difficult to achieve in realistic scenarios. Here, we propose a semi-device-independent framework for certifying channel properties directly from observed statistics, assuming only that the system dimension is known. By explicitly incorporating the full set of structural constraints inherent to Choi states, our approach exploits the Choi-Jamiołkowski isomorphism for rigorous certification of quantum channels. The entanglement dimensionality of quantum channels is first certified by introducing a witness and numerically determining its Schmidt-number-dependent bounds. This certification method reproduces known analytical benchmarks and is applied to dephasing and depolarizing noise channels, thereby confirming its validity. To provide a more complete assessment of channel performance, the entanglement fidelity of quantum channels is also certified using a hierarchy of semidefinite programming relaxations based on localizing matrices. Lower bounds on the entanglement fidelity are obtained that are compatible with either the full set of observed statistics or a single witness value.
Quantum circuit equivalence checking asks whether two circuits implement the same unitary. It guarantees compiler correctness and safe optimization, yet most existing approaches scale exponentially with the number of qubits or the circuit depth, or are restricted to specific circuit structures. In this work, we present an equivalence-checking method for circuits formed by arbitrary single-qubit layers interleaved with Clifford layers. This pattern is common in variational quantum algorithms and Hamiltonian simulation via Trotter decomposition. It can also represent any unitary with sufficient depth. We prove the existence of an efficient classical algorithm that determines whether a pair of circuits with shared single-qubit layers are equivalent for every possible choice of the shared single-qubit unitaries. The same algorithm can also certify their non-equivalence for fixed assignments of single-qubit unitaries. Our framework supports the validation of emerging quantum compilers and facilitate the discovery of novel circuit optimization passes.
We present a depth-aware optimization framework for quantum circuit compilation that unifies provable optimality with scalable heuristics. For exact synthesis of a target unitary, we formulate a mixed-integer linear program (MILP) that linearly handles global-phase equivalence and uses explicit parallel scheduling variables to certify depth-optimal solutions for small-to-medium circuits. Domain-specific valid constraints, including identity ordering, commuting-gate pruning, short-sequence redundancy cuts, and Hermitian-conjugate linkages, significantly accelerate branch-and-bound, yielding speedups up to 43x on standard benchmarks. The framework supports hardware-aware objectives, enabling fault-tolerant (e.g. T-count) and NISQ-era (e.g. entangling gates) devices. For approximate synthesis, we propose 3 objectives: (i) exact, but non-convex, phase-invariant fidelity maximization; (ii) a linear surrogate that maximizes the real trace overlap, yielding a tight lower bound to fidelity; and (iii) a convex quadratic function that minimizes the circuit's Frobenius error. To scale beyond exact MILP, we propose a novel rolling-horizon optimization (RHO) that rolls primarily in time, caps the active-qubits, and enforces per-qubit closure while globally optimizing windowed segments. This preserves local context, reduces the Hilbert-space dimension, and enables iterative improvements without ancillas. On a 142-gate seed circuit, RHO yields 116 gates, an 18.3% reduction from the seed, while avoiding the trade-off between myopic passes and long run times. Empirically, our exact compilation framework achieves certified depth-optimal circuits on standard targets, high-fidelity Fibonacci-anyon weaves, and a 36% gate-count reduction on multi-body parity circuits. All methods are in the open-source QuantumCircuitOpt, providing a single framework that bridges exact certification and scalable synthesis.
Limited qubit connectivity is a central architectural constraint in superconducting quantum processors, whose planar layouts require additional gates to mediate interactions between distant qubits. Here, we use the AshN control scheme, where rich two-qubit control on every nearest-neighbour pair allows a logical interaction and the required qubit routing to be merged into a single native operation, effectively transforming a sparse hardware graph into a more connected computational architecture. For the benchmark instances studied, the resulting synthesis capability enables reliable execution on constrained one- and two-dimensional lattices, with compiled two-qubit gate counts approaching those of an all-to-all-connected reference. Across seven benchmark circuits on one- and two-dimensional topologies, the AshN-based implementation achieves geometric-mean reductions of 45.2% and 43.7% in two-qubit gate count compared with controlled-Z-based compilation, respectively. Using AshN gates, we prepare an eight-qubit two-excitation Dicke state with a fidelity of 0.736 and certify its genuine multipartite entanglement using a fully positive-partial-transpose witness, whereas the same witness does not certify entanglement for the CZ-based implementation. The state fidelity and entanglement certification remain robust across the tested lattice configurations, including those with up to three connectivity defects. Our work establishes native-gate engineering as a practical approach to mitigating connectivity constraints.
Quantum circuit compilation is a crucial step in the realization of quantum computation, transforming high-level quantum algorithms into gate-level operations executable on specific quantum hardware. However, this process is inherently complex and susceptible to errors, including gate decomposition errors, qubit mapping errors, and resource allocation errors. These errors can significantly degrade the fidelity of the final computation. This paper proposes and investigates the application of formal verification techniques to guarantee the correctness of quantum circuit compilation. We demonstrate how model checking and formal methods can be applied to rigorously verify that the compilation algorithm adheres to predefined constraints, such as preserving quantum properties like unitary evolution and qubit orthogonality. The core claim is that formal verification offers a robust solution to the challenges of detecting and preventing errors in quantum compilation. The proposed approach significantly advances the reliability and trustworthiness of quantum computing by providing a rigorous method for ensuring compilation accuracy. We outline a framework for applying these techniques, focusing on key constraints and illustrating their application through a simplified compilation scenario.
Quantum computers are reaching a level where interactions between classical and quantum computations can happen in real-time. This marks the advent of a new, broader class of quantum circuits: dynamic quantum circuits. They offer a broader range of available computing primitives that lead to new challenges for design tasks such as simulation, compilation, and verification. Due to the non-unitary nature of dynamic circuit primitives, most existing techniques and tools for these tasks are no longer applicable in an out-of-the-box fashion. In this work, we discuss the resulting consequences for quantum circuit verification, specifically equivalence checking, and propose two different schemes that eventually allow to treat the involved circuits as if they did not contain non-unitaries at all. As a result, we demonstrate methodically, as well as, experimentally that existing techniques for verifying the equivalence of quantum circuits can be kept applicable for this broader class of circuits.