# IPS upper bound for subset sum axiom

I am reading the following paper

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?

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.