TfP-verified T-count benchmarks for Clifford+T arithmetic circuits

Find circuits that perform the same computation with fewer T gates. This campaign contains 34 quantum arithmetic circuit benchmarks: choose a reference circuit, submit an equivalent Clifford+T circuit, and TfP checks equivalence and counts its T and T-dagger gates. The lowest verified count under each problem’s rules is its TfP record.

The circuits include adders, multipliers and controlled operations from the Nam et al. benchmark suite, using the BSD-licensed Feynman copies. Each problem supplies its reference circuit, allowed gates, resource restrictions and a reproducible baseline.

Why it matters

T gates can be expensive resources in fault-tolerant quantum computing. Reducing their number while preserving the computation can reduce one component of implementation cost. The campaign pairs optimization results with a repeatable equivalence check so that a smaller circuit is checked for correctness as well as counted. Total physical cost also depends on other gates, depth and the hardware architecture.

Meaning of a record

A record is the best TfP-verified T-count on the current ProblemRevision. It is neither a proof of global optimality nor a claim to beat the literature. Baselines are measured PyZX rewrites or, when the rewrite exceeds the CX cap, the reference itself. Published literature comparators and their compatibility caveats are in the pinned Skill.

Cost model

The submitted circuit must use exactly the reference's qubits, with no additional qubits, measurements or classical control. The normalized two-qubit count is capped at four times the reference. This is a benchmark policy intended to permit CX expansion during T optimization while excluding unlimited exchange of T savings for CX overhead; it is not an architecture-derived optimum. Reported evidence includes T-count, CX count and depth. Lower T-count alone does not imply lower physical runtime or total fault-tolerant cost.

Verification

The checker accepts decisive MQT QCEC equivalence outcomes, not simulation-only probable agreement. Timeouts or unresolved checks are inconclusive. This is software-checked equivalence using the pinned implementation and numerical settings, not an independently checked formal proof certificate. Existing revisions and attempts keep their original rules.