arXiv subjects

Iddo Tzameret

Publications and source records attributed to Iddo Tzameret.

At least 19 recordsLinked to original sources

arXiv2026

The Weak Rank Principle: Lower Bounds and Applications

Given two symbolic matrices $X$ and $Y$ of dimensions $m\times n$ and $n\times m$, the *weak rank principle* (WRank) states the equation $XY = A$ is unsatisfiable when $m>n$ and rank of $A$ exceeds $n$. We study this principle as an algebraic generalisation of the weak pigeonhole principle (WPHP). As a strengthening of WPHP, it admits proof complexity lower bounds in settings where none are known for WPHP, while still supporting analogous applications. *Generators for PCR$_{F_2}$*: We prove exponential size lower bounds for algebraic, perfect matching, and bamboo-tree encodings of WRank in PCR$_{F_2}$. The latter encoding is the most relevant for applications to circuit lower-bound formulas, as considered by Alekhnovich, Ben-Sasson, Razborov, and Wigderson (SIAM J. Comput., 2004) and Razborov (Ann. Math., 2015). Using a standard iteration technique we amplify the stretch to exponential. This resolves the open problem concerning the construction of proof complexity generators with good stretch for PCR$_{F_2}$. *Generators for Sherali--Adams:* We develop a new size lower-bound technique showing that WRank, encoded as a bamboo-tree CNF, serves as a proof complexity generator for SA. Our method introduces a pseudoexpectation tailored specifically to the rank principle (and incompatible with WPHP). *Circuit lower bound formulas:* We show that PCR$_{F_2}$ does not admit short proofs of lower-bound statements against Boolean circuits, nor against weak models of algebraic circuits. This settles the open problem raised by Razborov (Ann. Math., 2015) concerning the provability of such lower bounds in PCR$_{F_2}$. *Strength of the weak rank principle:* Finally, we show that WRank is *necessary* for proving NC$^2$ circuit lower bounds and, for odd primes $p$, *sufficient* within the theory corresponding to AC$^{0}[p]$ for deriving AC$^{0}[p]$ lower bounds.

cs.CC↗

arXiv2026

Hard CNF Instances for Ideal Proof Systems

Since the introduction of the Ideal Proof System (IPS) by Grochow and Pitassi (J. ACM 2018), a substantial body of work has established size lower bounds for IPS and its fragments. In particular, Forbes, Shpilka, Tzameret, and Wigderson (Theory Comput. 2021) developed the main lower-bound frameworks for restricted IPS fragments, namely functional lower bounds and the hard multiples method, while Alekseev, Grigoriev, Hirsch, and Tzameret (SIAM J. Comput. 2024) gave a general template for conditional lower bounds for full IPS. Yet all these lower bounds apply only to purely algebraic formulas over a field, that is, non-Boolean formulas not directly expressible in propositional logic. Proving lower bounds for CNF formulas has therefore remained a central open problem in this line of work. The current work resolves this question for IPS over read-once oblivious algebraic branching programs (roABPs) by proving lower bounds for refutations of CNF formulas in this system. Our approach is a rank-based feasible interpolation argument, following the method of Pudlák and Sgall (Proof Complexity and Feasible Arithmetic 1996) for monotone span programs, in which decomposing a given roABP refutation along a variable partition yields a low-dimensional space of polynomials from which we construct a span-program interpolant. We extend their result from Nullstellensatz refutations measured by degree to Nullstellensatz refutations measured by roABP size (i.e., roABP-IPS$_\text{LIN}$).

cs.CC↗

arXiv2025

AC^0[p]-Frege Cannot Efficiently Prove that Constant-Depth Algebraic Circuit Lower Bounds are Hard

We study whether lower bounds against constant-depth algebraic circuits computing the Permanent over finite fields (Limaye-Srinivasan-Tavenas, J. ACM 2025; Forbes, CCC 2024) are hard to prove in certain proof systems. We focus on a DNF formula that expresses that such lower bounds are hard for constant-depth algebraic proofs. Using an adaptation of the diagonalization framework of Santhanam and Tzameret (SIAM J. Comput. 2025), we show unconditionally that this family of DNF formulas does not admit polynomial-size propositional AC0[p]-Frege proofs infinitely often. This rules out the possibility that the DNF family is easy, and establishes that its status is either that of a hard tautology for AC0[p]-Frege or else unprovable (not a tautology). While it remains open whether the DNFs in question are tautologies, we provide evidence in this direction. In particular, under the plausible assumption that certain weak properties of multilinear algebra, specifically those involving tensor rank, do not admit short constant-depth algebraic proofs, the DNFs are tautologies. We also observe that several weaker variants of the DNF formula are provably tautologies, and we show that the question of whether the DNFs are tautologies connects to conjectures of Razborov (ICALP 1996) and Krajicek (J. Symb. Log. 2004). Our result has two additional features. (i) Existential depth amplification: the DNF formula is parameterised by a constant depth d bounding the depth of the algebraic proofs. We show that there exists some fixed depth d such that if there are no small depth-d algebraic proofs of certain circuit lower bounds for the Permanent, then there are no such small algebraic proofs in any constant depth. (ii) Necessity: we show that our result is a necessary step towards establishing lower bounds against constant-depth algebraic proofs, and more generally against any sufficiently strong proof system.

cs.CC↗

arXiv2025

Lower Bounds against the Ideal Proof System in Finite Fields

Lower bounds against strong algebraic proof systems and specifically fragments of the Ideal Proof System (IPS), have been obtained in an ongoing line of work. All of these bounds, however, are proved only over large (or characteristic $0$) fields, yet finite fields are the more natural setting for propositional proof complexity, especially for progress toward lower bounds for Frege systems such as $AC^0[p]$-Frege. This work establishes lower bounds against fragments of IPS over fixed finite fields. Specifically, we show that a variant of the knapsack instance studied by Govindasamy, Hakoniemi, and Tzameret (FOCS'22) has no polynomial-size IPS refutation over finite fields when the refutation is multilinear and written as a constant-depth circuit. The key ingredient of our argument is the recent set-multilinearization result of Forbes (CCC'24), which extends the earlier result of Limaye, Srinivasan, and Tavenas (FOCS'21) to all fields, and an extension of the techniques of Govindasamy, Hakoniemi, and Tzameret to finite fields. We also separate this proof system from the one studied by Govindasamy, Hakoniemi, and Tzameret. In addition, we present new lower bounds for read-once algebraic branching program refutations, roABP-IPS, in finite fields, extending results of Forbes, Shpilka, Tzameret, and Wigderson (Theor. of Comput.'21) and Hakoniemi, Limaye, and Tzameret (STOC'24). Finally, we show that any lower bound against any proof system at least as strong as (non-multilinear) constant-depth IPS over finite fields for any instance, even a purely algebraic instance (i.e., not a translation of a Boolean formula or CNF), implies a hard CNF formula for the respective IPS fragment, and hence an $AC^0[p]$-Frege lower bound by known simulations over finite fields (Grochow and Pitassi (J. ACM'18)).

cs.CC↗

arXiv2024

Functional Lower Bounds in Algebraic Proofs: Symmetry, Lifting, and Barriers

Strong algebraic proof systems such as IPS (Ideal Proof System; Grochow-Pitassi [GP18]) offer a general model for deriving polynomials in an ideal and refuting unsatisfiable propositional formulas, subsuming most standard propositional proof systems. A major approach for lower bounding the size of IPS refutations is the Functional Lower Bound Method (Forbes, Shpilka, Tzameret and Wigderson [FSTW21]), which reduces the hardness of refuting a polynomial equation f(x) = 0 with no Boolean solutions to the hardness of computing the function 1/f(x) over the Boolean cube with an algebraic circuit. Using symmetry, we provide a general way to obtain many new hard instances against fragments of IPS via the functional lower bound method. This includes hardness over finite fields and hard instances different from Subset Sum variants, both of which were unknown before, and stronger constant-depth lower bounds. Conversely, we expose the limitation of this method by showing it cannot lead to proof complexity lower bounds for any hard Boolean instance (e.g., CNFs) for any sufficiently strong proof systems.

cs.CC↗

arXiv2024

Feasibly Constructive Proof of Schwartz-Zippel Lemma and the Complexity of Finding Hitting Sets

The Schwartz-Zippel Lemma states that if a low-degree multivariate polynomial with coefficients in a field is not zero everywhere in the field, then it has few roots on every finite subcube of the field. This fundamental fact about multivariate polynomials has found many applications in algorithms, complexity theory, coding theory, and combinatorics. We give a new proof of the lemma that offers some advantages over the standard proof. First, the new proof is more constructive than previously known proofs. For every given side-length of the cube, the proof constructs a polynomial-time computable and polynomial-time invertible surjection onto the set of roots in the cube. The domain of the surjection is tight, thus showing that the set of roots on the cube can be compressed. Second, the new proof can be formalised in Buss' bounded arithmetic theory $\mathrm{S}^1_2$ for polynomial-time reasoning. One consequence of this is that the theory $\mathrm{S}^1_2 + \mathrm{dWPHP(PV)}$ for approximate counting can prove that the problem of verifying polynomial identities (PIT) can be solved by polynomial-size circuits. The same theory can also prove the existence of small hitting sets for any explicitly described class of polynomials of polynomial degree. To complete the picture we show that the existence of such hitting sets is \emph{equivalent} to the surjective weak pigeonhole principle $\mathrm{dWPHP(PV)}$, over the theory $\mathrm{S}^1_2$. This is a contribution to a line of research studying the reverse mathematics of computational complexity. One consequence of this is that the problem of constructing small hitting sets for such classes is complete for the class APEPP of explicit construction problems whose totality follows from the probabilistic method. This class is also known and studied as the class of Range Avoidance Problems.

cs.CC↗

arXiv2023

Stretching Demi-Bits and Nondeterministic-Secure Pseudorandomness

We develop the theory of cryptographic nondeterministic-secure pseudorandomness beyond the point reached by Rudich's original work (Rudich 1997), and apply it to draw new consequences in average-case complexity and proof complexity. Specifically, we show the following: *Demi-bit stretch*: Super-bits and demi-bits are variants of cryptographic pseudorandom generators which are secure against nondeterministic statistical tests (Rudich 1997). They were introduced to rule out certain approaches to proving strong complexity lower bounds beyond the limitations set out by the Natural Proofs barrier (Rudich and Razborov 1997). Whether demi-bits are stretchable at all had been an open problem since their introduction. We answer this question affirmatively by showing that: every demi-bit $b:\{0,1\}^n\to \{0,1\}^{n+1}$ can be stretched into sublinear many demi-bits $b':\{0,1\}^{n}\to \{0,1\}^{n+n^{c}}$, for every constant $0 >> see rest of abstract in paper.

cs.CC↗

arXiv2022

Simple Hard Instances for Low-Depth Algebraic Proofs

We prove super-polynomial lower bounds on the size of propositional proof systems operating with constant-depth algebraic circuits over fields of zero characteristic. Specifically, we show that the subset-sum variant $\sum_{i,j,k,\ell\in[n]} z_{ijk\ell}x_ix_j x_k x_\ell - β=0$, for Boolean variables, does not have polynomial-size IPS refutations where the refutations are multilinear and written as constant-depth circuits. Andrews and Forbes (STOC'22) established recently a constant-depth IPS lower bound, but their hard instance does not have itself small constant-depth circuits, while our instance is computable already with small depth-2 circuits. Our argument relies on extending the recent breakthrough lower bounds against constant-depth algebraic circuits by Limaye, Srinivasan and Tavenas (FOCS'21) to the functional lower bound framework of Forbes, Shpilka, Tzameret and Wigderson (ToC'21), and may be of independent interest. Specifically, we construct a polynomial $f$ computable with small-size constant-depth circuits, such that the multilinear polynomial computing $1/f$ over Boolean values and its appropriate set-multilinear projection are hard for constant-depth circuits.

cs.CC↗

arXiv2021

First-Order Reasoning and Efficient Semi-Algebraic Proofs

Semi-algebraic proof systems such as sum-of-squares (SoS) have attracted a lot of attention recently due to their relation to approximation algorithms: constant degree semi-algebraic proofs lead to conjecturally optimal polynomial-time approximation algorithms for important NP-hard optimization problems. Motivated by the need to allow a more streamlined and uniform framework for working with SoS proofs than the restrictive propositional level, we initiate a systematic first-order logical investigation into the kinds of reasoning possible in algebraic and semi-algebraic proof systems. Specifically, we develop first-order theories that capture in a precise manner constant degree algebraic and semi-algebraic proof systems: every statement of a certain form that is provable in our theories translates into a family of constant degree polynomial calculus or SoS refutations, respectively; and using a reflection principle, the converse also holds. This places algebraic and semi-algebraic proof systems in the established framework of bounded arithmetic, while providing theories corresponding to systems that vary quite substantially from the usual propositional-logic ones. We give examples of how our semi-algebraic theory proves statements such as the pigeonhole principle, we provide a separation between algebraic and semi-algebraic theories, and we describe initial attempts to go beyond these theories by introducing extensions that use the inequality symbol, identifying along the way which extensions lead outside the scope of constant degree SoS. Moreover, we prove new results for propositional proofs, and specifically extend Berkholz's dynamic-by-static simulation of polynomial calculus (PC) by SoS to PC with the radical rule.

cs.LO↗

arXiv2019

Resolution with Counting: Dag-Like Lower Bounds and Different Moduli

Resolution over linear equations is a natural extension of the popular resolution refutation system, augmented with the ability to carry out basic counting. Denoted Res(lin_R), this refutation system operates with disjunctions of linear equations with boolean variables over a ring R, to refute unsatisfiable sets of such disjunctions. Beginning in the work of [RT08], through the work of [IS14] which focused on tree-like lower bounds, this refutation system was shown to be fairly strong. Subsequent work (cf.[Kra17, IS14, KO18, GK18]) made it evident that establishing lower bounds against general Res(lin_R) refutations is a challenging and interesting task since the system captures a 'minimal' extension of resolution with counting gates for which no super-polynomial lower bounds are known to date. We provide the first super-polynomial size lower bounds on general (dag-like) resolution over linear equations refutations in the large characteristic regime. In particular we prove that the subset-sum principle 1+x1+...+2^n xn=0 requires refutations of exponential size over Q. Our proof technique is nontrivial and novel: roughly speaking, we show that under certain conditions every refutation of a subset-sum instance f=0 must pass through a fat clause containing an equation f=alpha for each alpha in the image of f under boolean assignments. We develop a somewhat different approach to prove exponential lower bounds against tree-like refutations of any subset-sum instance that depends on n variables, hence also separating tree-like from dag-like refutations over the rationals. (Abstract continued in the full paper.)

cs.CC↗

arXiv2019

Semi-Algebraic Proofs, IPS Lower Bounds and the $τ$-Conjecture: Can a Natural Number be Negative?

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: (abstract continues in document.)

cs.CC↗

arXiv2018

Uniform, Integral and Feasible Proofs for the Determinant Identities

Aiming to provide weak as possible axiomatic assumptions in which one can develop basic linear algebra, we give a uniform and integral version of the short propositional proofs for the determinant identities demonstrated over $GF(2)$ in Hrubes-Tzameret [SICOMP'15]. Specifically, we show that the multiplicativity of the determinant function and the Cayley-Hamilton theorem over the integers are provable in the bounded arithmetic theory $\mathbf{VNC}^2$; the latter is a first-order theory corresponding to the complexity class $\mathbf{NC}^2$ consisting of problems solvable by uniform families of polynomial-size circuits and $O(\log ^2 n)$-depth. This also establishes the existence of uniform polynomial-size $\mathbf{NC}^2$-Frege proofs of the basic determinant identities over the integers (previous propositional proofs hold only over the two element field).

cs.CC↗

arXiv2016

Algebraic Proof Complexity: Progress, Frontiers and Challenges

We survey recent progress in the proof complexity of strong proof systems and its connection to algebraic circuit complexity, showing how the synergy between the two gives rise to new approaches to fundamental open questions, solutions to old problems, and new directions of research. In particular, we focus on tight connections between proof complexity lower bounds (namely, lower bounds on the size of proofs of certain tautologies), algebraic circuit lower bounds, and the Polynomial Identity Testing problem from derandomization theory.

cs.CC↗

arXiv2016

Proof Complexity Lower Bounds from Algebraic Circuit Complexity

We give upper and lower bounds on the power of subsystems of the Ideal Proof System (IPS), the algebraic proof system recently proposed by Grochow and Pitassi, where the circuits comprising the proof come from various restricted algebraic circuit classes. This mimics an established research direction in the boolean setting for subsystems of Extended Frege proofs, where proof-lines are circuits from restricted boolean circuit classes. Except one, all of the subsystems considered in this paper can simulate the well-studied Nullstellensatz proof system, and prior to this work there were no known lower bounds when measuring proof size by the algebraic complexity of the polynomials (except with respect to degree, or to sparsity). We give two general methods of converting certain algebraic lower bounds into proof complexity ones. Our methods require stronger notions of lower bounds, which lower bound a polynomial as well as an entire family of polynomials it defines. Our techniques are reminiscent of existing methods for converting boolean circuit lower bounds into related proof complexity results, such as feasible interpolation. We obtain the relevant types of lower bounds for a variety of classes (sparse polynomials, depth-3 powering formulas, read-once oblivious algebraic branching programs, and multilinear formulas), and infer the relevant proof complexity results. We complement our lower bounds by giving short refutations of the previously-studied subset-sum axiom using IPS subsystems, allowing us to conclude strict separations between some of these subsystems.

cs.CC↗

arXiv2015

Characterizing Propositional Proofs as Non-Commutative Formulas

Does every Boolean tautology have a short propositional-calculus proof? Here, a propositional calculus (i.e. Frege) proof is a proof starting from a set of axioms and deriving new Boolean formulas using a set of fixed sound derivation rules. Establishing any super-polynomial size lower bound on Frege proofs (in terms of the size of the formula proved) is a major open problem in proof complexity, and among a handful of fundamental hardness questions in complexity theory by and large. Non-commutative arithmetic formulas, on the other hand, constitute a quite weak computational model, for which exponential-size lower bounds were shown already back in 1991 by Nisan [Nis91] who used a particularly transparent argument. In this work we show that Frege lower bounds in fact follow from corresponding size lower bounds on non-commutative formulas computing certain polynomials (and that such lower bounds on non-commutative formulas must exist, unless NP=coNP). More precisely, we demonstrate a natural association between tautologies $T$ to non-commutative polynomials $p$, such that: if $T$ has a polynomial-size Frege proof then $p$ has a polynomial-size non-commutative arithmetic formula; and conversely, when $T$ is a DNF, if $p$ has a polynomial-size non-commutative arithmetic formula over $GF(2)$ then $T$ has a Frege proof of quasi-polynomial size.

cs.CC↗

arXiv2014

Generating Matrix Identities and Proof Complexity

Motivated by the fundamental lower bounds questions in proof complexity, we initiate the study of matrix identities as hard instances for strong proof systems. A matrix identity of $d \times d$ matrices over a field $\mathbb{F}$, is a non-commutative polynomial $f(x_1,\ldots,x_n)$ over $\mathbb{F}$ such that $f$ vanishes on every $d \times d$ matrix assignment to its variables. We focus on arithmetic proofs, which are proofs of polynomial identities operating with arithmetic circuits and whose axioms are the polynomial-ring axioms (these proofs serve as an algebraic analogue of the Extended Frege propositional proof system; and over $GF(2)$ they constitute formally a sub-system of Extended Frege [HT12]). We introduce a decreasing in strength hierarchy of proof systems within arithmetic proofs, in which the $d$th level is a sound and complete proof system for proving $d \times d$ matrix identities (over a given field). For each level $d>2$ in the hierarchy, we establish a proof-size lower bound in terms of the number of variables in the matrix identity proved: we show the existence of a family of matrix identities $f_n$ with $n$ variables, such that any proof of $f_n=0$ requires $Ω(n^{2d})$ number of lines. The lower bound argument uses fundamental results from the theory of algebras with polynomial identities together with a generalization of the arguments in [Hru11]. We then set out to study matrix identities as hard instances for (full) arithmetic proofs. We present two conjectures, one about non-commutative arithmetic circuit complexity and the other about proof complexity, under which up to exponential-size lower bounds on arithmetic proofs (in terms of the arithmetic circuit size of the identities proved) hold. Finally, we discuss the applicability of our approach to strong propositional proof systems such as Extended Frege.

cs.CC↗

arXiv2014

Sparser Random 3SAT Refutation Algorithms and the Interpolation Problem

We formalize a combinatorial principle, called the 3XOR principle, due to Feige, Kim and Ofek (2006), as a family of unsatisfiable propositional formulas for which refutations of small size in any propositional proof system that possesses the feasible interpolation property imply an efficient deterministic refutation algorithm for random 3SAT with n variables and Ω(n^{1.4}) clauses. Such small size refutations would improve the state-of-the-art (with respect to the clause density) efficient refutation algorithm, which works only for Ω(n^{1.5}) many clauses (Feige and Ofek (2007)). We demonstrate polynomial-size refutations of the 3XOR principle in resolution operating with disjunctions of quadratic equations with small integer coefficients, denoted R(quad); this is a weak extension of cutting planes with small coefficients. We show that R(quad) is weakly automatizable iff R(lin) is weakly automatizable, where R(lin) is similar to R(quad) but with linear instead of quadratic equations (introduced in Raz and Tzameret (2008)). This reduces the problem of refuting random 3CNF with n variables and Ω(n^{1.4}) clauses to the interpolation problem of R(quad) and to the weak automatizability of R(lin).

cs.CC↗

arXiv2013

Short Proofs for the Determinant Identities

We study arithmetic proof systems P_c(F) and P_f(F) operating with arithmetic circuits and arithmetic formulas, respectively, that prove polynomial identities over a field F. We establish a series of structural theorems about these proof systems, the main one stating that P_c(F) proofs can be balanced: if a polynomial identity of syntactic degree d and depth k has a P_c(F) proof of size s, then it also has a P_c(F) proof of size poly(s,d) and depth O(k+\log^2 d + \log d\cd \log s). As a corollary, we obtain a quasipolynomial simulation of P_c(F) by P_f(F), for identities of a polynomial syntactic degree. Using these results we obtain the following: consider the identities det(XY) = det(X)det(Y) and det(Z)= z_{11}... z_{nn}, where X,Y and Z are nxn square matrices and Z is a triangular matrix with z_{11},..., z_{nn} on the diagonal (and det is the determinant polynomial). Then we can construct a polynomial-size arithmetic circuit det such that the above identities have P_c(F) proofs of polynomial-size and O(\log^2 n) depth. Moreover, there exists an arithmetic formula det of size n^{O(\log n)} such that the above identities have P_f(F) proofs of size n^{O(\log n)}. This yields a solution to a basic open problem in propositional proof complexity, namely, whether there are polynomial-size NC^2-Frege proofs for the determinant identities and the hard matrix identities, as considered, e.g., in Soltys and Cook (2004) (cf., Beame and Pitassi (1998)). We show that matrix identities like AB=I {\to} BA=I (for matrices over the two element field) as well as basic properties of the determinant have polynomial-size NC^2-Frege proofs, and quasipolynomial-size Frege proofs.

cs.CC↗