Document Open Access Logo

IPS Lower Bounds for Formulas and Sum of ROABPs

Authors Prerona Chatterjee , Utsab Ghosal , Partha Mukhopadhyay , Amit Sinhababu

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2025.22.pdf
  • Filesize: 0.87 MB
  • 21 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Algebraic complexity theory
  • Theory of computation → Proof complexity
Keywords
  • Ideal Proof System
  • Lower Bound
  • Algebraic Complexity

Metrics

Abstract

We give new lower bounds for the fragments of the Ideal Proof System (IPS) introduced by Grochow and Pitassi [Joshua A. Grochow and Toniann Pitassi, 2018]. The Ideal Proof System is a central topic in algebraic proof complexity developed in the context of Nullstellensatz refutation [Paul Beame et al., 1994] and simulates Extended Frege efficiently. Our main results are as follows.  
- mult-IPS_{Lin'}: We prove nearly quadratic-size formula lower bound for multilinear refutation (over the Boolean hypercube) of a variant of the subset-sum axiom polynomial. Extending this, we obtain a nearly matching qualitative statement for a constant degree target polynomial. 
- IPS_{Lin'}: Over the fields of characteristic zero, we prove exponential-size sum-of-ROABPs lower bound for the refutation of a variant of the subset-sum axiom polynomial. The result also extends over the fields of positive characteristics when the target polynomial is suitably modified. The modification is inspired by the recent results [Tuomas Hakoniemi et al., 2024; Amik Raj Behera et al., 2025]. 
The mult-IPS_{Lin'} lower bound result is obtained by combining the quadratic-size formula lower bound technique of Kalorkoti [Kalorkoti, 1985] with some additional ideas. The proof technique of IPS_{Lin'} lower bound result is inspired by the recent lower bound result of Chatterjee, Kush, Saraf and Shpilka [Prerona Chatterjee et al., 2024].

Cite As Get BibTex

Prerona Chatterjee, Utsab Ghosal, Partha Mukhopadhyay, and Amit Sinhababu. IPS Lower Bounds for Formulas and Sum of ROABPs. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 22:1-22:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSTTCS.2025.22

Author Details

Prerona Chatterjee
  • School of Computer Sciences, NISER, Bhubaneswar, India
Utsab Ghosal
  • Chennai Mathematical Institute, India
Partha Mukhopadhyay
  • Chennai Mathematical Institute, India
Amit Sinhababu
  • Chennai Mathematical Institute, India

Funding

  • Ghosal, Utsab: Partially supported by Infosys grant.
  • Mukhopadhyay, Partha: Partially supported by Infosys grant.
  • Sinhababu, Amit: Partially supported by Infosys grant.

Acknowledgements

We thank the anonymous reviewers for their valuable feedback and suggestions.

References

  1. Miklós Ajtai. The complexity of the pigeonhole principle. In 29th Annual Symposium on Foundations of Computer Science (FOCS), pages 346-355. IEEE, 1988. URL: https://doi.org/10.1109/SFCS.1988.21948.
  2. Michael Alekhnovich and Alexander A. Razborov. Lower bounds for polynomial calculus: Non-binomial case. In 42nd Annual Symposium on Foundations of Computer Science, FOCS 2001, Las Vegas, Nevada, USA, October 14-17, 2001, pages 190-199. IEEE Computer Society, 2001. URL: https://doi.org/10.1109/SFCS.2001.959893.
  3. Robert Andrews and Michael A. Forbes. Ideals, determinants, and straightening: proving and using lower bounds for polynomial ideals. In Stefano Leonardi and Anupam Gupta, editors, STOC '22: 54th Annual ACM SIGACT Symposium on Theory of Computing, Rome, Italy, June 20 - 24, 2022, pages 389-402. ACM, 2022. URL: https://doi.org/10.1145/3519935.3520025.
  4. Walter Baur and Volker Strassen. The complexity of partial derivatives. Theor. Comput. Sci., 22:317-330, 1983. URL: https://doi.org/10.1016/0304-3975(83)90110-X.
  5. Paul Beame, Stephen A. Cook, and H. James Hoover. Log depth circuits for division and related problems. SIAM Journal on Computing, 23(4):740-751, 1994. URL: https://doi.org/10.1137/S0097539791197240.
  6. Paul Beame, Russell Impagliazzo, Jan Krajícek, Toniann Pitassi, and Pavel Pudlák. Lower bound on hilbert’s nullstellensatz and propositional proofs. In 35th Annual Symposium on Foundations of Computer Science, Santa Fe, New Mexico, USA, 20-22 November 1994, pages 794-806. IEEE Computer Society, 1994. URL: https://doi.org/10.1109/SFCS.1994.365714.
  7. Paul Beame, Toniann Pitassi, and Russell Impagliazzo. Exponential lower bounds for the pigeonhole principle. In 24th Annual ACM Symposium on Theory of Computing (STOC), pages 200-220. ACM, 1992. URL: https://doi.org/10.1145/129712.129739.
  8. Amik Raj Behera, Nutan Limaye, Varun Ramanathan, and Srikanth Srinivasan. New bounds for the ideal proof system in positive characteristic. Electron. Colloquium Comput. Complex., TR25-079, 2025. URL: https://eccc.weizmann.ac.il/report/2025/079/.
  9. Michael Ben-Or. Lower bounds for algebraic computation trees. In Proceedings of the Fifteenth Annual ACM Symposium on Theory of Computing (STOC), pages 80-86. ACM, 1983. URL: https://doi.org/10.1145/800061.808735.
  10. C. S. Bhargav, Prateek Dwivedi, and Nitin Saxena. Lower bounds for the sum of small-size algebraic branching programs. Theor. Comput. Sci., 1041:115214, 2025. URL: https://doi.org/10.1016/J.TCS.2025.115214.
  11. Peter Bürgisser, Michael Clausen, and Mohammad A Shokrollahi. Algebraic complexity theory, volume 315. Springer Science & Business Media, 2013. Google Scholar
  12. Samuel R. Buss, Dima Grigoriev, Russell Impagliazzo, and Toniann Pitassi. Linear gaps between degrees for the polynomial calculus modulo distinct primes. J. Comput. Syst. Sci., 62(2):267-289, 2001. URL: https://doi.org/10.1006/JCSS.2000.1726.
  13. Samuel R. Buss, Russell Impagliazzo, Jan Krajícek, Pavel Pudlák, Alexander A. Razborov, and Jirí Sgall. Proof complexity in algebraic systems and bounded depth frege systems with modular counting. Comput. Complex., 6(3):256-298, 1997. URL: https://doi.org/10.1007/BF01294258.
  14. Abhranil Chatterjee, Mrinal Kumar, and Ben Lee Volk. Determinants vs. algebraic branching programs. Comput. Complex., 33(2):11, 2024. URL: https://doi.org/10.1007/S00037-024-00258-Z.
  15. Prerona Chatterjee, Utsab Ghosal, Partha Mukhopadhyay, and Amit Sinhababu. IPS lower bounds for formulas and sum of roabps. CoRR, abs/2507.09515, 2025. URL: https://doi.org/10.48550/arXiv.2507.09515.
  16. Prerona Chatterjee, Mrinal Kumar, Adrian She, and Ben Lee Volk. Quadratic lower bounds for algebraic branching programs and formulas. Comput. Complex., 31(2):8, 2022. URL: https://doi.org/10.1007/S00037-022-00223-8.
  17. Prerona Chatterjee, Deepanshu Kush, Shubhangi Saraf, and Amir Shpilka. Lower bounds for set-multilinear branching programs. In Rahul Santhanam, editor, 39th Computational Complexity Conference, CCC 2024, July 22-25, 2024, Ann Arbor, MI, USA, volume 300 of LIPIcs, pages 20:1-20:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.CCC.2024.20.
  18. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44(1):36-50, 1979. URL: https://doi.org/10.2307/2273702.
  19. Tal Elbaz, Nashlen Govindasamy, Jiaqi Lu, and Iddo Tzameret. Lower bounds against the ideal proof system in finite fields. arXive Preprint, June 2025. Preprint. URL: https://doi.org/10.48550/arXiv.2506.17210.
  20. Michael A. Forbes. Low-depth algebraic circuit lower bounds over any field. In Rahul Santhanam, editor, 39th Computational Complexity Conference, CCC 2024, July 22-25, 2024, Ann Arbor, MI, USA, volume 300 of LIPIcs, pages 31:1-31:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.CCC.2024.31.
  21. Michael A. Forbes, Amir Shpilka, Iddo Tzameret, and Avi Wigderson. Proof complexity lower bounds from algebraic circuit complexity. Theory Comput., 17:1-88, 2021. URL: https://doi.org/10.4086/TOC.2021.V017A010.
  22. Nashlen Govindasamy, Tuomas Hakoniemi, and Iddo Tzameret. Simple hard instances for low-depth algebraic proofs. In 63rd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2022, Denver, CO, USA, October 31 - November 3, 2022, pages 188-199. IEEE, 2022. URL: https://doi.org/10.1109/FOCS54457.2022.00025.
  23. Joshua A. Grochow and Toniann Pitassi. Circuit complexity, proof complexity, and polynomial identity testing: The ideal proof system. J. ACM, 65(6):37:1-37:59, 2018. URL: https://doi.org/10.1145/3230742.
  24. Tuomas Hakoniemi, Nutan Limaye, and Iddo Tzameret. Functional lower bounds in algebraic proofs: Symmetry, lifting, and barriers. In Bojan Mohar, Igor Shinkar, and Ryan O'Donnell, editors, Proceedings of the 56th Annual ACM Symposium on Theory of Computing, STOC 2024, Vancouver, BC, Canada, June 24-28, 2024, pages 1396-1404. ACM, 2024. URL: https://doi.org/10.1145/3618260.3649616.
  25. Johan Håstad. On small-depth frege proofs for PHP. In 64th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2023, Santa Cruz, CA, USA, November 6-9, 2023, pages 37-49. IEEE, 2023. URL: https://doi.org/10.1109/FOCS57990.2023.00010.
  26. Johan Håstad and Kilian Risse. On bounded depth proofs for tseitin formulas on the grid; revisited. In 63rd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2022, Denver, CO, USA, October 31 - November 3, 2022, pages 1138-1149. IEEE, 2022. URL: https://doi.org/10.1109/FOCS54457.2022.00110.
  27. Pavel Hrubes and Amir Yehudayoff. Monotone separations for constant degree polynomials. Inf. Process. Lett., 110(1):1-3, 2009. URL: https://doi.org/10.1016/J.IPL.2009.09.003.
  28. Russell Impagliazzo, Pavel Pudlák, and Jirí Sgall. Lower bounds for the polynomial calculus and the gröbner basis algorithm. Comput. Complex., 8(2):127-144, 1999. URL: https://doi.org/10.1007/S000370050024.
  29. K. A. Kalorkoti. A lower bound for the formula size of rational functions. SIAM Journal on Computing, 14(3):678-687, 1985. URL: https://doi.org/10.1137/0214050.
  30. Jan Krajíček, Pavel Pudlák, and Alan Woods. Exponential lower bounds to the size of bounded depth frege proofs of the pigeonhole principle. Random Structures & Algorithms, 7(1):15-39, 1995. URL: https://doi.org/10.1002/rsa.3240070103.
  31. Martin Kreuzer and Lorenzo Robbiano. Computational Commutative Algebra 2, volume 2 of Springer-Verlag Algorithms and Computation in Mathematics. Springer-Verlag, Berlin, Heidelberg, 2005. URL: https://doi.org/10.1007/b138062.
  32. Fu Li, Iddo Tzameret, and Zhengyu Wang. Characterizing propositional proofs as noncommutative formulas. SIAM J. Comput., 47(4):1424-1462, 2018. URL: https://doi.org/10.1137/16M1107632.
  33. Nutan Limaye, Srikanth Srinivasan, and Sébastien Tavenas. Superpolynomial lower bounds against low-depth algebraic circuits. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 804-814. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00083.
  34. Toniann Pitassi. Algebraic propositional proof systems. In Neil Immerman and Phokion G. Kolaitis, editors, Descriptive Complexity and Finite Models, Proceedings of a DIMACS Workshop 1996, Princeton, New Jersey, USA, January 14-17, 1996, volume 31 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 215-244. DIMACS/AMS, 1996. URL: https://doi.org/10.1090/DIMACS/031/07.
  35. Toniann Pitassi and Russell Impagliazzo. Exponential lower bounds for the polynomial calculus. In Proceedings of the 26th Annual ACM Symposium on Theory of Computing (STOC), pages 129-135. ACM, 1994. URL: https://doi.org/10.1145/195058.195120.
  36. Toniann Pitassi, Benjamin Rossman, Rocco A. Servedio, and Li-Yang Tan. Poly-logarithmic frege depth lower bounds via an expander switching lemma. In Daniel Wichs and Yishay Mansour, editors, Proceedings of the 48th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2016, Cambridge, MA, USA, June 18-21, 2016, pages 644-657. ACM, 2016. URL: https://doi.org/10.1145/2897518.2897637.
  37. Alexander A. Razborov. Lower bounds for the polynomial calculus. Comput. Complex., 7(4):291-324, 1998. URL: https://doi.org/10.1007/S000370050013.
  38. Robert A. Reckhow. On the lengths of proofs in the propositional calculus. Ph.d. thesis, University of Toronto, 1976. Technical Report #87. Google Scholar
  39. Ramprasad Saptharishi. A survey of lower bounds in arithmetic circuit complexity. Manuscript online at https://github.com/dasarpmar/lowerbounds-survey/releases/download/v9.0.3/fancymain.pdf, 2021. A selection of lower bounds in arithmatic circuit complexity. Google Scholar
  40. Amir Shpilka and Amir Yehudayoff. Arithmetic circuits: A survey of recent results and open questions. Found. Trends Theor. Comput. Sci., 5(3-4):207-388, 2010. URL: https://doi.org/10.1561/0400000039.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact