Quantum Information Theorems in Proof Assistants

A formally verified quantum program satisfies a theorem about a specified mathematical semantics. The key question is what equivalence that semantics preserves: a unitary matrix, a channel, outcome probabilities, selected branches, or an approximation bound. These distinctions determine whether a verified replacement remains valid inside a larger quantum protocol. This page studies those interfaces using published formal developments as examples, without claiming a comprehensive survey of current libraries.

Required background. Finite-Dimensional QM Formalization defines state, channel, and tensor interfaces; Quantum Instruments distinguishes branch maps from their normalized conditional states.

A correctness theorem compares denotations

For a circuit language with interpretation $\llbracket C\rrbracket$, an optimizer can be specified by

$$\llbracket\operatorname{opt}(C)\rrbracket =\llbracket C\rrbracket$$

for every well-formed circuit $C$. The theorem quantifies over a family of programs, unlike testing finitely many circuits on finitely many inputs. Its usefulness depends on an explicit interpretation: which gates, registers, measurements, and control structures the language contains.

Hietala and collaborators’ VOQC work provides a concrete example: circuits are represented in SQIR, and optimization functions are proved to preserve their symbolic matrix semantics in Coq. The paper illustrates a reusable semantic interface and proofs for program transformations. This statement about the published artifact is distinct from independently rebuilding a chosen revision or verifying a hardware implementation of the output.

Equivalence must survive the intended context

For a unitary $U$, the channel $\rho\mapsto U\rho U^*$ is unchanged by replacing $U$ with $e^{i\theta}U$. Thus equality of channels is weaker than equality of unitary matrices. At the top level of a closed circuit, an overall phase has no effect on outcome probabilities.

Controlled use changes the issue. Define

$$\operatorname{ctrl}(U) =|0\rangle\langle0|\otimes I +|1\rangle\langle1|\otimes U.$$

Replacing $U$ by $e^{i\theta}U$ changes the relative phase of the control branches. That is generally observable. Consequently a rewrite justified only up to global phase cannot automatically be lifted through an operation that adds coherent control. The formal language needs a stronger equality, explicit phase tracking, or a proof that the chosen context respects the weaker equivalence.

This is a mathematical specification issue, not a limitation of symbolic matrix multiplication. A proof assistant can correctly verify either equivalence if asked the corresponding question.

Reference systems strengthen protocol specifications

A protocol claimed to implement an identity channel on a subsystem must preserve its correlations with an untouched reference. Checking a few isolated input vectors does not establish that claim. In finite dimension, equality of linear maps on a full operator basis establishes channel equality, which then extends after tensoring with the identity reference map. The basis must span the operator space, including coherences.

For example, a dephasing channel fixes every computational-basis state but destroys off-diagonal operators. Testing only those basis density matrices misses the error. A formal teleportation specification should express the output channel and retained classical or quantum registers, not just the success of selected basis-state tests.

Register abstractions help make these subsystem claims explicit. Unruh’s Quantum and Classical Registers development in Isabelle formalizes compatible registers and their composition, with quantum and classical instances. It is an example of representing the accessible part of a larger memory through an interface rather than repeated coordinate-index manipulations.

Branch probabilities, termination, and approximation errors

A measurement branch is a completely positive trace-nonincreasing map. Equality of its normalized outputs alone omits the success probability. A correct instrument comparison must preserve the relevant subnormalized branch maps or explicitly specify what records are discarded.

For a quantum program with a loop, a denotation can be trace nonincreasing because some executions do not terminate. Proving a postcondition on terminating runs does not establish almost-sure termination. A total-correctness claim needs the additional termination argument under its input assumptions.

Approximate transformations require a metric and a composition theorem. An error measured only on isolated inputs is not automatically a bound with arbitrary reference entanglement. In finite dimensions, diamond-norm channel bounds are designed to control that extension; their computation and proof are additional work. An exact symbolic semantics also does not bound the calibration errors or noise of a physical processor.

Exercise: a global phase becomes a control phase

Compare $U=I$ and $V=-I$. They define the same channel on the target. Apply their controlled versions to $|+\rangle\otimes|\psi\rangle$. Give a measurement that distinguishes the outputs.

Solution

Controlled $I$ leaves the input unchanged. Controlled $-I$ sends it to $|-\rangle\otimes|\psi\rangle$. Measuring the control in the $\{|+\rangle,|-\rangle\}$ basis distinguishes them with certainty. The phase was global for the isolated target channel but became relative between the coherent control branches. A channel-level equivalence alone therefore does not justify this controlled replacement.

References

• Hietala, Kesha, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks, “A Verified Optimizer for Quantum Circuits,” Proceedings of the ACM on Programming Languages 5, POPL (2021), doi:10.1145/3434318, arXiv:1912.02250 — formal symbolic circuit semantics and verified optimization.
• Unruh, Dominique, “Quantum and Classical Registers,” Archive of Formal Proofs, 28 October 2021, formal development — register composition and subsystem reasoning.
• Watrous, John, The Theory of Quantum Information, Cambridge University Press, 2018, doi:10.1017/9781316848142 — channels, reference systems, and completely bounded trace norms.