Symbolic Specification and Reasoning for Quantum Data and Operations

TL;DR

This paper introduces a formal logical framework, Symbolic Operator Logic (SOL), enabling symbolic specification and reasoning about quantum data and operations, bridging classical logic and quantum verification tools.

Contribution

It presents the first comprehensive logical framework for symbolic reasoning in quantum computing, integrating classical logic with quantum data operations.

Findings

Framework enables reasoning about quantum data properties

Embedding classical logic facilitates use of existing verification tools

Supports formal verification in proof assistants like Lean and Coq

Abstract

In quantum information and computation research, symbolic methods have been widely used for human specification and reasoning about quantum states and operations. At the same time, they are essential for ensuring the scalability and efficiency of automated reasoning and verification tools for quantum algorithms and programs. However, a formal theory for symbolic specification and reasoning about quantum data and operations is still lacking, which significantly limits the practical applicability of automated verification techniques in quantum computing. In this paper, we present a general logical framework, called Symbolic Operator Logic $\mathbf{SOL}$, which enables symbolic specification and reasoning about quantum data and operations. Within this framework, a classical first-order logical language is embedded into a language of formal operators used to specify quantum data and operations, including their recursive definitions. This embedding allows reasoning about their properties modulo a chosen theory of the underlying classical data (e.g., Boolean algebra or group theory), thereby leveraging existing automated verification tools developed for classical computing. It should be emphasised that this embedding of classical first-order logic into $\mathbf{SOL}$ is precisely what makes the symbolic method possible. We envision that this framework can provide a conceptual foundation for the formal verification and automated theorem proving of quantum computation and information in proof assistants such as Lean, Coq, and related systems.