google-deepmind / google-deepmind/formal-conjectures

Formalize Open Quantum Problem #49: Single-prover interactive proofs for quantum computations

Open
#3,466 0 comments 0 reactions 0 assignees View on GitHub
new conjecture
Dominant language
Lean
Stars
1.3k
Forks
485
Avg merge
1d 20h
Merged PRs (30d)
327

Description

### What is the conjecture

This is problem [#49](https://oqp.iqoqi.oeaw.ac.at/single-prover-interactive-proofs-for-quantum-computations) in the [Open Quantum Problems collection](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems). [Note: At OQP, this conjecture is called #45, which is a double entry. Thus we call it #49].

> **Problem (Open Quantum Problem #49: “Single-prover interactive proofs for quantum computations”).**
> Find a single-prover interactive proof for polynomial-time quantum computations in which the verifier is fully classical, the honest prover needs only `BQP` power, and soundness holds against arbitrary cheating provers.

A standard formalization is in terms of **classical-verifier interactive proofs for `BQP`**:

* Let `L ⊆ {0,1}^*` be a language in `BQP`.
* A verifier `V` is a randomized classical polynomial-time interactive algorithm (a `BPP` machine) that exchanges only **classical messages** with a prover and outputs accept/reject after at most `poly(|x|)` rounds.
* An honest prover `P_hon` is a uniform polynomial-time quantum interactive machine (informally: a `BQP`-power prover).

The desired protocol `(V, P_hon)` should satisfy:

* **Completeness:** if `x ∈ L`, then `V` accepts after interacting with `P_hon` with high probability (say at least `2/3`).
* **Soundness:** if `x ∉ L`, then for every cheating prover strategy `P*` — even computationally unbounded — the verifier `V` accepts with probability at most `1/3`.

Then the main question is:

* **Main question / open complexity-theoretic problem:** does **every** `L ∈ BQP` admit such a protocol with
* a **fully classical verifier**,
* only **one prover**,
* an **honest prover implementable in quantum polynomial time**, and
* **information-theoretic / unconditional soundness** against all cheating provers?

Equivalently: can every efficient quantum computation be **classically verified** in the **single-prover** setting, without giving the verifier any quantum capability and without relying on computational assumptions?

Why this is nontrivial:

* By `IP = PSPACE` and `BQP ⊆ PSPACE`, there are already classical-verifier interactive proofs for `BQP` if the honest prover is allowed PSPACE power.
* The challenge is to keep the honest prover within `BQP`, while maintaining soundness against **arbitrary** provers.

The OQP page highlights several nearby relaxations / partial solutions:

* **Verifier with a constant quantum register:** Aharonov, Ben-Or, Eban, and Mahadev give protocols where the verifier is almost classical but can store/transmit a constant number of qubits.
* **Mostly-classical blind verification:** Broadbent, Fitzsimons, and Kashefi give blind verifiable delegation with a verifier that can prepare a few qubits.
* **Fully classical verifier with two provers:** Reichardt, Unger, and Vazirani give classical-verifier verification protocols using two non-communicating entangled provers.
* **Fully classical single-prover verification under cryptographic assumptions:** Mahadev gives such a protocol assuming hardness assumptions (notably LWE), with soundness against computationally bounded provers.

This is the **single-prover, fully classical, unconditional** version of the quantum computation verification problem.

### Where to find the details / references

Primary sources:

* [Open Quantum Problems site](https://oqp.iqoqi.oeaw.ac.at/single-prover-interactive-proofs-for-quantum-computations)
* [Open Quantum Problems master list (for numbering/metadata)](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems)

Key related references (as listed on the OQP page):

* C. Lund, L. Fortnow, H. Karloff, and N. Nisan, “Algebraic methods for interactive proof systems” (J. ACM 39(4), 859–868 (1992))
* A. Shamir, “IP = PSPACE” (J. ACM 39(4), 869–877 (1992))
* D. Aharonov, M. Ben-Or, E. Eban, and U. Mahadev, “Interactive Proofs for Quantum Computations” ([arXiv:1704.04487](https://arxiv.org/abs/1704.04487))
* A. Broadbent, J. Fitzsimons, and E. Kashefi, “Universal blind quantum computation” ([arXiv:0807.4154](https://arxiv.org/abs/0807.4154))
* B. W. Reichardt, F. Unger, and U. Vazirani, “Classical command of quantum systems” (Nature 496, 456–460 (2013); [arXiv:1209.0449](https://arxiv.org/abs/1209.0449))
* U. Mahadev, “Classical verification of quantum computations” ([arXiv:1804.01082](https://arxiv.org/abs/1804.01082))

(If you want to include one or two broader background pointers beyond the OQP page, Anne Broadbent’s “How to Verify a Quantum Computation” ([arXiv:1509.09180](https://arxiv.org/abs/1509.09180)) and the overview by Gheorghiu, Kapourniotis, and Kashefi, “Verification of quantum computation: An overview of existing approaches” ([arXiv:1709.06984](https://arxiv.org/abs/1709.06984)) are useful entry points, but the OQP references above are the core ones for writing the issue.)

### Prerequisites needed

* Computational complexity theory: `BQP`, `BPP`, `IP`, completeness/soundness, interactive proofs
* Basic quantum computation: quantum circuits, measurements, polynomial-time quantum algorithms
* Interactive-proof / delegation viewpoint: honest vs cheating prover, rounds/messages, verifier resource restrictions
* (For partial results) basic cryptographic assumptions such as LWE, and the distinction between computational and information-theoretic soundness
* (Optional) blind quantum computation, quantum authentication, and self-testing / nonlocal games for the multi-prover variants

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-81 (Quantum theory)
* ams-68 (Computer science)
* ams-94 (Information and communication theory)

### Choose either option

* [ ] I plan on adding this conjecture to the repository
* [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---

Contributor guide

Open the contributing guide

Research direction

Start with the Open Quantum Problems page and the cited interactive-proof references to understand the conjecture and its prerequisites. Then inspect existing formalized conjectures in this repository for the expected statement structure. Done means adding a suitable formal statement for Problem #49 and having it accepted by the repository's checks.

Written by the indexing model from the issue text.

Assessment

Domain
content
Issue type
Feature
Difficulty
5/5
Estimated time
Over a week
Activity status
Stale
Clarity
Needs clarification
Newbie friendliness
20/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.