Advancing Quantum Computing with Formal Methods

TL;DR

This paper introduces the application of formal methods, specifically weighted model counting, to analyze quantum circuits, aiming to inspire further research in combining quantum computing and formal verification techniques.

Contribution

It demonstrates how formal methods like weighted model counting can be used to analyze quantum circuits, bridging the gap between quantum computing and formal verification.

Findings

Weighted model counting can effectively analyze quantum circuits.

Quantum circuits' combinatorial complexity poses analysis challenges.

Formal methods can be adapted to quantum computing analysis.

Abstract

This tutorial introduces quantum computing with a focus on the applicability of formal methods in this relatively new domain. We describe quantum circuits and convey an understanding of their inherent combinatorial nature and the exponential blow-up that makes them hard to analyze. Then, we show how weighted model counting (\#SAT) can be used to solve hard analysis tasks for quantum circuits. This tutorial is aimed at everyone in the formal methods community with an interest in quantum computing. Familiarity with quantum computing is not required, but basic linear algebra knowledge (particularly matrix multiplication and basis vectors) is a prerequisite. The goal of the tutorial is to inspire the community to advance the development of quantum computing with formal methods.