IPS upper bound for subset sum axiom I am reading the following paper  


Michael A. Forbes, Amir Shpilka, Iddo Tzameret, Avi Wigderson ,"Proof Complexity Lower Bounds from Algebraic Circuit Complexity", 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
  
  
  $C(x, 0, 0) = 0$.
  $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.