SumOverPaths Formalism: A New Approach to Quantum Computing Verification

The SumOverPaths (SOP) formalism is a method used in quantum computing to symbolically manipulate linear maps that describe quantum systems. Introduced in 2018, it translates from most common gate-based descriptions of quantum processes and simplifies the term without altering its semantics. The SOP formalism is used to check circuit equivalence in quantum computing, and has been applied in several projects, including noiseless simulation of quantum processes. Despite its limitations, the SOP formalism has been extended to account for families of morphisms and used to verify algorithms and routines such as quantum phase estimation, Grover’s search, and Shor’s algorithm.

What is the SumOverPaths Formalism in Quantum Computing?

The SumOverPaths (SOP) formalism is a method used to symbolically manipulate linear maps that describe quantum systems. It is a tool used in the formal verification of such systems. Introduced in 2018 by Amy, the SOP formalism has two key features. Firstly, it can translate from most common gate-based descriptions of quantum processes in polynomial time and space. This provides an intermediary view between usual matrix semantics and these usual process descriptions. Secondly, it comes equipped with a rewrite system that simplifies the term without altering its semantics.

The SOP formalism represents quantum processes as weighted sums of Dirac kets and bras, a notation familiar in quantum mechanics. Despite its links with graphical languages such as the ZH-calculus, it provides a different view on quantum processes. The formalism has seen several applications, the first of which being verification. Verification is a crucial aspect of computations in the quantum realm where physical constraints like no-cloning or the fundamental probabilistic nature of quantum make it impossible to do debugging the way we do on classical algorithms.

How is the SumOverPaths Formalism Used in Quantum Computing?

The SOP formalism was introduced as a solution to circuit equivalence. To check the equivalence between two circuits C1 and C2, the system represents C2 C1 as an SOP term where C2 can be seen as the inverse of C2. It then tries to reduce it to the identity. If successful, this proves C1 and C2 represent the same unitary. Otherwise, the system searches for a witness that the term at hand does not represent the identity. As such, the system has been used in several different projects to check precisely for circuit equivalence. It was later extended to account for families of morphisms and used within the Qbricks environment together with automated solvers to verify algorithms and routines such as quantum phase estimation, Grover’s search, and Shor’s algorithm.

Among other applications of the SOP, we may cite noiseless simulation of quantum processes where the rewrite strategy is used to reduce the number of variables in the term, effectively decreasing the number of summands when expanding the term to actually compute its semantics. It is for instance one of the simulators implemented in the supercomputer Atos QLM.

What are the Limitations and Extensions of the SumOverPaths Formalism?

While the initial suggestion for SOP focussed on the Clifford+T fragment, a universal fragment of quantum computing, it also provided some interesting result for the Clifford fragment. It is known that the latter is not universal and actually efficiently simulable with a classical computer, so it is a good test for the relevance of a formalism to check how it handles them. And indeed, it was shown a weak form of confluence of the rewrite system in the Clifford fragment. More precisely, in this fragment C2 C1 reduces in polynomial time to the identity if and only if C2 and C1 represent the same unitary operator.

However, SOP terms may represent more than unitary operator but actually any linear map. With those, it is still possible to define the above restrictions and the rewrite system was extended to get confluence for the not necessarily unitary Clifford fragment. When moving to a universal fragment like Clifford+T, it is expected that we cannot provide a rewrite system with all the good properties of the Clifford case.

How Does the SumOverPaths Formalism Connect to Quantum Computing Theory?

The reason for this is that if we could provide such a system, deciding circuit equivalence would become polynomial while we know that it is QMA-complete, a quantum variant of NP-complete. A weaker property than that of confluence we can ask for is completeness. The question here is to decide whether two equivalent terms can be turned into one another with the assumption that rewrites can be used in both directions. In that case, we rather speak of an equation.

The author, Renaud Vilmart from Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, LMF, provides a new set of rewrite rules for the SOP formalism and shows that it is complete for Toffoli-Hadamard, the simplest approximately universal fragment of quantum mechanics. He shows that the rewriting is terminating but not confluent, which is expected from the universality of the fragment. He does so using the connection between SOP and graphical language ZH-calculus and also shows how the axiomatisation translates into the latter.

What are the Future Directions for the SumOverPaths Formalism?

Vilmart provides generalisations of the presented rewrite rules that can prove useful when trying to reduce terms in practice and shows how to graphically make sense of these new rules. He shows how to enrich the rewrite system to reach completeness for the dyadic fragments of quantum computation used in particular in the Quantum Fourier Transform and obtained by adding phase gates with dyadic multiples of π to the Toffoli-Hadamard gate set.

Finally, he shows how to perform sums and concatenation of arbitrary terms, something which is not native in a system designed for analysing gate-based quantum computation but necessary when considering Hamiltonian-based quantum computation. This work opens up new avenues for the application and extension of the SOP formalism in quantum computing.