Algebraic Proof Systems (Invited Talk)

Author Toniann Pitassi



PDF
Thumbnail PDF

File

LIPIcs.ICALP.2021.5.pdf
  • Filesize: 287 kB
  • 1 pages

Document Identifiers

Author Details

Toniann Pitassi
  • University of Toronto, Canada

Cite AsGet BibTex

Toniann Pitassi. Algebraic Proof Systems (Invited Talk). In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, p. 5:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ICALP.2021.5

Abstract

Given a set of polynomial equations over a field F, how hard is it to prove that they are simultaneously unsolvable? In the last twenty years, algebraic proof systems for refuting such systems of equations have been extensively studied, revealing close connections to both upper bounds (connections between short refutations and efficient approximation algorithms) and lower bounds (connections to fundamental questions in circuit complexity.) The Ideal Proof System (IPS) is a simple yet powerful algebraic proof system, with very close connections to circuit lower bounds: [Joshua A. Grochow and Toniann Pitassi, 2018] proved that lower bounds for IPS imply VNP ≠ VP, and very recently connections in the other direction have been made, showing that circuit lower bounds imply IPS lower bounds [Rahul Santhanam and Iddo Tzameret, 2021; Yaroslav Alekseev et al., 2020]. In this talk I will survey the landscape of algebraic proof systems, focusing on their connections to complexity theory, derandomization, and standard proposional proof complexity. I will discuss the state-of-the-art lower bounds, as well as the relationship between algebraic systems and textbook style propositional proof systems. Finally we end with open problems, and some recent progress towards proving superpolynomial lower bounds for bounded-depth Frege systems with modular gates (a major open problem in propositional proof complexity).

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Theory of computation → Algebraic complexity theory
  • Theory of computation → Circuit complexity
Keywords
  • complexity theory
  • proof complexity
  • algebraic circuits

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Yaroslav Alekseev, Dima Grigoriev, Edward A. Hirsch, and Iddo Tzameret. Semi-algebraic proofs, IPS lower bounds, and the tau-conjecture: can a natural number be negative? In Konstantin Makarychev, Yury Makarychev, Madhur Tulsiani, Gautam Kamath, and Julia Chuzhoy, editors, Proccedings of the 52nd Symposium on Theory of Computing, (STOC), pages 54-67. ACM, 2020. Google Scholar
  2. 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. Google Scholar
  3. Rahul Santhanam and Iddo Tzameret. Iterated lower bound formulas: A diagonalization approach to proof co mplexity. In Proceedings of the 53rd Symposium on Theory of Computing (STOC). ACM, 2021. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail