Synthesis of Compact and Expressive Quantum-Circuit Optimizations

Wei Qiang; Ronghui Gu

Source-linked AI summary

Synthesis of Compact and Expressive Quantum-Circuit Optimizations

Wei Qiang, Ronghui Gu

arXiv:2609.01762v1Sep 1, 2026cs.PL

TL;DR

Noisy quantum hardware and existing large, redundant rewrite-rule sets motivate more compact and expressive quantum-circuit optimization. Qsymb formalizes canonical symbolic rewriting, synthesizes bounded-complete concrete and expressive symbolic rules, and uses rule anchoring; it reports stronger benchmark reductions than existing rewrite-based optimizers.

Problem
Existing quantum rewrite optimizers can produce large, redundant rule sets and miss useful long-distance transformations, while noisy hardware makes circuit-size reduction important for reliable execution.
Method
Qsymb synthesizes non-derivable bounded-complete concrete rules and canonical symbolic rules, validates them, and applies rule anchoring to derive optimization-effective rules.
Results
Qsymb strictly outperforms Qiskit, Guoq, Quartz, TKET, and Queso in two-qubit-gate reduction on most standard benchmark comparisons across IBM-Eagle and Nam gate sets.
Takeaways & Limitations
Qsymb provides compact rewrite-rule sets with expressiveness and guarantees including soundness, non-derivability, and bounded completeness.
Takeaways & Limitations
Qsymb restricts synthesis to rules over at most 3 qubits because the search space grows exponentially with qubit count and rule size.

Abstract

from arXiv · show

Today's quantum devices are noisy, so reducing circuit size is critical for reliable execution. Existing rule-based optimizers often rely on large rule sets that are difficult to manage and still miss long-distance transformations. We present QSymb, a framework for synthesizing compact and expressive quantum-circuit rewrite rules with formal guarantees. We formalize symbolic rewrite rules in which a symbolic gate represents infinitely many subcircuits. We then define canonical symbolic rules of the form $L;S = S;R$ and prove that they constitute a compact generative core from which general symbolic rules can be derived. On top of this formal foundation, given a gate set, QSymb synthesizes (1) a small, non-derivable concrete rule set that is complete up to chosen size and qubit bounds, and (2) a small but expressive canonical symbolic rule set that captures transformations beyond finite or monomial-only patterns. We further present rule anchoring to derive optimization-effective rules from canonical symbolic rules. Together, these results provide both expressiveness and guarantees: soundness of synthesized rules via validation, non-derivability, and bounded completeness. On the IBM-Eagle gate set, QSymb strictly outperforms state-of-the-art rewrite-based optimizers (Qiskit, Guoq, Quartz, TKET, and Queso) in two-qubit-gate reduction on 90%, 67%, 82%, 85%, and 83% of standard quantum algorithm benchmarks, respectively; on Nam gate set, the corresponding rates are 88%, 74%, 81%, 86%, and 82.9%. It achieves final average two-qubit-gate reductions of 27.44% and 29.95%, respectively.

1 Introduction

Qsymb addresses the difficulty of building compact, expressive, and effective quantum-circuit optimizations for noisy hardware by synthesizing non-derivable concrete and canonical symbolic rewrite rules.

Motivation: Noisy quantum hardware makes compiled-circuit efficiency important for reliable execution.Short coherence times, gate errors, and restricted qubit connectivity can severely affect practical execution.
Motivation: Existing rewrite-based optimizers can generate many redundant or derivable rules while missing useful transformations.This motivates seeking more compact rule sets with broader expressive coverage.
Approach: Qsymb formalizes symbolic rewrite rules whose variables represent infinite subcircuit spaces and introduces canonical rules as a compact generative basis.Canonical rules have the form L;S = S;R, from which other symbolic rules can be derived.
Contributions: Qsymb synthesizes a smaller non-derivable concrete rule set that remains complete for circuits within chosen size and qubit bounds.The framework also synthesizes expressive canonical symbolic rules and supports rule anchoring for deriving more useful rules.
Contributions: The framework combines equality-saturation-based concrete-rule inference, symbolic-rule synthesis, and rule anchoring, and integrates the resulting rules with simple optimizers.The authors report that the resulting optimizer outperforms state-of-the-art rewrite-based optimizers.

2 Background

The background defines quantum states, gates, circuit semantics, rewrite rules, equivalence classes, and equality saturation as the formal basis for Qsymb.

Quantum Gates: A qubit has basis states 0 and 1 and may occupy a normalized superposition of them.An n-qubit state is represented using 2^n basis states, and measurement probabilities are determined by squared amplitudes.
Quantum Gates: Quantum operations transform qubit states; X acts like NOT, H creates superposition, and CNOT conditionally flips its target.CNOT flips the second qubit when the first qubit is 1.
Matrix Semantics: Quantum circuits are gate sequences whose operations are represented by unitary matrices.Sequential gates compose by matrix multiplication, while parallel gates compose using tensor products.
Path Sum Representation: Path-sum notation represents a gate using input states, path variables, symbolic angles, phase polynomials, and output functions.Multiple paths represent superposition, whereas monomial gates have a single path.
Quantum Rewrite Rule: Two circuits are equivalent when their matrix semantics agree up to a global phase, and a rewrite rule pairs such semantically equivalent circuits.Rewrite rules can be composed to transform longer circuits.
Quantum Rewrite Rule: An equivalence circuit class contains equivalent circuits, and a set of such classes is (n,q)-complete when bounded rewrites can be derived by composition.The bounds refer to circuit size and qubit count.
Equality Saturation: Equality saturation stores equivalent terms in e-graphs, adds matching rewrites until saturation, and extracts the lowest-cost term.Qsymb uses equality saturation to check whether rewrite rules are derivable from smaller rules.

3 Overview

Qsymb synthesizes compact concrete and symbolic rewrite rules, using canonical symbolic forms and anchoring to represent broader transformations while retaining derivability guarantees.

Concrete and symbolic rule synthesis: Qsymb builds a small, non-derivable concrete rule set that is complete for circuits within chosen size and qubit bounds.It enumerates circuits, groups equivalent terms, and removes transformations already derivable from learned rules.
Rule anchoring: Rule anchoring selectively appends prefixes or suffixes to canonical rules so concrete rewrite rules can apply after symbolic subcircuits.For CX cancellation, anchoring moves CX gates together so a concrete cancellation rule can remove them.
Concrete and symbolic rule synthesis: Qsymb models S with symbolic constraints that can represent infinitely many subcircuits, including subcircuits that induce superposition.This extends beyond symbolic gates restricted to monomial subcircuits.
Concrete and symbolic rule synthesis: Canonical symbolic rules have the form L;S = S;R and provide a compact generative basis for deriving general symbolic rules.Qsymb proves that symbolic rules can be reduced to and derived from canonical forms.
Rule anchoring: Qsymb addresses symbolic-rule synthesis challenges by grouping L and R with similar properties and avoiding direct solution of unitary constraints on S.The grouping method can determine whether a unitary solution exists while avoiding checks of all candidate pairs.

4 Synthesizing Concrete Rules

Qsymb combines equality saturation, equivalence-class grouping, pruning, and canonicalization to infer a compact set of concrete rules without retaining derivable transformations.

Bottom-Up Synthesis Algorithm: Qsymb groups enumerated quantum terms into equivalence classes using a Polynomial Identity Filter before inferring candidate rewrite rules.PIF keeps the probability of mixing semantically different circuits extremely low.
Bottom-Up Synthesis Algorithm: Equality saturation identifies candidate rules already derivable from learned rules, allowing Qsymb to discard redundant transformations.A candidate is derivable when its left- and right-hand sides enter the same e-class.
Bottom-Up Synthesis Algorithm: The synthesized concrete rule set derives all valid transformations formed by terms up to size n and qubit bound q.The enumeration procedure covers every circuit term within the specified bounds.
Bottom-Up Synthesis Algorithm: Priority ordering selects smaller and more abstract rules first, while pruning removes representative and common-prefix or common-suffix redundancies.For rules with the same structure, the most general valid rule is selected first.
Bottom-Up Synthesis Algorithm: Canonicalization merges rules with the same meaning across different qubit identities into a single generalized rule.For example, equivalent X-cancellation rules on distinct qubits become one rule parameterized by q.

5 Synthesizing Symbolic Rewrite Rules

Qsymb represents symbolic subcircuits through matrices and constraints, enabling rules that cover infinitely many unitary instantiations while addressing the costs of large rule sets and nonlinear validation.

Motivation: Large concrete rule sets increase synthesis and optimization costs, while small sets struggle to compose long-distance rewrites.Equality saturation may require many iterations, and search methods may take longer to discover large equivalences.
Symbolic Rule Representation: A symbolic rule represents a subcircuit variable S within concrete circuit contexts, with matching and substitution performed on the two occurrences of S.The left-hand occurrence matches a subcircuit, while the right-hand occurrence marks its replacement position.
Symbolic Rule Representation: Qsymb seeks a representation of S that captures the complete set of unitary interpretations preserving equivalence between both sides of the rule.It represents this solution set with a symbolic matrix used during matching.
Symbolic Matrix Constraints: A 4 × 4 symbolic matrix models the intermediate subcircuit of CX cancellation, with complex variables constrained by S S† = I.Expanding unitarity produces nonlinear equations, illustrated by the corresponding constraints.
Symbolic Matrix Constraints: Qsymb must enforce both circuit equivalence and the existence of a unitary solution, but direct enumeration and nonlinear solving scale poorly.The framework therefore develops an approach that infers candidate solutions without directly checking all nonlinear equations.

5.3 Canonical Symbolic Rules and Property Grouping

Qsymb reduces symbolic-rule synthesis to canonical forms, derives general rules from them, and groups candidates using spectral properties before solving linear systems.

Challenges: Symbolic terms are difficult to group because symbolic variables have infinitely many instantiations, and checking every candidate’s constraints is expensive.These challenges motivate necessary-condition grouping and canonicalization.
Canonical Forms: Under the finite-inverse gate-set assumption, every symbolic rule can be reduced to a canonical rule of the form L;S = S;R.The theorem establishes equivalence between the original rule and its canonical form.
Canonical Forms: Canonical rules generate broader symbolic rules by appending circuits implementing suitable unitary matrices to both sides.This provides a compact generative basis rather than enumerating every general symbolic-rule form.
Rule Derivation: The RZ-merging rule is derived from a canonical form by appending an RZ gate and applying a concrete rule that merges two RZ gates.This example illustrates how canonical rules become optimization-oriented rules.
Property Grouping: Qsymb groups candidate pairs first by trace and then by eigenvalues with multiplicities, using necessary conditions for a unitary intertwiner.Equal traces alone are insufficient, so eigenvalue checks further filter candidates.
Property Grouping: For grouped pairs, Qsymb solves a linear intertwining system and obtains S through the nullspace of K(R,L).The system uses K(R,L) = I_n ⊗ R − L^T ⊗ I_n for n × n matrices.

5.4 Synthesis Algorithm

The synthesis algorithm extracts representative concrete terms, groups them by sampled traces, solves linear systems for symbolic solutions, and validates eigenvalues to retain sound rules.

Candidate Generation: Algorithm 2 starts from one representative term for each equivalence class produced by equality saturation during concrete-rule synthesis.This reuses concrete equivalence information to limit symbolic candidates.
Candidate Grouping: Qsymb groups terms by concrete traces computed after evaluating symbolic angles at sampled values.Grouping reduces the number of candidate pairs considered.
Solution Construction: For each pair within a group, the algorithm solves the intertwining equation and obtains basis matrices whose linear combinations define S.Candidates with no basis solution are discarded before validation.
Validation: Eigenvalue validation determines whether a unitary solution exists, avoiding direct solution of S’s nonlinear unitary constraints.The grouping and validation stages eliminate many invalid symbolic rules early.
Guarantees: Every bounded symbolic rule is derivable from the generated canonical symbolic and concrete rules, while each generated canonical rule is non-derivable from the others.These properties provide bounded completeness and a nonredundant canonical set.
Guarantees: The resulting compact symbolic-rule set represents a large family of circuit equivalences because symbolic variables can denote infinitely many unitary matrices.The synthesis process therefore combines compactness with broad symbolic coverage.

5.5 Checking Constraints

Qsymb applies a symbolic rule by matching its concrete pattern, checking the matched circuit against the symbolic matrix constraint, and verifying consistency across unconstrained qubits.

Constraint Checking: Matching maps the symbolic variable S to a concrete subcircuit C, while the rule’s concrete components must match syntactically.The matched circuit’s unitary matrix is then tested as a model of the symbolic matrix.
Constraint Checking: A CX-cancellation symbolic rule can match a subcircuit when its concrete matrix admits an assignment satisfying the symbolic matrix constraint.The example assigns complex values to the symbolic matrix variables and applies the rule after validation.
Constraint Checking: Qsymb can match a k-qubit symbolic matrix to an n-qubit subcircuit when k < n, provided the constrained qubits transform correctly.It additionally checks that interactions with remaining qubits keep L;C and C;R consistent.

5.6 Anchoring Canonical Rules

Qsymb anchors canonical symbolic rules by selectively appending prefixes or suffixes that enable later concrete rewrites. This preserves a compact rule basis while deriving optimization-effective extensions.

Canonical symbolic rules are mostly size-preserving and move concrete parts around a symbolic subcircuit.Size-reducing transformations can sometimes be enabled directly by appending prefixes or suffixes.
Qsymb selectively instantiates anchored variants likely to collaborate with concrete rules, avoiding exhaustive prefix and suffix enumeration.The technique appends carefully chosen prefixes or suffixes to both sides of canonical rules.
Anchoring maintains valid rules and ensures that an anchored symbolic rewrite can be followed by a concrete rewrite.The full anchored set includes derived rules and canonical rules that produce no further anchored extensions.
In the example, matching a symbolic parameter enables appending a concrete suffix to both sides, after which an existing concrete rule can reduce size.Only the anchored symbolic extension is retained; the subsequent size-reducing transformation occurs during runtime optimization.

6 Applying Rules

Qsymb applies concrete rules through equality saturation and symbolic rules through stochastic search. The optimizer alternates these mechanisms until timeout and extracts the lowest-cost circuit found.

Qsymb integrates generated rules with equality saturation and simulated annealing-style search-based optimization.Concrete rules are integrated into equality-saturation engines, while symbolic rules support broader transformations.
Algorithm 3 alternates equality-saturation iterations with stochastic symbolic-rule applications inside a timeout-controlled loop.Each symbolic step randomly selects a rule, matches its left-hand side, and applies it when a matching subcircuit exists.
The optimizer extracts the current lowest-cost circuit and updates the best circuit whenever the cost decreases.The algorithm returns the best circuit after repeated search iterations.
A smaller matching window accelerates individual matches, while larger transformations can still be achieved through multiple symbolic rewrites.The search can optimize circuits larger than the selected window through successive symbolic applications.

7 Implementation and Evaluation

Qsymb combines compact concrete rules, symbolic-rule synthesis, anchoring, and simple optimization algorithms in a broad evaluation. Across gate sets and benchmarks, it reduces synthesis cost and improves optimization results.

Implementation: Qsymb is implemented with Java and Python components for rule synthesis, symbolic constraint solving, and equality saturation.The implementation uses SymPy for symbolic matrix systems and egglog for e-graphs.
Evaluation: The evaluation asks how Qsymb compares with prior synthesis engines and optimizers, and how grouping, symbolic rules, and anchoring affect performance.These questions are tested through rule-size, synthesis-time, optimization, and ablation experiments.
Rewrite Rule Synthesis: Qsymb generates concrete rule sets 26x–191x smaller than prior sets while still deriving all rules generated by Queso and Quartz.The comparison spans IBM-Eagle, Rigetti, ion-trap, and Nam gate sets.
Symbolic Rules: Property-based grouping yields an average 11.6x speedup for canonical symbolic-rule synthesis.Across gate sets, measured speedups range from 7.3x to 17.0x.
Metrics: The metric is percentage reduction in two-qubit-gate count, supplemented by circuit fidelity where hardware calibration data are available.Two-qubit gates are emphasized because they typically have higher error rates on NISQ hardware.
Optimization Performance: On IBM-Eagle, Qsymb strictly outperforms Qiskit, Guoq, Quartz, TKET, and Queso in two-qubit reduction on 90%, 67%, 82%, 85%, and 83% of benchmarks.For fidelity, the corresponding rates are 89%, 78%, 94%, 87%, and 87%.
Optimization Performance: Full Qsymb reaches final average two-qubit reductions of 27.44% on IBM-Eagle and 29.95% on Nam, while continuing to improve after ten minutes.It converges faster and reaches better final results than Queso and Quartz in the reported comparison.

8 Discussion and Future Work

Qsymb’s synthesis remains bounded because the search space grows exponentially with qubit count and rule size. The paper identifies machine-learning guidance and resynthesis integration as future directions.

Qsymb restricts synthesis to rules over at most 3 qubits because the search space grows exponentially with qubit count and rule size.Larger rules may be eliminated by the e-graph and do not necessarily improve optimization.
Machine-learning guidance for symbolic-rule application and integration with resynthesis techniques are left for future work.The paper specifically mentions using an LLM to analyze circuit structure and guide symbolic-rule application.

9 Related Work

Prior quantum-circuit optimization spans hand-crafted rules, graphical rewriting, verified compilers, and synthesized rewrite systems. Qsymb combines equality saturation, SMT validation, bounded completeness, and broader symbolic-rule support than highlighted prior synthesizers.

Queso synthesizes rewrite rules and checks equivalence with efficient polynomial testing but does not use SMT-based checking, potentially permitting low-probability false positives.
Queso supports only symbolic circuits with monomial gates, whereas Qsymb supports symbolic rules whose variables represent infinite structures.
Qsymb uses equality saturation for concrete-rule synthesis, producing a smaller SMT-validated rule set with (n,q)-completeness.
Most quantum-circuit compilers rely on fixed sets of hand-crafted optimizations, while PyZX applies graphical rewrite rules from ZX calculus.
VOQC provides a formally verified quantum-circuit optimizer built on Coq, and Giallar uses SMT-based automated verification for Qiskit optimizations.
Qsymb’s concrete rule inference relates to equality-saturation systems such as Ruler and Enumo, while integrating a domain-specific polynomial identity filter.