Iddo Tzameret Publications




        Manuscript

Jiaqi Lu, Rahul Santhanam and Iddo Tzameret Meta-Mathematics of Algebraic Circuit Lower Bounds and Conjectured Tautologies Hard for AC0[p]-Frege Manuscript, 2024.

soon |
How hard is it to prove algebraic circuit lower bounds? We study this question and connectit to proof complexity lower bounds in the conjectured tautologies regime (cf. [Raz15] and references therein) which seeks to establish proof-length lower bounds for propositional formulas expressing complexity-theoretic statements we believe are true. We focus on the following question: which proof system can (efficiently) prove frontier lower bounds such as those against constantdepth algebraic circuits computing the Permanent over finite fields (Limaye-Srinivasan-Tavenas and Forbes [LST21, For24]). We provide both concrete lower bounds, concrete upper bounds and unconditional lower bounds in the conjectured tautologies regime, as follows:

PC lower bounds: Polynomial calculus (PC) cannot efficiently prove the lower bounds of [LST21, For24], or in fact super-polynomial constant-depth algebraic circuit lower bounds for any polynomial. This gives a constant-depth algebraic analogue of the PC lower bounds shown by Razborov [Raz98] and Raz [Raz04] for Boolean circuit lower bounds.

NC2-Frege upper bounds: According to the informal correspondence between circuit classes C and proof systems operating with proof-lines from C, it is expected that propositional proofs operating with NC-circuits (i.e., NC-Frege) are both necessary and sufficient to prove rank-based arguments. We show that already NC2-Frege (and the bounded arithmetic theory VNC2) is sufficient to formulate the rank argument in [LST21, For24] and hence prove constant-depth algebraic circuit lower bounds over finite fields.

No short AC0[p]-Frege proofs: We consider the question whether constant-depth algebraic proofs (formally IPS) can efficiently prove the lower bounds in [LST21, For24] (over finite fields) and formulate a DNF formula expressing that no such efficient proof exists. We show unconditionally that this family of DNF formulas, expected to be tautologies, do not admit propositional AC0[p]-Frege proofs, infinitely often. This adapts the diagonalization framework of Santhanam-Tzameret [ST21], which was predicated upon unbounded-depth algebraic circuit lower bounds, to the constant-depth setting. This result has the following special features: (i) Necessity: we show that super-polynomial lower bounds for the DNF formulas we consider, in which we replace ‘constant-depth algebraic circuits’ with any “reasonable” algebraic circuit class C, are necessary in order to prove super-polynomial lower bounds against algebraic proofs operating with circuits from C. (ii) Existential depth amplification: our DNF 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. (iii) Expected validity: Razborov [Raz96] and Kraj´ıˇcek [Kra04] conjectured that the Extended Frege proof system cannot efficiently prove super-polynomial Boolean circuit lower bounds for any Boolean function. We observe that under an analogous constant-depth algebraic conjecture our DNF formulas are tautologies.


        Published

Rahul Santhanam and Iddo Tzameret Iterated Lower Bound Formulas: A Diagonalization-Based Approach to Proof Complexity To appear in SIAM J. Comput. 2025 (SICOMP) (special issue of STOC 2021).

PDF | STOC Video |
We propose a diagonalization-based approach to several important questions in proof complexity. We illustrate this approach in the context of the algebraic proof system IPS and in the context of propositional proof systems more generally. We give an explicit sequence of CNF formulas $\phi_n$ such that $VNP \neq= VP$ iff there are no polynomial-size IPS proofs for the formulas $\phi_n$. This provides a natural equivalence between proof size lower bounds and standard algebraic complexity lower bounds. Our proof of this fact uses the implication from IPS lower bounds to algebraic complexity lower bounds due to Grochow and Pitassi together with a diagonalization argument: the formulas φn themselves assert the non-existence of short IPS proofs for formulas encoding VNP $\neq$ VP at a different input length. Our result also has meta-mathematical implications: it gives evidence for the difficulty of proving strong lower bounds for IPS within IPS. More generally, for any strong enough propositional proof system R we propose a new explicit hard candidate, the iterated R-lower bound formulas, which inductively asserts the non-existence of short R proofs for formulas encoding this same statement at a different input length. We show that these formulas are unconditionally hard for Resolution following recent results of Atserias and M¨uller and of Garlik. We further give evidence in favour of this hypothesis for other proof systems.

Albert Atserias and Iddo Tzameret Feasibly Constructive Proof of Schwartz-Zippel Lemma and the Complexity of Finding Hitting Sets In 57th Annual ACM Symposium on Theory of Computing (STOC), Prague, June 2025.

PDF |
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 \(\mathsf{S}^1_2\) for polynomial-time reasoning. One consequence of this is that the theory \(\mathsf{S}^1_2 + \mathsf{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 \(\mathsf{dWPHP(PV)}\), over the theory \(\mathsf{S}^1_2\). This is a contribution to a line of research studying the reverse mathematics of computational complexity (cf. Chen-Li-Oliveira, FOCS'24). 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 (Kleinberg-Korten-Mitropolsky-Papadimitriou, ITCS'21; cf. Korten, FOCS'21). This class is also known and studied as the class of Range Avoidance Problems (Ren-Santhanam-Wang, FOCS'22).

Fedor Part, Neil Thapen and Iddo Tzameret First-Order Reasoning and Efficient Semi-Algebraic Proofs Annals of Pure and Applied Logic (APAL), Elsevier, Vol. 176 (1), 2024.

PDF | DOI |
Semi-algebraic proof systems such as sum-of-squares (SoS) have attracted a lot of attention 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. Moreover, we prove new results for propositional proofs, and specifically extend Berkholz's dynamic-by-static simulation of polynomial calculus (PC) by to PC with the radical rule.

Tuomas Hakoniemi, Nutan Limaye and Iddo Tzameret Functional Lower Bounds in Algebraic Proofs: Symmetry, Lifting, and Barriers In 56th Annual ACM Symposium on Theory of Computing (STOC), Vancouver, June 2024.
Manuscript, 2023.

PDF | DOI | ECCC |

  Strong algebraic proof systems such as IPS (Ideal Proof System; Grochow-Pitassi 2018) 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 2021), which reduces the hardness of refuting a polynomial equation \(f(\overline x)=0\) with no Boolean solutions to the hardness of computing the function \(\frac{1}{f(\overline 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. Specifically, we show the following:

\(\textbf{Nullstellensatz degree lower bounds using symmetry}\): Extending [FSTW21] we show that every unsatisfiable symmetric polynomial with \(n\) variables requires degree \(>n\) refutations (over sufficiently large characteristic). Using symmetry again, by characterising the \(\frac{n}{2}\)-homogeneous slice appearing in refutations, we show that unsatisfiable *invariant* polynomials of degree \(\frac{n}{2}\) require degree \(\ge n\) refutations.
\(\textbf{Lifting to size lower bounds}\): Lifting our Nullstellensatz degree bounds to IPS-size lower bounds, we obtain exponential lower bounds for any poly-logarithmic degree symmetric instance against IPS refutations written as oblivious read-once algebraic programs (roABP-IPS). For invariant polynomials, we show lower bounds against roABP-IPS and refutations written as multilinear formulas in the placeholder IPS regime (studied by Andrews-Forbes 2022), where the hard instances do not necessarily have small roABPs themselves, including over \emph{positive characteristic} fields. This provides the first IPS-fragment lower bounds over finite fields. By an adaptation of the work of Amireddy, Garg, Kayal, Saha and Thankey 2023, we extend the constant-depth IPS lower bounds obtained recently in Govindasamy, Hakoniemi and Tzameret [GHT22] which held only for multilinear proofs, to \(O(\log \log n) \), individual degree proofs. This is a natural and stronger constant depth proof system than in [GHT22], which we show admits small refutations for standard hard instances like PHP and Tseitin formulas.
\(\textbf{Barriers for Boolean instances}\): While lower bounds against strong propositional proof systems were the original motivation for studying algebraic proof systems in the 1990s [BeameIKPP96,BussIKPRS96], we show that the functional lower bound method alone cannot establish any size lower bound for *Boolean* instances for any sufficiently strong proof systems, and in particular, cannot lead to lower bounds against AC\(^0[p]\)-Frege and TC\(^0\)-Frege.

Yaroslav Alekseev, Dima Grigoriev, Edward A. Hirsch and Iddo Tzameret Semi-Algebraic Proofs, IPS Lower Bounds and the τ-Conjecture: Can a Natural Number be Negative? In SIAM Journal on Computing (SICOMP), 2024.

PDF | DOI |
tbc.

Iddo Tzameret and Lu-Ming Zhang Stretching Demi-Bits and Nondeterministic-Secure Pseudorandomness In proceedings of 15th Innovations in Theoretical Computer Science Conference (ITCS) 2024, January, 2024, Berkeley, CA, USA. Electronic Colloquium on Computational Complexity TR23-057, 2023.

PDF | ECCC |
tbc.

Nashlen Govindasamy, Tuomas Hakoniemi and Iddo Tzameret Simple Hard Instances for Low-Depth Algebraic Proofs In Symp. on Found. Computer Science (FOCS), 2022.

PDF | DOI |
tbc.

Rahul Santhanam and Iddo Tzameret Iterated Lower Bound Formulas: A Diagonalization-Based Approach to Proof Complexity In 53rd Annual ACM Symposium on Theory of Computing (STOC), Rome, June 2021. Invited to SIAM J. Comput. special issue.

PDF | STOC Video |
tbc.

Fedor Part, Neil Thapen and Iddo Tzameret First-Order Reasoning and Efficient Semi-Algebraic Proofs In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic In Computer Science (LICS), June 2021.

PDF | Fedor's Video |
tbc.

Michael Forbes, Amir Shpilka, Iddo Tzameret and Avi Wigderson Proof Complexity Lower Bounds from Algebraic Circuit Complexity Theory of Computing (ToC), Vol. 17, no.10, 1-88, 2021. (Invited; special journal issue on CCC'16; DOI:10.4086/toc.2021.v017a010)

PDF | DOI |
tbc.

Fedor Part and Iddo Tzameret Resolution with Counting: Different Moduli and Dag-Like Lower Bounds Comput. Complex. (CC), Springer Birkhäuser, (2021) 30:2.

PDF | DOI |
tbc.

Iddo Tzameret and Stephen A. Cook Uniform, Integral and Feasible Proofs for the Determinant Identities Journal of the ACM (JACM), Vol. 68, No. 2 (2021).

PDF | DOI |
tbc.

Yaroslav Alekseev, Dima Grigoriev, Edward A. Hirsch and Iddo Tzameret Semi-Algebraic Proofs, IPS Lower Bounds and the τ-Conjecture: Can a Natural Number be Negative? In proceedings of 52nd Annual ACM Symposium on Theory of Computing (STOC), Chicago, IL, June 22-26, 2020.

PDF | DOI |
tbc.

Fedor Part and Iddo Tzameret Resolution with Counting: Different Moduli and Dag-Like Lower Bounds In proceedings of 11th Innovations in Theoretical Computer Science Conference (ITCS) 2020, January, 2020, Seattle, WA, USA. Electronic Colloquium on Computational Complexity TR18-117, 2018.

PDF | DOI |
tbc.

Iddo Tzameret From classical proof theory to P vs. NP: A Guide to Bounded Theories. 28th EACSL Annual Conference on Computer Science Logic (CSL) 2020, January 13-16, 2020, Barcelona, Spain. LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik 2020.

PDF |
tbc.

Fu Li, Iddo Tzameret and Zhengyu Wang Characterizing Propositional Proofs as Non-commutative Formulas SIAM Journal on Computing (SICOMP) 47(4), pp. 1424-1462, 2018.

PDF |
tbc.

Fu Li and Iddo Tzameret Witnessing Matrix Identities and Proof Complexity Int. J. Algebra Comput. (IJAC) 28 (2), pp. 217-256. World Scientific, 2018.

PDF |
tbc.

Iddo Tzameret and Stephen A. Cook Uniform, Integral and Efficient Proofs for the Determinant Identities In Proceedings of the 32th Annual ACM/IEEE Symposium on Logic In Computer Science (LICS), 20-23 June 2017. Invited to the Journal of the ACM (JACM)

PDF |
tbc.

Tonnian Pitassi and Iddo Tzameret Algebraic Proof Complexity: Progress, Frontiers and Challenges ACM SIGLOG News (SIGLOG), 3 (3), pp. 21-43, ACM New York, July 2016.

PDF |
tbc.

Michael Forbes, Amir Shpilka, Iddo Tzameret and Avi Wigderson Proof Complexity Lower Bounds from Algebraic Circuit Complexity In Proceedings of the 31th Annual Computational Complexity Conference (CCC): June 16-18, 2016. Invited to the special journal issue on CCC'16 (Theory Comput. ToC)

PDF |
tbc.

Fu Li, Iddo Tzameret and Zhengyu Wang Non-commutative Formulas and Frege Lower Bounds: a New Characterization of Propositional Proofs In Proceedings of the 30th Annual Computational Complexity Conference (CCC): June 17-19, 2015. Invited to the special journal issue on CCC'15 (Comput. Complexity CC).

PDF |
tbc.

Pavel Hrubeš and Iddo Tzameret Short Proofs for the Determinant Identities SIAM Journal on Computing (SICOMP) 44 (2015), No. 2, pp. 340-383.

PDF |
tbc.

Sebastian Müller and Iddo Tzameret Short Propositional Refutations for Dense Random 3CNF Formulas Annals of Pure and Applied Logic (APAL) 165(12):1864-1918 (2014).

PDF |
tbc.

Iddo Tzameret Sparser Random 3SAT Refutation Algorithms and the Interpolation Problem Preliminary version in Proceedings of the 41st International Colloquium on Automata, Languages and Programming (ICALP) track A, July 2014.

PDF |
tbc.

Eric Allender, George Davie, Luke Friedman, Sam Hopkins and Iddo Tzameret Kolmogorov Complexity, Circuits, and the Strength of Formal Theories of Arithmetic Chicago Journal of Theoretical Computer Science (CJTCS) (5): 1-15, 2013. Preprint in ECCC 2012.

PDF |
tbc.

Sebastian Müller and Iddo Tzameret Proving Random Formulas in Propositional Logic In Johan van Benthem and Fenrong Liu, eds. Logic Across the University: Foundations and Application, Proceedings of the Tsinghua Logic Conference, pp. 201-208. Volume 47: Studies in Logic. College Publications London, 2013.

PDF |
tbc.

Pavel Hrubeš and Iddo Tzameret Short Proofs for the Determinant Identities In Proceedings of the 44th Annual ACM Symposium on the Theory of Computing (STOC), pp.193-212. 19-22 May 2012.

PDF |
tbc.

Sebastian Müller and Iddo Tzameret Short Propositional Refutations for Dense Random 3CNF Formulas Proceedings of the 27th Annual ACM/IEEE Symposium on Logic In Computer Science (LICS), pp. 501-510. 25-28 June 2012. Preprint in ECCC.

PDF | DOI |
tbc.

Iddo Tzameret Algebraic Proofs over Noncommutative Formulas Information and Computation (I&C) 209 (10):1269-1292, 2011.

PDF |
tbc.

Nachum Dershowitz and Iddo Tzameret Complexity of Propositional Proofs under a Promise ACM Transactions on Computational Logic (ToCL) 11(3):1-29, 2010.

PDF |
tbc.

Iddo Tzameret Algebraic Proofs over Noncommutative Formulas invited to The 7th Annual Conference on Theory and Applications of Models of Computation, June 7-11, 2010. Volume 6108 of Lecture Notes in Comput. Sci., pp. 60-71. Springer, Berlin.

PDF |
tbc.

Pavel Hrubeš and Iddo Tzameret The Proof Complexity of Polynomial Identities Proceedings of the 24th IEEE Conference on Computational Complexity (CCC), pp. 41-51, 15-18 July 2009.

PDF | Conference Version |
tbc.

Ran Raz and Iddo Tzameret Resolution over Linear Equations and Multilinear Proofs Annals of Pure and Applied Logic (APAL) 155(3):194-224, 2008. Preliminary version in ECCC 2007 [arXiv] [doi:10.1016/j.apal.2008.04.001]

PDF |
tbc.

Ran Raz and Iddo Tzameret The Strength of Multilinear Proofs Computational Complexity (CC) 17(3) October, 2008. Preliminary version in ECCC 2006. [doi:10.1007/s00037-008-0246-0]

PDF |
tbc.

Nachum Dershowitz and Iddo Tzameret Complexity of Propositional Proofs under a Promise Preliminary version in Proceedings of the 34th International Colloquium on Automata, Languages and Programming (ICALP) track A, pp. 9-13 July 2007.

PDF |
tbc.

Nachum Dershowitz and Iddo Tzameret Gap Embedding for Well-Quasi-Orderings Electronic Notes in Theoretical Computer Science, Vol. 84.

PDF |
tbc.

Nachum Dershowitz and Iddo Tzameret Gap Embedding for Well-Quasi-Orderings Proceedings of the 10th Workshop on Logic, Language, Information and Computation (WoLLIC '03).

PDF |
tbc.

Nachum Dershowitz and Iddo Tzameret Quasi-Ordered Gap Embedding Extended Abstracts of the International Workshop on Termination. (WST '03), Valencia, Spain.

PDF |
tbc.


        Notes

Iddo Tzameret Håstad‘s Separation of Constant-Depth Circuits Using Sipser Functions Apr. 2009. (Updated Oct. 2012)

PDF |
tbc.

Iddo Tzameret On the Structure and Complexity of Symbolic Proofs of Polynomial Identities Manuscript, April 2008. Subsumed (and improved) in the above paper with P. Hrubeš.

PDF |
tbc.

Iddo Tzameret A Concise Research Summary Note, January 2017

PDF |
tbc.

Iddo Tzameret Complexity, Proofs and Algebra Note.

PDF |
tbc.


        Dissertations

Studies in Algebraic and Propositional Proof Complexity PhD thesis, Tel Aviv University, preliminary submission 2008 (diploma conferred 2010).

PDF |
tbc.

Kruskal-Friedman Gap Embedding Theorems Over Well-Quasi-Orderings M.Sc. thesis, School of Computer Science, Tel Aviv university.

PDF |
tbc.