Authors:

Sarthak T

Date Created:

Not specified

Course Title:

Professor:

Not specified

About Paper:

Quantum circuit cutting-decomposing large quantum programs into smaller subcircuits-has emerged as a key technique for scaling computations beyond current hardware limitations. However, ensuring the correctness of such decompositions under realistic noise remains an open challenge. This research presents ZX-Checker, a formal verification tool that extends the ZX-calculus to reason about circuit cutting in the presence of global noise models. The approach embeds ZX-diagrams into the category CPM(Qubit) using a double-wire construction, enabling symbolic modeling of completely positive tracepreserving (CPTP) maps. ZX-Checker implements a modified ZX-calculus, expressing noisy circuit fragments as linear combinations of enriched ZX-diagrams and simulating their reconstruction via algebraic rewriting. By integrating categorical quantum mechanics with automated rewriting and simulation, ZX-Checker offers a mathematically rigorous framework for verifying noise-aware circuit decompositions. This enables scalable, provably correct compilation pipelines for near-term quantum devices, advancing the formal methods toolkit available for noisy intermediate-scale quantum (NISQ) computing. Keywords: Quantum Computing; Quantum Error Correction; ZX Calculus; Quantum Verification

Source:

Purdue University / 2025

Topics:

No topics listed

Co-authors:

Sarthak T