<p>First, Kaveh is correct that the verification for IPS is randomized, so all it would show is $\mathsf{NP} \subseteq \mathsf{coAM}$ (not $\mathsf{NP} = \mathsf{coNP}$). However, this alone would still be enough to collapse the polynomial hierarchy.</p>

<p>Second, I think the actual thing you are missing here is that the IPS proofs they give have size polynomial in the size of $|A| = |\{\sum_i \alpha_i x_i : \vec{x} \in \{0,1\}^n\}|$, which can be exponential in $n$, in general. </p>

CC BY-SA 3.0
2018-01-02T06:57:59.967Z
2018-01-02T06:57:59.967Z
Joshua Grochow
<p>I think what you are missing is probably the complexity of the proof verification algorithm for IPS.</p>

<p>It is generally true that if we have a Cook-Reckhow proof system and have short proofs for a coNP-complete problem (e.g. TAUT) then that would imply NP=coNP. But not every proof system is a Cook-Reckhow proof system, e.g. it can be the case that the proofs could be verified in <em>deterministic</em> polynomial-time.</p>

<p>If the IPS proof system was a Cook-Reckhow proof system then the existence of polynomial-size proofs for the complement of subset-sum would imply an NP-algorithm for a coNP-complete problem. But it is not clear if IPS has a deterministic polynomial-time verification algorithm.</p>

CC BY-SA 3.0
2018-01-02T01:08:30.233Z
2018-01-02T01:57:18.577Z
2018-01-02T01:57:18.577Z
Kaveh
<p>I am reading the following paper  </p>

<ul>
<li>Michael A. Forbes, Amir Shpilka, Iddo Tzameret, Avi Wigderson ,"<a href="https://arxiv.org/abs/1606.05050" rel="nofollow noreferrer">Proof Complexity Lower Bounds from Algebraic Circuit Complexity</a>", 2016.</li>
</ul>

<p>IPS is defined as follows:</p>

<blockquote>
  <p>(Ideal Proof System (IPS), Grochow-Pitassi [GP14]). Let $f_1(x), \ldots , f_m(x) ∈ F[x_1, \ldots , x_n]$ be a system of polynomials. An IPS refutation for showing that the polynomials $\{f_j\}_j$ have no common solution in $\{0, 1\}^n$ is an algebraic circuit $C(x, y, z) ∈ F[x, y_1, \ldots , y_m, z_1, \ldots , z_n]$
  such that</p>
  
  <ol>
  <li>$C(x, 0, 0) = 0$.</li>
  <li>$C(x, f_1(x), \ldots , f_m(x), x^2_1 − x_1, . . . , x^2_n − x_n) = 1$.</li>
  </ol>
</blockquote>

<p>Then:</p>

<blockquote>
  <p>We then consider the subset-sum axioms, previously considered by Impagliazzo, Pudlak, and Sgall [IPS99], and show that they can be refuted in polynomial size by the C-IPS_LIN proof
  system where C is either the class of roABPs, or the class of multilinear formulas.</p>
</blockquote>

<p>The subset-sum axiom is defined as follows:</p>

<blockquote>
  <p>That is, we give such refutations for whenever the polynomial $\sum
_i α_ix_i − β$ is unsatisfiable over the boolean cube $\{0, 1\}^n$, where the size of the refutation is polynomial in the size of the set $A := \{\sum_i α_ix_i : x ∈\{0, 1\}^n\}$. </p>
</blockquote>

<hr>

<p>They have given a polynomial size refutation for the subset-sum axiom. Polynomial-size proofs for the complement of subset-sum should imply
NP=coNP, doesn't it? What am I missing?</p>

<algebraic-complexity><proof-complexity>
IPS upper bound for subset sum axiom
Chetan Gupta
# IPS upper bound for subset sum axiom

(Asked by: username_0 on 2017-12-31)

I am reading the following paper

* Michael A. Forbes, Amir Shpilka, Iddo Tzameret, Avi Wigderson ,"[Proof Complexity Lower Bounds from Algebraic Circuit Complexity](https://arxiv.org/abs/1606.05050)", 2016.

IPS is defined as follows:

> (Ideal Proof System (IPS), Grochow-Pitassi [GP14]). Let $f\_1(x), \ldots , f\_m(x) ∈ F[x\_1, \ldots , x\_n]$ be a system of polynomials. An IPS refutation for showing that the polynomials $\{f\_j\}\_j$ have no common solution in $\{0, 1\}^n$ is an algebraic circuit $C(x, y, z) ∈ F[x, y\_1, \ldots , y\_m, z\_1, \ldots , z\_n]$
> such that
>
> 1. $C(x, 0, 0) = 0$.
> 2. $C(x, f\_1(x), \ldots , f\_m(x), x^2\_1 − x\_1, . . . , x^2\_n − x\_n) = 1$.

Then:

> We then consider the subset-sum axioms, previously considered by Impagliazzo, Pudlak, and Sgall [IPS99], and show that they can be refuted in polynomial size by the C-IPS\_LIN proof
> system where C is either the class of roABPs, or the class of multilinear formulas.

The subset-sum axiom is defined as follows:

> That is, we give such refutations for whenever the polynomial $\sum
> \_i α\_ix\_i − β$ is unsatisfiable over the boolean cube $\{0, 1\}^n$, where the size of the refutation is polynomial in the size of the set $A := \{\sum\_i α\_ix\_i : x ∈\{0, 1\}^n\}$.

---

They have given a polynomial size refutation for the subset-sum axiom. Polynomial-size proofs for the complement of subset-sum should imply
NP=coNP, doesn't it? What am I missing?

**Tags:** algebraic-complexity, proof-complexity

---

## 2 answers

### Answer by username_1 on 2018-01-02. Score: 3

First, Kaveh is correct that the verification for IPS is randomized, so all it would show is $\mathsf{NP} \subseteq \mathsf{coAM}$ (not $\mathsf{NP} = \mathsf{coNP}$). However, this alone would still be enough to collapse the polynomial hierarchy.

Second, I think the actual thing you are missing here is that the IPS proofs they give have size polynomial in the size of $|A| = |\{\sum\_i \alpha\_i x\_i : \vec{x} \in \{0,1\}^n\}|$, which can be exponential in $n$, in general.


---

### Answer by username_2 on 2018-01-02. Score: 2

I think what you are missing is probably the complexity of the proof verification algorithm for IPS.

It is generally true that if we have a Cook-Reckhow proof system and have short proofs for a coNP-complete problem (e.g. TAUT) then that would imply NP=coNP. But not every proof system is a Cook-Reckhow proof system, e.g. it can be the case that the proofs could be verified in *deterministic* polynomial-time.

If the IPS proof system was a Cook-Reckhow proof system then the existence of polynomial-size proofs for the complement of subset-sum would imply an NP-algorithm for a coNP-complete problem. But it is not clear if IPS has a deterministic polynomial-time verification algorithm.


---

