arXiv:2001.04383v1 [quant-ph] 13 Jan 2020
MIP
∗
=
RE
Zhengfeng Ji
∗
1
, Anand Natarajan
†
2,3
, Thomas Vidick
‡
3
, John Wright
§
2,3,4
, and Henry Yuen
¶
5
1
Centre for Quantum Software and Information, University of
Technology Sydney
2
Institute for Quantum Information and Matter, California I
nstitute of Technology
3
Department of Computing and Mathematical Sciences, Califo
rnia Institute of Technology
4
Department of Computer Science, University of Texas at Aust
in
5
Department of Computer Science and Department of Mathemati
cs, University of Toronto
January 14, 2020
Abstract
We show that the class
MIP
∗
of languages that can be decided by a classical verifier inter
acting with
multiple all-powerful quantum provers sharing entangleme
nt is equal to the class
RE
of recursively enu-
merable languages. Our proof builds upon the quantum low-de
gree test of (Natarajan and Vidick, FOCS
2018) by integrating recent developments from (Natarajan a
nd 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 effici
ent reduction from the Halting Problem
to the problem of deciding whether a two-player nonlocal gam
e has entangled value
1
or at most
1
2
.
Using a known connection, undecidability of the entangled v
alue 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. Ma
th. Phys. 2011) our results provide a
refutation of Connes’ embedding conjecture from the theory
of von Neumann algebras.
∗
Email: zhengfeng.ji@uts.edu.au
†
Email: anandn@caltech.edu
‡
Email: vidick@caltech.edu
§
Email: wright@cs.utexas.edu
¶
Email: hyuen@cs.toronto.edu
1
Contents
1 Introduction
4
1.1 Interactive proof systems . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . .
5
1.2 Statement of result . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . .
9
1.3 Consequences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . .
11
1.4 Open questions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . .
13
2 Proof Overview
15
3 Preliminaries
22
3.1 Turing machines . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . .
22
3.2 Linear spaces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . .
23
3.3 Finite fields . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . .
25
3.3.1 Subfields and bases . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . .
25
3.3.2 Bit string representations . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . .
28
3.4 Low-degree encoding . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . .
30
3.4.1 A canonical injection . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . .
31
3.5 Linear spaces and registers . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . .
33
3.6 Measurements and observables . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . .
33
3.7 Generalized Pauli observables . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . .
34
4 Conditionally Linear Functions, Distributions, and Samp
lers
37
4.1 Conditionally linear functions and distributions . . . .
. . . . . . . . . . . . . . . . . . . .
37
4.2 Conditionally linear samplers . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . .
42
5 Nonlocal Games
45
5.1 Games and strategies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . .
45
5.2 Distance measures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . .
46
5.3 Self-testing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . .
49
5.4 Normal form verifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . .
50
6 Types
51
6.1 Typed samplers, deciders, and verifiers . . . . . . . . . . . . . .
. . . . . . . . . . . . . . .
51
6.2 Graph distributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . .
53
6.3 Detyping typed verifiers . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . .
55
7 Classical and Quantum Low-degree Tests
58
7.1 The classical low-degree test . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . .
58
7.1.1 The game . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
.
58
7.1.2 Conditionally linear functions for the plane-point d
istribution . . . . . . . . . . . .
60
7.1.3 Complexity of the classical low-degree test. . . . . . . .
. . . . . . . . . . . . . . .
62
7.2 The Magic Square game . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . .
62
7.3 The Pauli basis test . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . .
66
7.3.1 The game . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
.
66
7.3.2 Conditional linear functions for the Pauli basis test
. . . . . . . . . . . . . . . . . .
72
2
7.3.3 Canonical parameters and complexity of the Pauli basi
s test . . . . . . . . . . . . .
73
8 Introspection Games
75
8.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . .
75
8.2 The introspective verifier . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . .
76
8.3 Completeness and complexity of the introspective verifi
er . . . . . . . . . . . . . . . . . . .
82
8.3.1 Preliminary lemmas . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . .
82
8.3.2 Complexity and completeness of the introspective ver
ifier . . . . . . . . . . . . . .
84
8.4 Soundness of the introspective verifier . . . . . . . . . . . . . .
. . . . . . . . . . . . . . .
87
8.4.1 The Pauli twirl . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . .
87
8.4.2 Preliminary lemmas . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . .
93
8.4.3 Proof of Theorem
8.9
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
95
9 Oracularization
104
9.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . .
104
9.2 Oracularizing normal form verifiers . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . .
104
9.3 Completeness and complexity of the oracularized verifie
r . . . . . . . . . . . . . . . . . . .
105
9.4 Soundness of the oracularized verifier . . . . . . . . . . . . . . .
. . . . . . . . . . . . . .
107
10 Answer Reduction
109
10.1 Circuit preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . .
110
10.2 A Cook-Levin theorem for bounded deciders . . . . . . . . . . .
. . . . . . . . . . . . . .
110
10.3 A succinct 5SAT description for deciders . . . . . . . . . . . .
. . . . . . . . . . . . . . .
118
10.4 A PCP for normal form deciders . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . .
122
10.4.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . .
122
10.4.2 The PCP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
.
124
10.5 A normal form verifier for the PCP . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . .
129
10.5.1 Parameters and notation . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . .
129
10.5.2 The answer-reduced verifier . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . .
130
10.6 Completeness and complexity of the answer-reduced ver
ifier . . . . . . . . . . . . . . . . .
131
10.7 Soundness of the answer-reduced verifier . . . . . . . . . . . .
. . . . . . . . . . . . . . .
134
11 Parallel Repetition
142
11.1 The anchoring transformation . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . .
142
11.2 Parallel repetition of anchored games . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . .
143
12 Gap-preserving Compression
146
12.1 Proof of Theorem
12.2
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
147
12.2 The Kleene-Rogers fixed point theorem . . . . . . . . . . . . . . .
. . . . . . . . . . . . .
152
12.3 An
MIP
∗
protocol for the Halting problem . . . . . . . . . . . . . . . . . . . . . . .
. . . .
154
12.4 An explicit separation . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . .
159
3
1 Introduction
For integer
n
,
k
≥
2
define the quantum (spatial) correlation set
C
qs
(
n
,
k
)
as the subset of
R
n
2
k
2
that
contains all tuples
(
p
abxy
)
representing families of bipartite distributions that can
be locally generated in
non-relativistic quantum mechanics. Formally,
(
p
abxy
)
∈
C
qs
(
n
,
k
)
if and only if there exist separable
Hilbert spaces
H
A
and
H
B
, for every
x
∈ {
1, . . . ,
n
}
(resp.
y
∈ {
1, . . . ,
n
}
), a collection of projec-
tions
{
A
x
a
}
a
∈{
1,...,
k
}
on
H
A
(resp.
{
B
y
b
}
b
∈{
1,...,
k
}
on
H
B
) that sum to identity, and a state (unit vector)
ψ
∈ H
A
⊗ H
B
such that
∀
x
,
y
∈ {
1, 2, . . . ,
n
}
,
∀
a
,
b
∈ {
1, 2, . . . ,
k
}
,
p
abxy
=
ψ
∗
A
x
a
⊗
B
y
b
ψ
.
(1)
Note that due to the normalization conditions on
ψ
and on
{
A
x
a
}
and
{
B
y
b
}
, for each
x
,
y
,
(
p
abxy
)
is a
probability distribution on
{
1, 2, . . . ,
k
}
2
. By taking direct sums it is easy to see that the set
C
qs
(
n
,
k
)
is
convex. Let
C
qa
(
n
,
k
)
denote its closure (it is known that
C
qs
(
n
,
k
)
6
=
C
qa
(
n
,
k
)
, see [
Slo19a
]).
Our main result is that the family of sets
{
C
qa
(
n
,
k
)
}
n
,
k
∈
N
is extraordinarily complex, in the following
computational sense. For any
0
<
ε
<
1
define the
ε
-
weak membership problem
for
C
qa
as the problem of
deciding, given
n
,
k
∈
N
and a point
p
= (
p
abxy
)
∈
R
n
2
k
2
, whether
p
lies in
C
qa
(
n
,
k
)
or is
ε
-far from
it in
ℓ
1
distance, promised that one is the case. Then we show that for
any given
0
<
ε
<
1
the
ε
-weak
membership problem for
C
qa
cannot be solved by a Turing machine that halts with the corre
ct answer on
every input.
We show this by directly reducing the Halting problem to the w
eak membership problem for
C
qa
: we
show that for all
0
<
ε
<
1
and any Turing machine
M
one can efficiently compute integers
n
,
k
∈
N
and
a linear functional
ℓ
M
on
R
n
2
k
2
such that, whenever
M
halts it holds that
sup
p
∈
C
qa
(
n
,
k
)
ℓ
M
(
p
)
=
1 ,
(2)
whereas if
M
does not halt then
sup
p
∈
C
qa
(
n
,
k
)
ℓ
M
(
p
)
≤
1
−
ε
.
(3)
By standard results in convex optimization, this implies th
e aforementioned claim on the undecidability of
the
ε
-weak membership problem for
C
qa
(for any
0
<
ε
<
1
).
Our result has interesting consequences for long-standing
conjectures in quantum information theory and
the theory of von Neumann algebras. Through a connection tha
t follows from the work of Navascues, Piro-
nio, and Acin [
NPA08
] the undecidability result implies a negative answer to Tsi
relson’s problem [
Tsi06
].
Let
C
qc
(
n
,
k
)
denote the set of quantum commuting correlations, which is t
he set of tuples
(
p
abxy
)
arising
from operators
{
A
x
a
}
and
{
B
y
b
}
acting on a single Hilbert space
H
and a state
ψ
∈ H
such that
∀
x
,
y
∈ {
1, . . . ,
n
}
,
∀
a
,
b
∈ {
1, . . . ,
k
}
,
p
abxy
=
ψ
∗
A
x
a
B
y
b
ψ
and
A
x
a
,
B
y
b
=
0 .
(4)
Then
Tsirelson’s problem
asks if, for all
n
,
k
, the sets
C
qa
(
n
,
k
)
and
C
qc
(
n
,
k
)
are equal. Using results
from [
NPA08
] we give integer
n
,
k
and an explicit linear function
ℓ
on
R
n
2
k
2
such that
sup
p
∈
C
qc
(
n
,
k
)
ℓ
(
p
)
=
1 ,
but
sup
p
∈
C
qa
(
n
,
k
)
ℓ
(
p
)
≤
1
2
,
which implies that
C
qa
(
n
,
k
)
6
=
C
qc
(
n
,
k
)
. By an implication of Fritz [
Fri12
] and Junge et al. [
JNP
+
11
]
we further obtain that Connes’ Embedding Conjecture [
Con76
] is false; in other words, there exist type II
1
4
von Neumann factors that do not embed in an ultrapower of the h
yperfinite II
1
factor. We explain these
connections in more detail in Section
1.3
below.
Our approach to constructing such linear functionals on cor
relation sets goes through the theory of inter-
active proofs from complexity theory. To explain this conne
ction we first review the concept of interactive
proofs. The reader familiar with interactive proofs may ski
p the next section to arrive directly at a formal
statement of our main complexity-theoretic result in Secti
on
1.2
.
1.1 Interactive proof systems
An
interactive proof system
is an abstraction that generalizes the familiar notion of
proof
. Intuitively, given
a formal statement
z
(for example, “this graph admits a proper
3
-coloring”), a proof
π
for
z
is information
that enables one to check the validity of
z
more efficiently than without access to the proof (in this exa
mple,
π
could be an explicit assignment of colors to each vertex of th
e graph).
Complexity theory formalizes the notion of proof in a way tha
t emphasizes the role played by the veri-
fication procedure. To explain this, first recall that in comp
lexity theory a
language
L
is a subset of
{
0, 1
}
∗
,
the set of all bit strings of any length, that intuitively rep
resents all problem instances to which the answer
should be “yes”. For example, the language
L
=
3-C
OLORING
contains all strings
z
such that
z
is the
description (according to some pre-specified encoding sche
me) of a
3
-colorable graph
G
. We say that a
language
L
admits efficiently verifiable proofs if there exists an algor
ithm
V
(formally, a polynomial-time
Turing machine) that satisfies the following two properties
: (i) for any
z
∈
L
there is a string
π
such that
V
(
z
,
π
)
returns
1
(we say that
V
“accepts”), and (ii) for any
z
/
∈
L
there is no string
π
such that
V
(
z
,
π
)
accepts. Property (i) is generally referred to as the
completeness
property, and (ii) is the
soundness
. The
set of all languages
L
with both these completeness and soundness properties is de
noted by the complexity
class
NP
.
Research in complexity and cryptography in the 1980s and 199
0s led to a significant generalization
of the notion of “efficiently verifiable proof”. The first modi
fication is to allow
randomized
verification
procedures by relaxing (i) and (ii) to
high probability
statements: every
z
∈
L
should have a proof
π
that is
accepted
with probability at least
c
(the completeness parameter), and for no
z
/
∈
L
should there be a proof
π
that is accepted
with probability larger than
s
(the soundness parameter). A common setting is to take
c
=
2
3
and
s
=
1
3
; standard amplification techniques reveal that the exact va
lues do not significantly affect
the class of languages that admit such proofs, provided that
they are chosen within reasonable bounds.
The second modification is to allow
interactive
verification. Informally, this means that instead of re-
ceiving a proof string
π
in its entirety and making a decision based on it, the verifica
tion algorithm (called
the “verifier”) instead communicates with another algorith
m called a “prover”, and based on the communi-
cation decides whether
z
∈
L
. There are no restrictions on the computational power of the
prover, whereas
the verifier is required to run in polynomial time.
1
To understand how randomization and interaction can help fo
r proof checking, consider the following
example of an interactive proof for the language G
RAPH
N
ON
-I
SOMORPHISM
, which contains all pairs of
graphs
(
G
0
,
G
1
)
such that
G
0
and
G
1
are
not
isomorphic.
2
It is not known if G
RAPH
N
ON
-I
SOMORPHISM
∈
NP
, because it is not clear how to give an efficiently verifiable p
roof string that two graphs
G
0
and
G
1
are
1
The reader may find the following mental model useful: in an in
teractive proof, an all-powerful prover is trying to convin
ce
a skeptical, but computationally limited, verifier that a st
ring
z
(known to both) lies in the set
L
, even when it may be that in fact
z
/
∈
L
. By interactively interrogating the prover, the verifier ca
n reject false claims, i.e. determine with high statistical
confidence
whether
z
∈
L
or not. Importantly, the verifier is allowed to probabilisti
cally and adaptively choose its messages to the prover.
2
Here and in the rest of the section, we implicitly assume that
graphs and tuples of graphs have a canonical encoding as bina
ry
strings.
5
not isomorphic. (A proof of isomorphism is, of course, trivi
al: given a bijection from the vertices of
G
0
to
those of
G
1
it is straightforward to verify that the bijection induces a
n isomorphism.) However, consider
the following
randomized
,
interactive
verification procedure. Suppose the input to the verifier and
prover
is a pair of
n
-vertex graphs
(
G
0
,
G
1
)
(if the graphs do not have the same number of vertices, they ar
e
trivially non-isomorphic and the verification procedure ca
n automatically accept). The verifier first selects
a uniformly random
b
∈ {
0, 1
}
and a uniformly random permutation
σ
of
{
1, . . . ,
n
}
and sends the graph
H
=
σ
(
G
b
)
to the prover. The prover is then supposed to respond with a bi
t
b
′
∈ {
0, 1
}
; if
b
′
=
b
the
verifier accepts and if
b
′
6
=
b
it rejects.
Clearly, if
G
0
and
G
1
are not isomorphic then there exists a prover strategy to com
pute
b
from
H
with
probability
1
: using its unlimited computational power, the prover can de
termine whether
H
is isomorphic
to
G
0
or to
G
1
. However, if
G
0
and
G
1
are
isomorphic then the distribution of
H
is uniform over the
isomorphism class of
G
0
, which is the same as the isomorphism class of
G
1
, and the prover (despite having
unlimited computational power) cannot distinguish betwee
n whether the verifier generated
H
using
G
0
or
G
1
. Thus the probability that
any
prover can correctly guess
b
′
=
b
is exactly
1
2
. As a result, we have
shown that the graph non-isomorphism problem has an interac
tive proof system with completeness
c
=
1
and soundness
s
=
1
2
. Note how little “information” is communicated by the prove
r: a single bit! The
extreme succinctness of the “proof” comes from the fact that
whether
G
0
is isomorphic to
G
1
determines
whether a prover can reliably compute, given the data availa
ble to it (which is
G
0
,
G
1
, and
H
), the correct
bit
b
.
We denote by
IP
the class of languages that admit randomized interactive pr
oof systems such as the one
just described. The class
IP
is easily seen to contain
NP
, but it is thought to be a much larger class: one
of the famous results of complexity theory is that
IP
is exactly the same as
PSPACE
[
LFKN90
,
Sha90
], the
class of languages decidable by Turing machines using polyn
omial space.
3
Thus a polynomial-time verifier,
when augmented with the ability to interrogate an all-power
ful prover and use randomization, can solve
computational problems that are (believed to be) vastly mor
e difficult than those that can be checked using
static, deterministic proofs (i.e.
NP
problems).
Multiprover interactive proofs.
We now discuss a generalization of interactive proofs calle
d
multiprover
interactive proofs
. Here, a polynomial-time verifier can interact with
two
(or more) provers to decide
whether a given instance
z
is in a language
L
or not. In this setting, after the verifier and all the provers
receive the common input
z
, the provers are not allowed to communicate with each other,
and the verifier
“cross-interrogates” the provers in order to decide if
z
∈
L
. The provers may coordinate a joint strategy
ahead of time, but once the protocol begins the provers can on
ly interact with the verifier. As we will see,
the extra condition that the provers cannot communicate wit
h each other is a powerful constraint that can be
leveraged by the verifier.
Consider the computational problem of deciding membership
in a
promise
language called G
AP
-M
AXCUT
.
A promise language
L
is specified by two disjoint subsets
L
yes
,
L
no
⊆ {
0, 1
}
∗
, and the task is to decide
whether a given instance
z
is in
L
yes
or
L
no
, promised that
z
∈
L
yes
∪
L
no
. In a proof system for a promise
language, the completeness case consists of accepting with
probability at least
c
if
z
∈
L
yes
, and the sound-
ness case consists of accepting with probability at most
s
if
z
∈
L
no
. If
z
/
∈
L
yes
∪
L
no
, then there are no
constraints on the behavior of the verifier.
The promise language G
AP
-M
AXCUT
is defined as follows: G
AP
-M
AXCUT
yes
(resp. G
AP
-M
AXCUT
no
)
3
The reason
PSPACE
is considered a “difficult” class of problems is because many
computational problems believed to require
super-polynomial or exponential time (such as 3-C
OLORING
or deciding whether a quantified Boolean formula is true) can
be
solved using a polynomial amount of space.
6
is the set of all graphs
G
with a
cut
(i.e. a bipartition of the vertices) such that at least
90%
of edges cross
the cut (resp. at most
60%
of edges cross the cut).
4
For simplicity, we also assume that all graphs in
G
AP
-M
AXCUT
yes
∪
G
AP
-M
AXCUT
no
are regular, i.e. the degree is a constant across all vertice
s in the
graph.
The G
AP
-M
AXCUT
problem clearly lies in
NP
, since given a candidate cut it is easy to count the number
of edges that cross it and verify that it is at least
90%
of the total number of edges. Observe that the length
of the proof and the time required to verify it are linear in th
e size of the graph (the number of vertices and
edges).
Finding
the proof is of course much harder, but we are only concerned w
ith the complexity of the
verification procedure.
Now consider the following simple
two-prover interactive proof system
for G
AP
-M
AXCUT
. Given a
graph
G
, the verification procedure first samples a uniformly random
edge
e
=
{
u
,
v
}
in
G
. It then sends a
uniformly random
x
∈ {
u
,
v
}
to the first prover, and a uniformly random
y
∈ {
u
,
v
}
to the second prover.
Each prover sees its respective question only and is expecte
d to respond with a single bit,
a
,
b
∈ {
0, 1
}
respectively. The verification procedure accepts if and onl
y if
a
=
b
if
x
=
y
, and
a
6
=
b
if
x
6
=
y
.
We claim that the verification procedure described in the pre
ceding paragraph is a
multiprover interactive
proof system
for the language G
AP
-M
AXCUT
, with completeness
c
=
0.95
and soundness
s
=
0.9
, in the
following sense. First, whenever
G
∈
G
AP
-M
AXCUT
yes
then there is a successful strategy for the provers:
specifically, the provers can fix an optimal bipartition and c
onsistently answer “
0
” when asked about a vertex
from one side of the partition, and “
1
” when asked about a vertex from the other side; assuming ther
e exists
a cut that is crossed by at least
90%
of the edges, this strategy succeeds with probability at lea
st
1
2
+
1
2
0.9
,
where the first factor
1
2
arises from the case when both provers are sent the same verte
x, in which case they
always succeed.
Conversely, suppose given a strategy for the provers that is
accepted with probability
p
=
1
2
+
1
2
(
1
−
δ
)
when the verification procedure is executed on a (regular)
n
-vertex graph
G
. We then claim that
G
has a
cut crossed by at least a
1
−
2
δ
fraction of all edges. To show this, we leverage the non-comm
unication
assumption on the provers. Since either prover’s question i
s always a single vertex, their strategy can be rep-
resented by a function from the vertices of
G
to answers in
{
0, 1
}
. Any such function specifies a bipartition
of
G
. While the provers’ bipartitions need not be identical, the
fact that they succeed with high probability,
for the case when they are sent the same vertex, implies that t
hey must be consistent with high probability.
Finally, the fact that they also succeed with high probabili
ty when sent opposite endpoints of a randomly
chosen edge implies that either prover’s bipartition must b
e cut by a large number of edges. Taking the
contrapositive establishes the soundness property.
We denote by
MIP
the class of languages that have multiprover interactive pr
oof systems such as the
one described in the preceding paragraph. Note that, in comp
arison to the
NP
verification procedure for
G
AP
-M
AXCUT
considered earlier, the interactive, two-prover verificat
ion is much more efficient in terms
of the effort required for the verifier. Assuming the graph is
provided in a convenient format,
5
it is possible
to sample a random edge and verify the provers’ answers in tim
e and space that scales
logarithmically
with
the size of the graph. This exponential improvement in the ef
ficiency of the verification procedure serves
as the starting point for another celebrated result from com
plexity theory:
MIP
is exactly the same as the
class
NEXP
[
BFL91
], which are problems that admit
exponential-time checkable proofs
.
6
The class
NEXP
4
The specific numbers
90%
and
60%
are not too important; the only thing that really matters is t
hat the first one is strictly less
than
100%
and the second strictly larger than
50%
, as otherwise the problem becomes much easier.
5
For example, the graph can be specified via a circuit that take
s as input an edge index — using some arbitrary ordering — and
returns labels for the two endpoints of the edge.
6
An example of such a problem is the language S
UCCINCT
-3-C
OLORING
, which contains descriptions of polynomial-size
circuits
C
that specify a
3
-colorable graph
G
C
on
exponentially many
vertices.
7
contains
PSPACE
, but is believed to be much larger; this suggests that the abi
lity to interrogate more than
one prover enables a polynomial-time verifier to verify much
more complex statements.
Nonlocal games.
In this paper we will only be concerned with multiprover inte
ractive proof systems
that consist of a single round of communication with two prov
ers: the verifier first sends its questions to
each of the provers, the provers respond with their answers,
and the verifier decides whether to accept or
reject. The class of problems that admit such interactive pr
oofs is denoted
MIP
(
2, 1
)
, and it is known that
MIP
=
MIP
(
2, 1
)
[
FL92
]. Such proof systems have a convenient reformulation using
the language of
nonlocal games
, that we now explain.
In a nonlocal game, we say that a verifier interacts with multi
ple non-communicating
players
(instead
of provers — there is no formal difference between the two ter
ms). An
n
-question,
k
-answer nonlocal
game
G
is specified by two procedures: a
question sampling
procedure that samples a pair of questions
(
x
,
y
)
∈ {
1, . . . ,
n
}
2
for the players according to a distribution
μ
(known to the verifier and the players), and
a
decision
procedure that takes as input the players’ questions and the
ir respective answers
a
,
b
∈ {
1, . . . ,
k
}
and evaluates a predicate
D
(
x
,
y
,
a
,
b
)
∈ {
0, 1
}
to determine the verifier’s acceptance or rejection. In
classical complexity theory, the main quantity associated
with a nonlocal game
G
is its
classical value
,
which is the maximum success probability that two cooperati
ng but non-communicating players have in the
game. Formally, the classical value is defined as
val
(
G
) =
sup
p
∈
C
c
(
n
,
k
)
∑
x
,
y
μ
(
x
,
y
)
∑
a
,
b
D
(
x
,
y
,
a
,
b
)
p
abxy
,
(5)
where the set
C
c
(
n
,
k
)
is the set of
classical correlations
, which are tuples
(
p
abxy
)
such that there exists a
set
Λ
with probability measure
ν
and for every
λ
∈
Λ
functions
A
λ
,
B
λ
:
{
1, 2, . . . ,
n
} → {
1, 2, . . . ,
k
}
such that
∀
x
,
y
∈ {
1, 2, . . . ,
n
}
,
∀
a
,
b
∈ {
1, 2, . . . ,
k
}
,
p
abxy
=
Pr
λ
∼
ν
(
A
λ
(
x
) =
a
∧
B
λ
(
y
) =
b
)
.
This definition captures the intuitive notion that a classic
al strategy for the players is specified by (i) a
distribution
ν
on
Λ
that represents some probabilistic information shared by t
he players that is independent
of the verifier’s questions, and (ii) two functions
A
λ
,
B
λ
that represent each players’ “local strategy” for
answering given their shared randomness
λ
and question
x
or
y
.
7
Note that due to the shared randomness
λ
, the set
C
c
(
n
,
k
)
is a (closed) convex subset of
[
0, 1
]
n
2
k
2
.
To make the connection with interactive proof systems, obse
rve that the assertion that
L
∈
MIP
(
2, 1
)
precisely amounts to the specification of an efficient mappin
g
8
from problem instances
z
to games
G
z
such
that whenever
z
∈
L
then
val
(
G
z
)
≥
2
3
, whereas if
z
/
∈
L
then
val
(
G
z
)
≤
1
3
. Thus the complexity
of the optimization problem (
5
) captures the complexity of the decision problem
L
. The aforementioned
characterization of
MIP
as the class
NEXP
by [
BFL91
] shows that in general this optimization problem is
very difficult: it is as hard as deciding any language in
NEXP
.
7
For the functional analyst we briefly note that if we define a te
nsor
L
=
∑
x
,
y
,
a
,
b
μ
(
x
,
y
)
D
(
x
,
y
,
a
,
b
)
e
xa
⊗
e
yb
∈
R
nk
⊗
R
nk
then
val
(
G
) =
k
L
k
ℓ
n
1
(
ℓ
∞
)
k
⊗
ǫ
ℓ
n
1
(
ℓ
∞
)
k
, with
⊗
ǫ
denoting the injective tensor norm of Banach spaces. (For mo
re connections between
interactive proofs, nonlocal games and tensor norms we refe
r to the survey [
PV16
].)
8
Here by “efficient” we mean that there should be a polynomial-
time Turing machine that on input
z
returns (i) a polynomial-size
randomized circuit that samples from
μ
, and (ii) a polynomial-size circuit that evaluates the pred
icate
D
.
8
1.2 Statement of result
We now introduce the main complexity class that is the focus o
f this paper:
MIP
∗
, the “entangled-prover”
analogue of the class
MIP
considered earlier. Informally the class
MIP
∗
, first introduced in [
CHTW04
],
contains all languages that can be decided by a classical pol
ynomial-time verifier interacting with multiple
quantum
provers sharing
entanglement
. We focus on the class
MIP
∗
(
2, 1
)
, which corresponds to the setting
of one-round protocols with two provers. Equivalently, a la
nguage
L
is in
MIP
∗
(
2, 1
)
if and only if there is an
efficient mapping from instances
z
∈ {
0, 1
}
∗
to nonlocal games
G
z
such that if
z
∈
L
, then
val
∗
(
G
z
)
≥
2/3
and otherwise
val
∗
(
G
z
)
≤
1/3
. Here, for an
n
-question,
k
-answer game
G
, we let
val
∗
(
G
)
denote its
entangled value
, which is defined as
val
∗
(
G
) =
sup
p
∈
C
qs
(
n
,
k
)
∑
x
,
y
μ
(
x
,
y
)
∑
a
,
b
D
(
x
,
y
,
a
,
b
)
p
abxy
,
(6)
where the set
C
qs
(
n
,
k
)
is the quantum spatial correlation set introduced in (
1
). In other words, the entangled
value is the supremum of the success probabilities achieved
by players that use quantum spatial strategies
(i.e., perform local measurements on a shared entangled sta
te). Note that (
6
) can be equivalently defined as
taking the supremum over the set
C
qa
(
n
,
k
)
, the closure of
C
qs
(
n
,
k
)
.
Since
C
c
(
n
,
k
)
⊆
C
qs
(
n
,
k
)
, we have that
val
(
G
)
≤
val
∗
(
G
)
; in other words, using quantum spatial
strategies can do at least as well as classical strategies in
a nonlocal game.
The consideration of quantum strategies and the set
C
qs
(
n
,
k
)
for the definition of
MIP
∗
is motivated by
a long line of works in the foundations of quantum mechanics a
round the topic of
Bell inequalities
, that are
linear functionals which separate the sets
C
c
(
n
,
k
)
and
C
qs
(
n
,
k
)
. The simplest such functional is the
CHSH
inequality
[
CHSH69
], that shows
C
c
(
2, 2
)
(
C
qs
(
2, 2
)
. The CHSH inequality can be reformulated as a
game
G
such that
val
∗
(
G
)
>
val
(
G
)
. This game is very simple: it is defined by setting
μ
(
x
,
y
) =
1
4
for
all
x
,
y
∈ {
0, 1
}
and
D
(
x
,
y
,
a
,
b
) =
1
if and only if
a
⊕
b
=
x
∧
y
. It can be shown that
val
(
G
) =
3
4
and
val
∗
(
G
) =
1
2
+
1
2
√
2
>
3
4
. The study of Bell inequalities is a large area of research no
t only in foundations,
where they are a tool to study the nonlocal properties of enta
nglement, but also in quantum cryptography,
where they form the basis for cryptographic protocols for e.
g. quantum key distribution [
Eke91
].
The introduction of entanglement in the setting of interact
ive proofs has interesting consequences for
complexity theory; indeed it is not
a priori
clear how the class
MIP
∗
compares to
MIP
. Take a language
L
∈
MIP
(
2, 1
)
, and let
z
be an instance. Then the associated game
G
z
is such that
val
(
G
z
)
≥
2
3
if
z
∈
L
,
and
val
(
G
z
)
≤
1
3
otherwise. The fact that in general
val
∗
(
G
z
)
≥
val
(
G
z
)
(and that as demonstrated by
the CHSH game inequality can be strict) cuts both ways. On the
one hand, the soundness property can be
affected, so that instances
z
/
∈
L
could have
val
∗
(
G
z
) =
1
, meaning that we would not be able to establish
that
L
∈
MIP
∗
. On the other hand, a language
L
∈
MIP
∗
(
2, 1
)
may not necessarily be in
MIP
, because for
z
∈
L
the fact that
val
∗
(
G
z
)
≥
2
3
does not automatically imply
val
(
G
z
)
>
1
3
(in other words, the game
G
z
may require the players to use a quantum strategy in order to w
in with probability greater than
1/3
). Just
as the complexity of the class
MIP
is characterized by the complexity of approximating the cla
ssical value
of nonlocal games (the optimization problem in (
5
)), the complexity of
MIP
∗
is intimately related to the
complexity of approximating the entangled value of games (t
he optimization problem in (
6
)).
In [
IV12
] the first non-trivial lower bound on
MIP
∗
was shown, establishing that
MIP
=
NEXP
⊆
MIP
∗
.
(Earlier results [
KKM
+
11
,
IKM09
] gave more limited hardness results, for approximating the
entangled
value up to inverse polynomial precision.) This was proved b
y arguing that for the specific games con-
structed by [
BFL91
] that show
NEXP
⊆
MIP
, the classical and entangled values are approximately the
same. In other words, the classical soundness and completen
ess properties of the proof system of [
BFL91
]
9
are maintained in the presence of shared entanglement betwe
en the provers. Following [
IV12
] a sequence of
works [
Vid16
,
Ji16
,
NV18b
,
Ji17
,
NV18a
,
FJVY19
] established progressively stronger lower bounds on the
complexity of approximating the entangled value of nonloca
l games, culminating in [
NW19
] which showed
that approximating the entangled value is at least as hard as
NEEXP
, the collection of languages decidable
in non-deterministic
doubly exponential
time. This proves that
NEEXP
⊆
MIP
∗
, and since it is known that
NEXP
(
NEEXP
it follows that
MIP
6
=
MIP
∗
.
In contrast to these increasingly strong lower bounds the on
ly upper bound known on
MIP
∗
is the trivial
inclusion
MIP
∗
⊆
RE
, the class of recursively enumerable languages, i.e. langu
ages
L
such that there
exists a Turing machine
M
such that
x
∈
L
if and only if
M
halts and accepts on input
x
. This inclusion
follows since the supremum in (
6
) can be approximated from below by performing an exhaustive
search in
increasing dimension and with increasing accuracy. We note
that, in addition to containing all decidable
languages, this class also contains undecidable problems s
uch as the Halting problem, which is to decide
whether a given Turing machine eventually halts.
Our main result is a proof of the reverse inclusion:
RE
⊆
MIP
∗
. Combined with the preceding observa-
tion it follows that
MIP
∗
=
RE
,
which is a full characterization of the power of entangled-p
rover interactive proofs. In particular for any
0
<
ε
<
1
, it is an undecidable problem to determine whether a given no
nlocal game has entangled value
1
or at most
1
−
ε
(promised that one is the case).
Proof summary.
The proof of the inclusion
RE
⊆
MIP
∗
is obtained by designing an entangled-prover
interactive proof for the Halting problem, which is complet
e for the class
RE
. Specifically, we design an
efficient transformation that maps any Turing machine
M
to a nonlocal game
G
M
such that, if
M
halts
(when run on an empty input tape) then there is a quantum strat
egy for the provers that succeeds with
probability
1
in
G
M
(i.e.
val
∗
(
G
M
) =
1
), whereas if
M
does not halt then no quantum strategy can
succeed with probability larger than
1
2
in the game (i.e.
val
∗
(
G
M
)
≤
1
2
).
A very rough sketch of this construction is as follows (we giv
e a detailed overview in Section
2
). Given
an infinite family of games
{
G
n
}
n
∈
N
, we say that the family is
uniformly generated
if there is a polynomial-
time Turing machine that on input
n
returns a description of the game
G
n
. Given a game
G
and
p
∈
[
0, 1
]
let
E
(
G
,
p
)
denote the minimum local dimension of an entangled state sha
red by the players in order for
them to succeed in
G
with probability at least
p
.
We proceed in two steps. First, we design a
compression
procedure for a specific class of nonlocal
games that we call
normal form
. Given as input a uniformly generated family
{
G
n
}
n
∈
N
of normal form
games, the compression procedure returns another uniforml
y generated family
{
G
′
n
}
n
∈
N
of normal form
games with the following properties: (i) for all
n
, if
val
∗
(
G
2
n
) =
1
then
val
∗
(
G
′
n
) =
1
, and (ii) for all
n
, if
val
∗
(
G
2
n
)
≤
1
2
then
val
∗
(
G
′
n
)
≤
1
2
and moreover
E
(
G
′
n
,
1
2
)
≥
max
n
E
G
2
n
,
1
2
, 2
2
Ω
(
n
)
o
.
The construction of this compression procedure is our main c
ontribution. Informally, it combines the
recursive compression technique developed in [
Ji17
,
FJVY19
] with the so-called “introspection” technique
of [
NW19
] that was used to prove
NEEXP
⊆
MIP
∗
. The introspection technique itself relies heavily on the
quantum low-degree test of [
NV18a
] to robustly self-test certain distributions that arise fr
om constructions
of
classical
probabilistically checkable proofs. The quantum low-degr
ee test and the introspection technique
allow us to avoid the shrinking gap limitation of the results
from [
FJVY19
].
10
In the second step, we use the compression procedure in an ite
rated fashion to construct an interactive
proof system for the Halting problem. Fix a Turing machine
M
and consider the following family of
nonlocal games
{
G
(
0
)
M
,
n
}
n
∈
N
: for all
n
∈
N
, if
M
halts in at most
n
steps (when run on an empty input
tape), then
val
∗
(
G
(
0
)
M
,
n
) =
1
, and otherwise
val
∗
(
G
(
0
)
M
,
n
)
≤
1
2
.
9
Constructing such a family of games is trivial; furthermore
, they can be made in the “normal form”
required by the compression procedure. However, consider a
pplying the compression procedure to obtain a
family of normal form games
{
G
(
1
)
M
,
n
}
n
∈
N
. Then for all
n
∈
N
, it holds that if
M
halts in at most
2
n
steps
then
val
∗
(
G
(
1
)
M
,
n
) =
1
, and otherwise
val
∗
(
G
(
1
)
M
,
n
)
≤
1
2
, and furthermore any strategy that achieves a value
of at least
1
2
requires an entangled state of dimension at least
2
2
Ω
(
n
)
.
Intuitively, one would expect that iterating this procedur
e and “taking the limit” gives a family of games
{
G
(
∞
)
M
,
n
}
n
∈
N
such that if
M
halts then
val
∗
(
G
(
∞
)
M
,
n
) =
1
for all
n
∈
N
, whereas if
M
does not halt then no
finite-dimensional strategy can succeed with probability l
arger than
1
2
in
G
(
∞
)
M
,
n
, for all
n
∈
N
; in particular
val
∗
(
G
(
∞
)
M
,
n
)
≤
1
2
. Formally, we do not take such a limit but instead define direc
tly the family of games
{
G
(
∞
)
M
,
n
}
n
∈
N
as a
fixed point
of the Turing machine that implements the compression proce
dure. The game
G
M
can then be taken as
G
(
∞
)
M
,1
. We describe this in more detail in Section
2
.
1.3 Consequences
Our result is motivated by a connection with Tsirelson’s pro
blem from quantum information theory, itself
related to Connes’ Embedding Conjecture in the theory of von
Neumann algebras [
Con76
]. In a celebrated
sequence of papers, Tsirelson [
Tsi93
] initiated the systematic study of quantum correlation set
s. Recall the
definition of the set of quantum spatial correlations
C
qs
(
n
,
k
) =
(
p
abxy
)
|
p
abxy
=
h
ψ
|
A
x
a
⊗
B
y
b
|
ψ
i
,
|
ψ
i ∈ H
A
⊗ H
B
,
∀
xy
,
{
A
x
a
}
a
,
{
B
y
b
}
b
POVM
,
(7)
where here
|
ψ
i
ranges over all unit norm vectors
|
ψ
i ∈ H
A
⊗ H
B
with
H
A
and
H
B
arbitrary (separable)
Hilbert spaces, and a POVM is defined as a collection of positi
ve semidefinite operators that sum to identity.
(From now on we use the Dirac ket notation
|
ψ
i
for states.) Recall the closure
C
qa
(
n
,
k
)
of
C
qs
(
n
,
k
)
.
Tsirelson observed that there is a natural alternative defin
ition to the quantum spatial correlation set,
called the
quantum commuting correlation set
and defined as
C
qc
(
n
,
k
) =
(
p
abxy
)
|
p
abxy
=
h
ψ
|
A
x
a
B
y
b
|
ψ
i
,
(8)
where
|
ψ
i ∈ H
is a quantum state,
{
A
x
a
}
and
{
B
y
b
}
are POVMs for all
x
,
y
, and
[
A
x
a
,
B
y
b
] =
0
for all
a
,
b
,
x
,
y
. Note the key difference with spatial correlations is that i
n (
8
) all operators act on the same (separa-
ble) Hilbert space. The requirement that operators associa
ted with different inputs (questions)
x
,
y
commute
is arguably a minimal requirement within the context of quan
tum mechanics for there to not exist any causal
connection between outputs (answers)
a
,
b
obtained in response to the respective input.
The set
C
qc
(
n
,
k
)
is closed and convex, and it is easy to see that
C
qa
(
n
,
k
)
⊆
C
qc
(
n
,
k
)
for all
n
,
k
≥
1
.
When Tsirelson initially introduced these sets he claimed t
hat equality holds. However, it was later pointed
out that this is not obviously true. The question of equality
between
C
qc
and
C
qa
(for all
n
,
k
) is now known
as
Tsirelson’s problem
[
Tsi06
]. Let
C
q
(
n
,
k
)
denote the same as
C
qs
(
n
,
k
)
except that both
H
A
and
H
B
9
There is nothing special about the choice of
1
2
; this can be set to any constant that is less than
1
.
11
in (
7
) are restricted to finite-dimensional spaces. Then more gen
erally one can consider the following chain
of inclusions
C
q
(
n
,
k
)
⊆
C
qs
(
n
,
k
)
⊆
C
qa
(
n
,
k
)
⊆
C
qc
(
n
,
k
)
,
(9)
for all
n
,
k
∈
N
, and ask which (if any) of these inclusions are strict. We let
C
q
,
C
qs
,
C
qa
,
C
qc
denote the
union of
C
q
(
n
,
k
)
,
C
qs
(
n
,
k
)
,
C
qa
(
n
,
k
)
,
C
qc
(
n
,
k
)
, respectively, over all integers
n
,
k
∈
N
. In a breakthrough
work, Slofstra established the first separation between the
se four correlation sets by proving that
C
qs
6
=
C
qc
[
Slo19b
]; he later proved the stronger statement that
C
qs
6
=
C
qa
[
Slo19a
]. As a consequence of the
technique used to demonstrate the separation Slofstra also
obtains the complexity-theoretic statement that
the problem of determining whether an element
p
lies in
C
qc
, even promised that if it does, then it also lies in
C
qa
, is undecidable. Interestingly, this is shown by reduction
from the
complement
of the halting problem;
for our result we reduce from the halting problem (see Sectio
n
1.4
for further discussion of this point).
Since his work, simpler proofs of Slofstra’s results have be
en found [
DPP19
,
MR18
,
Col19
]. In [
CS18
],
Coladangelo and Stark showed that
C
q
6
=
C
qs
by exhibiting a
5
-input,
3
-output correlation that can be
attained using infinite-dimensional spatial strategies (i
.e. infinite-dimensional Hilbert spaces, a state and
POVMs satisfying (
7
)) but cannot be attained via finite-dimensional strategies
.
As already noted in [
FNT14
] (and further elaborated on by [
FJVY19
]), the undecidability of
MIP
∗
(
2, 1
)
implies the separation
C
qa
6
=
C
qc
.
10
This follows from the observation that if
C
qa
=
C
qc
, then there exists
an algorithm that can correctly determine if a nonlocal game
G
satisfies
val
∗
(
G
) =
1
or
val
∗
(
G
)
≤
1
2
and
always halts: this algorithm interleaves a hierarchy of sem
idefinite programs providing outer approximations
to the set
C
qc
[
NPA08
,
DLTW08
] with a simple exhaustive search procedure providing inner
approximations
to
C
q
. Our result that
RE
⊆
MIP
∗
(
2, 1
)
implies that no such algorithm exists, thus resolving Tsire
lson’s
problem in the negative.
We furthermore exhibit an explicit nonlocal game
G
such that
val
∗
(
G
)
<
val
co
(
G
) =
1
, where
val
co
(
G
)
is defined as
val
∗
(
G
)
except that the supremum is taken over the set
C
qc
(
n
,
k
)
in (
8
). This in
turn yields an explicit correlation that is in the set
C
qc
but not in
C
qa
. This game closely resembles the game
G
M
described in the sketch of the proof that
RE
⊆
MIP
∗
, where
M
is the Turing machine that runs the
hierarchy of semidefinite programs on the game
G
M
and halts if it certifies that
val
co
(
G
M
)
<
1
. It is in
principle possible to determine an upper bound on the parame
ters
n
,
k
for our separating correlation from the
proof. While we do not provide such a bound, there is no step in
the proof that requires it to be astronomical;
e.g. we believe (without proof) that
10
20
is a clear upper bound.
Connes’ Embedding Conjecture.
Connes’ Embedding Conjecture (CEC) [
Con76
] is a conjecture in the
theory of von Neumann algebras. Briefly, CEC posits that ever
y type II
1
von Neumann factor embeds into an
ultrapower of the hyperfinite II
1
factor. We refer to [
Oza13
] for a precise formulation of the conjecture and
connections to other conjectures in operator algebras, suc
h as Kirchberg’s QWEP conjecture. In independent
work Fritz [
Fri12
] and Junge et al. [
JNP
+
11
] showed that a positive answer to CEC would imply a positive
resolution of Tsirelson’s problem, i.e. that
C
qa
(
n
,
k
) =
C
qc
(
n
,
k
)
for all
n
,
k
. (This was later promoted to an
equivalence by Ozawa [
Oza13
].) Since our result disproves this equality for some
n
,
k
it also implies that
CEC does not hold. We note that using the constructive aspect
of our result it may be possible to give an
explicit description of a factor that does not embed into an u
ltrapower of the hyperfinite II
1
factor, but we
do not give such a construction.
10
Technically [
FNT14
] make the observation for the commuting-prover analogue
MIP
co
(
2, 1
)
, discussed further in Section
1.4
,
but the reasoning is the same.
12