TY - GEN
T1 - Semi-algebraic proofs, IPS lower bounds, and the τ-conjecture
T2 - 52nd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2020
AU - Alekseev, Yaroslav
AU - Grigoriev, Dima
AU - Hirsch, Edward A.
AU - Tzameret, Iddo
N1 - Publisher Copyright:
© 2020 ACM.
PY - 2020/6/8
Y1 - 2020/6/8
N2 - We introduce the binary value principle which is a simple subset-sum instance expressing that a natural number written in binary cannot be negative, relating it to central problems in proof and algebraic complexity. We prove conditional superpolynomial lower bounds on the Ideal Proof System (IPS) refutation size of this instance, based on a well-known hypothesis by Shub and Smale about the hardness of computing factorials, where IPS is the strong algebraic proof system introduced by Grochow and Pitassi (2018). Conversely, we show that short IPS refutations of this instance bridge the gap between sufficiently strong algebraic and semi-algebraic proof systems. Our results extend to full-fledged IPS the paradigm introduced in Forbes et al. (2016), whereby lower bounds against subsystems of IPS were obtained using restricted algebraic circuit lower bounds, and demonstrate that the binary value principle captures the advantage of semi-algebraic over algebraic reasoning, for sufficiently strong systems. Specifically, we show the following: Conditional IPS lower bounds: The Shub-Smale hypothesis (1995) implies a superpolynomial lower bound on the size of IPS refutations of the binary value principle over the rationals defined as the unsatisfiable linear equation g'i=1n 2i-1xi = -1, for boolean xi's. Further, the related τ-conjecture (1995) implies a superpolynomial lower bound on the size of IPS refutations of a variant of the binary value principle over the ring of rational functions. No prior conditional lower bounds were known for IPS or for apparently much weaker propositional proof systems such as Frege. Algebraic vs. semi-algebraic proofs: Admitting short refutations of the binary value principle is necessary for any algebraic proof system to fully simulate any known semi-algebraic proof system, and for strong enough algebraic proof systems it is also sufficient. In particular, we introduce a very strong proof system that simulates all known semi-algebraic proof systems (and most other known concrete propositional proof systems), under the name Cone Proof System (CPS), as a semi-algebraic analogue of the ideal proof system: CPS establishes the unsatisfiability of collections of polynomial equalities and inequalities over the reals, by representing sum-of-squares proofs (and extensions) as algebraic circuits. We prove that IPS is polynomially equivalent to CPS iff IPS admits polynomial-size refutations of the binary value principle (for the language of systems of equations that have no 0/1-solutions), over both g.,Currency sign and g.,.
AB - We introduce the binary value principle which is a simple subset-sum instance expressing that a natural number written in binary cannot be negative, relating it to central problems in proof and algebraic complexity. We prove conditional superpolynomial lower bounds on the Ideal Proof System (IPS) refutation size of this instance, based on a well-known hypothesis by Shub and Smale about the hardness of computing factorials, where IPS is the strong algebraic proof system introduced by Grochow and Pitassi (2018). Conversely, we show that short IPS refutations of this instance bridge the gap between sufficiently strong algebraic and semi-algebraic proof systems. Our results extend to full-fledged IPS the paradigm introduced in Forbes et al. (2016), whereby lower bounds against subsystems of IPS were obtained using restricted algebraic circuit lower bounds, and demonstrate that the binary value principle captures the advantage of semi-algebraic over algebraic reasoning, for sufficiently strong systems. Specifically, we show the following: Conditional IPS lower bounds: The Shub-Smale hypothesis (1995) implies a superpolynomial lower bound on the size of IPS refutations of the binary value principle over the rationals defined as the unsatisfiable linear equation g'i=1n 2i-1xi = -1, for boolean xi's. Further, the related τ-conjecture (1995) implies a superpolynomial lower bound on the size of IPS refutations of a variant of the binary value principle over the ring of rational functions. No prior conditional lower bounds were known for IPS or for apparently much weaker propositional proof systems such as Frege. Algebraic vs. semi-algebraic proofs: Admitting short refutations of the binary value principle is necessary for any algebraic proof system to fully simulate any known semi-algebraic proof system, and for strong enough algebraic proof systems it is also sufficient. In particular, we introduce a very strong proof system that simulates all known semi-algebraic proof systems (and most other known concrete propositional proof systems), under the name Cone Proof System (CPS), as a semi-algebraic analogue of the ideal proof system: CPS establishes the unsatisfiability of collections of polynomial equalities and inequalities over the reals, by representing sum-of-squares proofs (and extensions) as algebraic circuits. We prove that IPS is polynomially equivalent to CPS iff IPS admits polynomial-size refutations of the binary value principle (for the language of systems of equations that have no 0/1-solutions), over both g.,Currency sign and g.,.
KW - Algebraic complexity
KW - Algebraic proofs
KW - Proof complexity
KW - Semi-algebraic proofs
KW - Sum-of-squares proofs
KW - Tau-conjecture
UR - http://www.scopus.com/inward/record.url?scp=85086760049&partnerID=8YFLogxK
U2 - 10.1145/3357713.3384245
DO - 10.1145/3357713.3384245
M3 - ???researchoutput.researchoutputtypes.contributiontobookanthology.conference???
AN - SCOPUS:85086760049
T3 - Proceedings of the Annual ACM Symposium on Theory of Computing
SP - 54
EP - 67
BT - STOC 2020 - Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing
A2 - Makarychev, Konstantin
A2 - Makarychev, Yury
A2 - Tulsiani, Madhur
A2 - Kamath, Gautam
A2 - Chuzhoy, Julia
Y2 - 22 June 2020 through 26 June 2020
ER -