Abstraqt: Analysis of Quantum Circuits via Abstract Stabilizer Simulation

The key idea of ABSTRAQT is to avoid tracking the exact state p of a quantum system and instead only track key aspects of p. To this end, we rely on the established framework of abstract interpretation [8, 9], which is traditionally used to analyze classical programs [10, 11] or neural networks [12] by describing sets of possible states without explicitly enumerating all of them. Here, we use abstract interpretation to describe the set of quantum states that could occur at a specific point during execution of a circuit, by over-approximating the summands that could occur in any of those quantum states p.Merging Summands. This allows us to curb the exponential blow-up of stabilizer simulation by merging multiple summands in Eq. (1) into an abstract single summand which over-approximates all summands, at the cost of lost precision. The key technical challenge addressed by our work is designing a suitable abstract domain to describe sets of summands, accompanied by the correspond-ing abstract transformers to over-approximate the actions performed by the original exponential stabilizer simulation on individual summands.