Source-linked AI summary
Challenging Benchmarks for Diagrammatic Equivalence of Circuits in TPTP and SMT-LIB
Julie Cailler, Noé Delorme, Sophie Tourret
TL;DR
Diagrammatic equivalence asks whether circuit terms can be rewritten into one another under coherence equations, a problem relevant to certifying quantum-circuit equivalences. The paper introduces three benchmark variants, first-order encodings, and parameterizable generation scripts, then evaluates them with automated provers and SMT solvers. The experiments show that the problem remains challenging, with cvc5 generally outperforming Vampire and performance depending on wires and term size.
Problem
Diagrammatic equivalence requires deciding whether two circuit terms can be rewritten into one another using coherence equations.
Method
The paper introduces three variants and provides first-order encodings, benchmark-generation tools, and parameterizable scripts for producing instances.
Results
Current automated provers find diagrammatic equivalence challenging; cvc5 solves more instances across benchmark families than Vampire, while wires and term size affect performance.
Takeaways & Limitations
The benchmarks provide a challenge for automated reasoning, particularly at the interaction between arithmetic and equational reasoning.
Takeaways & Limitations
Most ATPs with proof-production capabilities do not handle arithmetic, motivating interest in arithmetic-free encodings that correctly capture the guards.
Abstract
from arXiv · showhide
We introduce a new family of benchmarks for the problem of diagrammatic equivalence between circuits. Three variants of this problem are considered, ranging from basic to challenging, and benchmarks are generated for each variant. We provide first-order encodings in both TPTP and SMT-LIB formats, together with scripts that automatically generate benchmark instances, and evaluate these benchmarks on state-of-the-art automated theorem provers and SMT solvers.
1 Introduction
The paper introduces benchmark families for diagrammatic equivalence of circuits, motivated by proof certification and the need for new repository contributions. It defines three problem variants and provides encodings, generation tools, and evaluations for automated reasoning systems.
- Contribution context: The contribution responds to limited new benchmark contributions by making curated circuit-equivalence benchmarks and production tools available to the research community.Preparing reproducible archives and curating repository additions requires substantial effort that is not well rewarded.
- Problem motivation: The benchmarks originate from efforts to produce certificates for proofs of quantum-circuit equivalence.The paper situates circuit equivalence within graphical languages and diagrammatic reasoning.
- Problem motivation: The work addresses diagrammatic equivalence: deciding whether two circuit terms can be rewritten into one another using coherence equations.Circuits may have different syntactic forms while representing the same diagram.
- Benchmark construction: It provides tools that generate diagrammatically equivalent terms and benchmark instances for automated theorem provers.The benchmarks are presented as a challenge for the ATP community because prover performance is modest and certificate-production techniques remain immature.
- Benchmark variants: The paper introduces three variants, ranging from the general setting to permutation circuits and a simpler restricted configuration.The second variant has no generators and expresses permutations; the third restricts that setting further.
- Paper scope: The paper describes the variants, their encodings, benchmark-generation tools, and evaluations on state-of-the-art ATPs, with experiment materials available on Zenodo.The stated encodings and benchmark formats are developed in the paper’s later sections.
2 Problem Description
Circuits are terms built from generators, identities, swaps, and sequential or parallel composition, with coherence equations identifying syntactically different representations of the same diagram. The paper studies three equivalence problems—general circuits, permutation circuits, and simplified permutation circuits—and encodes them as challenging benchmark problems.
- Circuits and Their Graphical Representation: Circuits are terms generated from primitive generators under sequential and parallel composition, with inputs and outputs represented by wires.Sequential composition is drawn horizontally, while parallel composition is drawn vertically.
- Circuits and Their Graphical Representation: Coherence equations ensure that syntactically distinct circuit terms representing the same diagram are equivalent.The induced congruence relation corresponds to diagrammatic equivalence and relates equivalent circuits to isomorphic graphs.
- Challenging Equivalence Checking Problems: The paper frames these three variants as challenging equivalence-checking benchmarks for automated theorem provers.The general circuit setting is connected to graph isomorphism in the CE case, whose complexity is described as quasi-polynomial, although general circuit-equivalence complexity is not established.
- Challenging Equivalence Checking Problems: Circuit Equivalence (CE) is the general decision problem of determining whether two circuits can be rewritten into one another under the coherence equations.The paper encodes this equivalence-checking problem in SMT-LIB and TPTP to produce challenging benchmarks.
- Challenging Equivalence Checking Problems: Permutation Circuit Equivalence (PCE) restricts CE to circuits without generators, where every size-n circuit represents a permutation of n wires.This restriction corresponds to the case Σ = ∅, so circuits consist solely of wires with equal input and output counts.
- Challenging Equivalence Checking Problems: Simplified Permutation Circuit Equivalence (SPCE) further restricts PCE to concrete permutations expressed using only id, σ, sequential composition, and parallel composition.Its coherence equations simplify accordingly, including the disappearance of rules involving empty circuits.
3 Encodings
The paper encodes three diagrammatic-equivalence variants as first-order theories over circuit terms, using guarded coherence equations to preserve properness. It supplies these encodings in SMT-LIB and TPTP formats.
- Theory files: The three variants are encoded as first-order theories with equality and linear arithmetic constraints in SMT-LIB and TPTP.SMT-LIB uses UFLIA, while TPTP uses typed first-order logic in TFF format.
- Circuit syntax: Circuit terms comprise identities, swaps, generators, sequential composition, and parallel composition.The encoding computes input and output arities recursively for each constructor.
- Circuit syntax: Terms are an over-approximation of circuits, so properness requires matching wire arities across compositions.For example, seq(id(2), id(3)) is syntactically valid but improperly typed.
- Guarded equations: Ungarded coherence equations can equate proper and improper terms, producing contradictions.The encoding therefore adds guards to ambiguous equations, including sequential identity and interchange.
- Permutation encodings: Permutation circuits remove generators from the syntax, while SPCE further reduces terms to id, swap, seq, and par.SPCE fixes id and swap arities and uses simplified coherence equations to reduce arithmetic reasoning.
- Permutation encodings: SPCE still requires an interchange guard because term ordering cannot orient the rule left-to-right across all equivalent terms.The attempted guard elimination was abandoned because global orientation could not be preserved.
4 Benchmark Generators
The benchmark generators create equivalent but syntactically distinct terms in three problem classes through graphical construction, equivalence-preserving rewrites, and term extraction. Each class has dedicated automated generation scripts.
- Overview: The benchmark suite targets CE, PCE, and SPCE, with dedicated instances and generation tools for each class.The generators produce equality problems between two syntactically distinct yet diagrammatically equivalent terms.
- SPCE generation: SPCE begins with an id-only rectangular grid, adds binary swaps, and rewrites subgrids using simplified coherence rules.The transformations include (idid)e2, (idswap)e2, (inv)e2, and (yaba)e2.
- SPCE generation: SPCE translates transformed grids into sequential or parallel terms after checking that selected cuts do not break swaps.The script supports vertical and horizontal splits.
- PCE generation: PCE extends SPCE with arbitrary-size swaps, symmetry and involution patterns, and rewrite rules for identity, symmetry, and involution.Its maximal swap size is controlled by the -a parameter, while -s controls the number of rule applications.
- PCE generation: PCE also rewrites parallel identity compositions into equivalent decompositions and validates that corresponding input wires exit at the same positions.For example, par(id(2), id(3)) may become id(5) or par(id(1), id(4)).
- CE generation: CE constructs planar acyclic graphs from arbitrary generators, layers them topologically, inserts identities for alignment, and extracts equivalent terms by node merging.The generator can optionally restrict nodes to Clifford generators H, S, and CNOT.
5 Evaluations
The evaluation measures benchmark difficulty and solver behavior across CE, PCE, and SPCE using arithmetic-capable, independently checkable proof-producing tools. cvc5 generally outperforms Vampire, while wire count and term size strongly affect performance.
- The evaluation targets benchmark difficulty and the practical impact of encodings and tool configurations.
- Tools: Vampire and cvc5 were selected because both support arithmetic reasoning and produce independently checkable proof certificates.
- Benchmark design: Each benchmark instance combines equivalent circuit terms with its corresponding theory file, and instances are parameterized by input-wire count and initial column count.
- Benchmark design: 100 problems were generated for each term-size interval, with instance sizes restricted to a ±5 window around each interval midpoint.For example, the [0, 25] interval contains 7–17 composition operators.
- Results: cvc5 outperforms Vampire across all benchmark families, solving more instances and scaling better as wire count and term size increase.
- Results: CE is the hardest category: cvc5 struggles above roughly 100 term-size units, while Vampire solves no problem above the [0–25] interval.For SPCE and PCE with 5 wires, cvc5 solves all instances across the tested term-size range.
6 Conclusion
The paper contributes a benchmark family for diagrammatic equivalence, covering three problem variants with TPTP and SMT-LIB encodings and parameterizable generators. Experiments show that current provers remain challenged, with cvc5 more robust than Vampire and arithmetic–equational interaction a central bottleneck.
- The paper introduces CE, PCE, and SPCE benchmarks with first-order encodings in TPTP and SMT-LIB and scripts for generating instances.
- cvc5 handles the guarded encodings more robustly than Vampire, solving more instances across all benchmark families.
- Arithmetic and equational reasoning remain a central bottleneck, while wire count and syntactic term size significantly affect performance across solvers and families.
- Future work includes arithmetic-free encodings and systematic variation of generation parameters to analyze coherence-rule bottlenecks and possible phase transitions.
- The benchmark suite and generation scripts are intended to stress-test solvers and support new techniques for reasoning about string diagrams and quantum circuits.