Quantum algorithms in CSLib?

Stream: CSLib

[Maris Ozols]

Hi, everyone! I'm a professor at the University of Amsterdam working on quantum computing and quantum information. I am interested in formalizing some key quantum algorithms that are important in my research in Lean. Perhaps this can be done as part of CSLib by creating a quantum extension of Boole? I wonder if there are other people with background in quantum computing who might be interested in this endeavor?

My research interests are on using representation-theoretic techniques in quantum computing (more specifically, I'm interested in various generalizations of the Fourier transform). As a long-term goal, I would like to implement the quantum circuits and formalize their correctness for Fourier transform for symmetric group and Schur transform. Here is a brief summary of the current state of the art on these two.

Fourier transform for symmetric group

The original 1997 paper by Beals describes the ideas on a high level and doesn't contain any quantum circuits or pseudo code. A much more precise description of the algorithm was spelled out by Kawano and Sekigawa in 2016. However, my master's student recently found that their description of the algorithm and its analysis is incomplete. He is defending his thesis on Friday and we hope to turn it into a paper afterwards. I hope that it can be used as a basis for a blueprint for formalization.

Schur transform

Schur transform is a key subroutine in many quantum information tasks which implements the basis change appearing in the so-called Schur–Weyl duality which relates the representation theory of symmetric and unitary groups. A quantum algorithm for it was first described in these two papers by Bacon, Chuang and Harrow (I recommend the 2nd half of Harrow's PhD thesis from 2005 as a particularly good source). Unfortunately they don't give explicit quantum circuits. First explicit circuits (albeit with sub-optimal complexity) were provided by Kirby and Strauch in the special case of qubits.

An alternative approach to Schur transform was devised by Krovi in 2018 which makes use of the symmetric group Fourier transform. However, recently a mistake in the last step of his algorithm was discovered, so we posted a paper last month that corrects this error and provides a much more detailed analysis and description of the algorithm.

Together with a new PhD student who will start with me in January, we will be looking at implementing these two quantum algorithms and formally proving their correctness. If anyone else is interested in this subject, especially someone with more expertise in Lean, please let me know.

[Shreyas Srinivas]

There is a QuantumInfo repository which might be better suited for this

[Shreyas Srinivas]

They also have a channel https://leanprover.zulipchat.com/#narrow/channel/508986-Quantum-information

[Maris Ozols]

Thanks, I'm aware of it! I just wanted to stop by here and say "hi" because I wasn't aware of CSLib until I run into @George Tsoukalas last week. He got me in touch with @Swarat Chaudhuri who suggested I drop by here.

[Maris Ozols]

Here are some additional thoughts. While I have not seen the specification of the Boole language yet, my hope is that it can be extended with the following extra "quantum" functionality:

• A special variable nq that tells the current number of qubits.
• An operation ancilla k that adds k ancilla qubits initialized in state $|0\rangle$. It would increase nq by k and replaces the current nq-qubit state $|\Psi\rangle$ with $|\Psi\rangle \otimes |0\rangle^{\otimes k}$.
• An operation gate i U that applies unitary U on qubit i, where U comes from some predefined gate set. If U is a 2-qubit gate, it would be applied on qubits i and i+1.

I think this would be enough for the two algorithms I want to implement since they are fully coherent (they describe isometries with quantum input and quantum output, so they do not involve measurements).

For more general quantum algorithms you would also want something like this.

• An operation measure i that measures the i-th qubit in the standard basis and returns the boolean measurement outcome.
• An operation discard i that discards the i-th qubit. It effectively measures the qubit and forgets the measurement outcome. Since the post-measurement state is in product with the rest, the measured qubit can be removed.

An extra complication that these operations create is that one needs to deal with mixed states, which can be described either by density matrices or by explicit probabilistic mixtures of pure states. For the purposes of what I want to do, I think this won't be needed.

[Shreyas Srinivas]

I am not sure it will be that simple. There will have to be a way to enforce no cloning and loss of a qubit state after it is measured

[Shreyas Srinivas]

Measurements in the quantum sense are irreversible whereas in the classical setting. one can always read a memory location as many time as one wants to. Encoding this will require some linear resource usage system which might be a non trivial addition

[Maris Ozols]

No cloning follows from linearity, so enforcing linearity of gates should be enough.

[Maris Ozols]

I only have a rough idea how formal program verification works classically, so I'm likely naive about this. However, at least for the project I have in mind, measurements are not needed, so I hope that this will keep things much simpler than in the general case.

[Alex Meiburg]

I think Maris's idea makes sense, as long as your building it up from unitary gates and ancillae these properties (linearity, no cloning) will come along for free, philosophically these shouldn't have to be "extra" constraints to impose at any point

[Alex Meiburg]

I think a monad for unitary (or more generally, CPTP) operations might be the best way to do this then, esp. since it lets us build on lots of the convenient monadic work already in Lean.

[Alex Meiburg]

You can imagine a UnitaryM which you work with by building up these gate sets. It would track the total unitary you apply, and probably also the number of gates applied. (Other nice things you could track in the monad: gate depth (by tracking depth on each qubit; fidelity (when you're building a unitary A that you want to closely approximate another unitary B and to keep track of the running error.)

Then you can divide your circuit construction into separate operations on the monad, and talk about pre- and post-conditions for each and so on.

[Shreyas Srinivas]

Gates are unitary and reversible. Qubits are linear w.r.t. measurement

[Shreyas Srinivas]

Adding linearity is not a trivial thing afaik.

[Shreyas Srinivas]

the program logic you need to express this might be some linear separation logic on top of MoSel or something similar.

[Shreyas Srinivas]

For example : https://arxiv.org/abs/2102.00329

This is of course just the program logic. To make it work with good automation, we might want to build it on top of a framework like Loom.

[Chris Henson]

Hi @Maris Ozols, sorry this took me a bit to get to! To echo what others have said I am not exactly sure of the right place for your formalization, but I am sure it will be welcome somewhere. I am not one of the maintainers who is an expert in Boole, but my understanding is that it works by defining a Strata dialect that is used to generate the language. If such a thing is amenable to the formalization work you want to do, I would be happy to review, as I have some experience with quantum in Rocq (mostly via trying out Robert Rand's work). Even if you prefer to do a more bespoke embedding, I think this could be considered or there is the QuantumInfo repo as well.

As a side note, a few years ago I read your essay on the Solovay-Kitaev theorem and found it very useful! I did not know you were involved in formalization. I would love to help formalize it at some point if that hasn't been done already.

[Bas Spitters]

@Maris Ozols Have you looked at formalizations in Rocq and Isabelle?
E.g. (non-exhaustive!)
https://arxiv.org/abs/1912.02250
https://dl.acm.org/doi/10.1145/3571222
and the work on the Qwhile language for post-quantum cryptography:
https://dominique-unruh.github.io/qrhl-tool/install.html
https://www.isa-afp.org/search/?s=unruh
https://inria.hal.science/hal-03529301v1/document (EasyPQC)