Table of Contents
Fetching ...

MIP*=RE

Zhengfeng Ji, Anand Natarajan, Thomas Vidick, John Wright, Henry Yuen

TL;DR

This work proves a groundbreaking equivalence: the class of languages decidable by a classical verifier interacting with multiple entangled quantum provers, MIP*(2,1), equals the recursively enumerable languages RE. The authors achieve this by constructing a gap-preserving, compression-based interactive proof framework that iteratively compresses large questions and complex verifications into smaller, conditionally linear distributions, while preserving completeness and entanglement requirements. Central to the method are the CL distributions, introspection games, and PCP-based answer reduction, all integrated via an anchored parallel-repetition scheme to maintain a robust gap across recursion. The resulting RE ⊆ *^*(2,1) together with the known trivial upper bound *^* ⊆ RE yields *^* = RE, with profound consequences: undecidability of entangled-value problems, a negative resolution to Tsirelson’s problem, and a refutation of Connes’ Embedding Conjecture, alongside explicit entanglement-tested constructions and a richer understanding of prover/round reductions in quantum-proof systems.

Abstract

We show that the class MIP* of languages that can be decided by a classical verifier interacting with multiple all-powerful quantum provers sharing entanglement is equal to the class RE of recursively enumerable languages. Our proof builds upon the quantum low-degree test of (Natarajan and Vidick, FOCS 2018) and the classical low-individual degree test of (Ji, et al., 2020) by integrating recent developments from (Natarajan and Wright, FOCS 2019) and combining them with the recursive compression framework of (Fitzsimons et al., STOC 2019). An immediate byproduct of our result is that there is an efficient reduction from the Halting Problem to the problem of deciding whether a two-player nonlocal game has entangled value $1$ or at most $1/2$. Using a known connection, undecidability of the entangled value implies a negative answer to Tsirelson's problem: we show, by providing an explicit example, that the closure $C_{qa}$ of the set of quantum tensor product correlations is strictly included in the set $C_{qc}$ of quantum commuting correlations. Following work of (Fritz, Rev. Math. Phys. 2012) and (Junge et al., J. Math. Phys. 2011) our results provide a refutation of Connes' embedding conjecture from the theory of von Neumann algebras.

MIP*=RE

TL;DR

This work proves a groundbreaking equivalence: the class of languages decidable by a classical verifier interacting with multiple entangled quantum provers, MIP*(2,1), equals the recursively enumerable languages RE. The authors achieve this by constructing a gap-preserving, compression-based interactive proof framework that iteratively compresses large questions and complex verifications into smaller, conditionally linear distributions, while preserving completeness and entanglement requirements. Central to the method are the CL distributions, introspection games, and PCP-based answer reduction, all integrated via an anchored parallel-repetition scheme to maintain a robust gap across recursion. The resulting RE ⊆ *^*(2,1) together with the known trivial upper bound *^* ⊆ RE yields *^* = RE, with profound consequences: undecidability of entangled-value problems, a negative resolution to Tsirelson’s problem, and a refutation of Connes’ Embedding Conjecture, alongside explicit entanglement-tested constructions and a richer understanding of prover/round reductions in quantum-proof systems.

Abstract

We show that the class MIP* of languages that can be decided by a classical verifier interacting with multiple all-powerful quantum provers sharing entanglement is equal to the class RE of recursively enumerable languages. Our proof builds upon the quantum low-degree test of (Natarajan and Vidick, FOCS 2018) and the classical low-individual degree test of (Ji, et al., 2020) by integrating recent developments from (Natarajan and Wright, FOCS 2019) and combining them with the recursive compression framework of (Fitzsimons et al., STOC 2019). An immediate byproduct of our result is that there is an efficient reduction from the Halting Problem to the problem of deciding whether a two-player nonlocal game has entangled value or at most . Using a known connection, undecidability of the entangled value implies a negative answer to Tsirelson's problem: we show, by providing an explicit example, that the closure of the set of quantum tensor product correlations is strictly included in the set of quantum commuting correlations. Following work of (Fritz, Rev. Math. Phys. 2012) and (Junge et al., J. Math. Phys. 2011) our results provide a refutation of Connes' embedding conjecture from the theory of von Neumann algebras.

Paper Structure

This paper contains 146 sections, 110 theorems, 565 equations, 17 figures, 2 tables.

Key Result

Theorem 2.1

There exists a polynomial-time Turing machine $\mathsf{Compress}$ that, when given as input the description of a normal form verifier $\mathcal{V} = (\mathcal{S},\mathcal{D})$, outputs the description of another normal form verifier $\mathcal{V}' = (\mathcal{S}',\mathcal{D}')$ that satisfies the fol

Figures (17)

  • Figure 1: An illustration of an $\ell$-level CL function $L$. First a register subspace $V_{1}$ and a linear map $L_{1}$ are chosen and applied to obtain $x^{L_{1}} = L_{1}(x^{V_{1}}) \in V_{1}$. Then depending the value of $x^{L_{1}}$, a register subspace $V_{2}$ and a linear map $L_{2,\,x^{L_{1}}}$ are chosen and applied to obtain $x^{L_{2}} = L_{2,\,x^{{L_{1}}}}(x^{V_{2}}) \in V_{2}$ and so on. Finally, $L(x)$ is defiend to be $\sum_{k=1}^{\ell} x^{L_{k}}$.
  • Figure 2: Specification of the conditionally linear functions corresponding to $G$.
  • Figure 3: The decision procedure $\mathcal{D}^\textsc{ld}$ for the simultaneous low-degree test, parameterized by $\mathsf{ldparams} = (q,m,d,k)$. The function $\chi(s)$ is defined in \ref{['eq:chi-func']}, and $\pi_{i-1}(v)$ zeroes out the first $i-1$ coordinates of $v$.
  • Figure 4: The Magic Square game
  • Figure 5: Type graph $G^\textsc{MS}\xspace$ for the Magic Square game.
  • ...and 12 more figures

Theorems & Definitions (322)

  • Theorem 2.1: Gap-preserving compression of normal form verifiers, informal
  • Theorem 3.1: Efficient universal Turing machine hartmanis1965computational
  • Definition 3.2: Register subspace
  • Definition 3.3
  • Lemma 3.4
  • proof
  • Definition 3.5
  • Definition 3.6
  • Remark 3.7
  • Remark 3.8
  • ...and 312 more