The Measurement Problem

A major problem of intuition that physicists find in the formalism of quantum mechanics is the so-called measurement problem. According to experimental evidence, a quantum system in a superposition of states, say \(|\psi\rangle = \alpha |0\rangle + \beta |1\rangle\), when measured as either \(|0\rangle\) or \(|1\rangle\), will report either 0 or 1 and the superposition will collapse to the measured state. There are many reasons why this is an issue. The first and most fundamental is probably that this makes a categorical distinction between the object being observed and the subject observing it. However, the subject is also a quantum system that evolves and can be observed by another observer. There is no reasonable solution to this issue: if one considers the line of interactions from the observed system to the 'conscious' observation (whatever that means) and passing through all the measurement apparatus and human biology, there is no single point where the system changed from object to subject. This is not a matter of continuity vs discreteness or something special about consciousness either as demonstrated by the Wigner's friend thought experiment. In the experiment, Wigner stands outside a room where his friend performs a quantum measurement on a system. Wigner's friend then observes the collapse of the wavefunction; however, Wigner, who is outside the room, has not measured anything; therefore, he still considers the system's evolution to be unitary and when Wigner measures the system himself, he is supposed to still possibly observe a different outcome than his friend's.

A solution to this problem is to forget the conscious observer and consider that everything and everyone (the entire Universe) is a single composite quantum system. In this case, the apparent collapse of the wavefunction is nothing more than an entanglement between the observed system and the observer within the Hilbert space of the Universe as a whole. Therefore, what Wigner sees is that the system experiment-friend still follows unitary evolutions, but the state of Wigner's friend and that of the system can no longer be faithfully described independently of one another. This is known as the many-worlds interpretation. The reason it's called many-worlds is, at least in my way of seeing it, that since we cannot possibly describe the state of the entire Universe as a whole, we can gradually, at each measurement, augment the system we are describing by tensoring it with a new and entangled "copy" of itself. This "copy" represents part of the observer which has now become entangled with the observed system. Since it is not part of the system per se, we can imagine that the world has split into many, one for each possible outcome of the measurement and that the "conscious" observation is in only one of them. The advantage of this view is that, while the worlds are technically still in a superposition, we are not supposed to be able to apply transformations involving the observer, as it is not part of the system in question; therefore, worlds cannot interfere in any interesting ways. This is very informal, but bear with me, there is a formal version of each statement here, separately, but the notion of 'worlds' is metaphysical anyway, and it doesn't mean much, formally, beyond refuting collapse and using a universal wavefunction instead.

Path-sums and Hybrid Path-sums

Another, though indirect, inspiration for our work is the path-integral formulation of quantum mechanics, in particular, a discrete version of it known as path-sums [Amy18]. Path-sums exist in many forms, balanced [Amy18], unbalanced [Amy23], "double-sided" [Vilmart22], and, in our work, hybrid [CIN+26], but the basic idea is quite simple. Let's say you're a high-school student, which you may be, (with educational inflation, you might need to be a bachelor's or even master's student, I guess), and you just learned some linear algebra and the basics of quantum computing: gates and circuits. Now, you have just seen the circuit for the quantum Fourier transform on \(10\) qubits, and it starts with a parallel Hadamard gate on all \(10\) qubits and you want to run through it to see its output on some input basis state \(|x_1\cdots x_{10}\rangle\). With all certainty, you will not explicitly write down \(2^{10} = 1024\) terms of the decomposition over the computational basis. Instead, you will likely write the following:

This is a path-sum. It is simply a symbolic sum describing a vector or a matrix or some other linear "object" compactly, without expanding all its terms. How you define its precise syntax and semantics gives you all the variations and is central to a computational application, but whatever you do, this is what a path-sum is. The paths are each of the assignments of the variables \(y_1,\ldots,y_{10}\), which are referred to as path variables.

Does this remind you of anything? The paths existing in parallel and in a superposition resemble, quite a lot, the worlds that exist in superposition in the many-worlds interpretation. Here's a question: how would you describe the state after measuring the first 5 qubits of \(|\psi\rangle\)? You could list the \(2^5 = 32\) possible outcomes, and the respective projections of the state, but more likely than not, you would also want to find a shortcut. If we look back at the interpretation of the measurement in the many-worlds model, we realize that all we need to do is to augment the system with 5 new "qubits" representing the parts of the measurement apparatus that needs to get entangled with the measured qubits, let's denote them \(|-\rangle_{A_1}\cdots |-\rangle_{A_5}\). We can entangle these qubits with the qubits of the system by copying the \(|y_i\rangle\) values into them. Indeed, in the path where the state of the first qubit is \(|y_i\rangle\), the measurement outcome is \(y_i\). As such, we get the following hybrid path-sum:

Then, you can interpret this hybrid path-sum by considering that the \(A_i\) qubits are not really accessible. This gives you a set of \(2^5\) worlds, in each of which, the state can be described by a sum over the remaining 5 path variables:

More generally, if the content of the \(A_i\) qubits was not just a standalone variable, but some more involved boolean function \(f_i(y_1,\ldots,y_{10})\) of the path variables, the splitting into worlds corresponds to a partition of the path space into \(2^5\) sets, with the projected (subnormalized) states being given by

And voilà, that's our work! Well, of course not, but that's the core idea.

Equivalence and refinement

If this ancilla system, the \(A_i\) qubits, is seen as a set of classical bits, the hybrid path-sum becomes a compact representation of a quantum-classical system. That, in itself, is quite great, but to unlock its full potential, we need methods to manipulate, simplify, and check the equivalence of these path-sums. By being able to check the equivalence of two hybrid-path sums, we can check the equivalence of two quantum-classical programs, an essential task for the verification of a range of tasks, from quantum circuit optimization to compilation, and more. Furthermore, if we can describe the specification of a quantum-classical program itself as a hybrid path-sum, equivalence checking becomes functional verification. Another approach is to relate hybrid path-sums with a "refinement" relation \(h_1 \preceq h_2\) which says, roughly speaking, that the hybrid path-sum \(h_1\) is a more detailed description of the system than \(h_2\). In this context, specifications no longer need to be exact, but the verification can still be done by tools similar to equivalence checking.

Practically speaking, the tools we are talking about concern a rewriting system given by a set of concrete rules of the form \(h_1 \to h_2\) where if some pattern is found in \(h_1\), then, \(h_1\) can be replaced by an equivalent path-sum \(h_2\). If there is a path of rewrites from some specification path-sum \(h_s\) to the path-sum of the program \(h_p\), then, \(h_s\) and \(h_p\) are equivalent, and the program satisfies its specification. Similarly, we can define a set of refinement rules where \(h_p \to h_s\) means that \(h_p\) is a refinement of \(h_s\) and the program, again, satisfies its specification.

I do not wish to elaborate more on the technical aspects here and instead refer the reader to the article itself [CIN+26] as well as the implementation of the corresponding tool, HQbricks, available on GitHub.

Bibliography