Symbolic Specification and Reasoning for Quantum Data and Operations
Mingsheng Ying
TL;DR
Symbolic Operator Logic (SOL) provides a two-layer framework built on a classical first-order logic to enable symbolic specification and reasoning about quantum data and operations. By treating formal operators as parameterized expressions over classical variables and defining entailment modulo underlying classical theories, SOL aims to leverage classical verification tools such as proof assistants for quantum reasoning. The paper formalizes the syntax, signatures, and semantics of SOL, demonstrates basic and recursive symbolic reasoning about quantum data, and outlines concrete applications in proof assistants, program verification, symbolic execution, and model checking. It also discusses future directions, including incorporating super-operators and integrating with alternative quantum representations, to enhance scalability and practical applicability.
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.