Document Open Access Logo

From Proof Complexity to Circuit Complexity via Interactive Protocols

Authors Noel Arteche , Erfan Khaniki , Ján Pich , Rahul Santhanam

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2024.12.pdf
  • Filesize: 0.87 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Theory of computation → Circuit complexity
  • Theory of computation → Complexity theory and logic
Keywords
  • proof complexity
  • circuit complexity
  • interactive protocols

Metrics

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

Abstract

Folklore in complexity theory suspects that circuit lower bounds against NC¹ or P/poly, currently out of reach, are a necessary step towards proving strong proof complexity lower bounds for systems like Frege or Extended Frege. Establishing such a connection formally, however, is already daunting, as it would imply the breakthrough separation NEXP ⊈ P/poly, as recently observed by Pich and Santhanam [Pich and Santhanam, 2023].
We show such a connection conditionally for the Implicit Extended Frege proof system (iEF) introduced by Krajíček [Krajíček, 2004], capable of formalizing most of contemporary complexity theory. In particular, we show that if iEF proves efficiently the standard derandomization assumption that a concrete Boolean function is hard on average for subexponential-size circuits, then any superpolynomial lower bound on the length of iEF proofs implies #P ⊈ FP/poly (which would in turn imply, for example, PSPACE ⊈ P/poly). Our proof exploits the formalization inside iEF of the soundness of the sum-check protocol of Lund, Fortnow, Karloff, and Nisan [Lund et al., 1992]. This has consequences for the self-provability of circuit upper bounds in iEF. Interestingly, further improving our result seems to require progress in constructing interactive proof systems with more efficient provers.

Cite As Get BibTex

Noel Arteche, Erfan Khaniki, Ján Pich, and Rahul Santhanam. From Proof Complexity to Circuit Complexity via Interactive Protocols. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.ICALP.2024.12

Author Details

Noel Arteche
  • Lund University, Sweden
  • University of Copenhagen, Denmark
Erfan Khaniki
  • Institute of Mathematics of the Czech Academy of Sciences, Prague, Czech Republic
Ján Pich
  • University of Oxford, UK
Rahul Santhanam
  • University of Oxford, UK

Funding

  • Arteche, Noel: This work was supported by the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation.
  • Khaniki, Erfan: This work was supported by the Institute of Mathematics of the Czech Academy of Sciences (RVO 67985840) and GAČR grant 19-27871X.
  • Pich, Ján: This work received support from the Royal Society University Research Fellowship URF\R1\211106 "Proof complexity and circuit complexity: a unified approach".

Acknowledgements

Independently, Albert Atserias suggested to us to consider using interactive proof systems to derive this type of connections. We thank Pavel Pudlák for useful comments, and the anonymous reviewers for relevant comments and references. This work was done in part while the first author was visiting the University of Oxford and the Institute of Mathematics of the Czech Academy of Sciences. For the purpose of Open Access, the authors have applied a CC BY public copyright license to any Author Accepted Manuscript version arising from this submission.

References

  1. Miklós Ajtai. Σ₁¹-formulae on finite structures. Annals of Pure and Applied Logic, 24(1):1-48, 1983. Google Scholar
  2. Miklós Ajtai. The complexity of the pigeonhole principle. Combinatorica, 14:417-433, 1994. Google Scholar
  3. Noga Alon and Ravi B Boppana. The monotone circuit complexity of Boolean functions. Combinatorica, 7:1-22, 1987. Google Scholar
  4. Aleksandr Egorovich Andreev. A method for obtaining lower bounds on the complexity of individual monotone functions. In Doklady Akademii Nauk, volume 282(5), pages 1033-1037. Russian Academy of Sciences, 1985. Google Scholar
  5. Sanjeev Arora and Boaz Barak. Computational Complexity: A Modern Approach. Cambridge University Press, 2009. Google Scholar
  6. Noel Arteche, Gaia Carenini, and Matthew Gray. Quantum automating TC⁰-Frege is LWE-hard, 2024. URL: https://arxiv.org/abs/2402.10351.
  7. László Babai. Trading group theory for randomness. In Proceedings of the seventeenth annual ACM symposium on Theory of computing, pages 421-429, 1985. Google Scholar
  8. Paul Beame, Russell Impagliazzo, Jan Krajíček, Toniann Pitassi, Pavel Pudlák, and Alan Woods. Exponential lower bounds for the pigeonhole principle. In Proceedings of the Twenty-Fourth Annual ACM Symposium on Theory of Computing, pages 200-220, 1992. Google Scholar
  9. Arnold Beckmann and Sam Buss. The NP search problems of Frege and Extended Frege proofs. ACM Transactions on Computational Logic (TOCL), 18(2):1-19, 2017. Google Scholar
  10. Stephen Bellantoni, Toniann Pitassi, and Alasdair Urquhart. Approximation and small-depth Frege proofs. SIAM Journal on Computing, 21(6):1161-1179, 1992. Google Scholar
  11. Olaf Beyersdorff, Ilario Bonacina, Leroy Chew, and Jan Pich. Frege systems for quantified boolean logic. Journal of the ACM (JACM), 67(2):1-36, 2020. Google Scholar
  12. Maria Luisa Bonet, Carlos Domingo, Ricard Gavalda, Alexis Maciel, and Toniann Pitassi. Non-automatizability of bounded-depth Frege proofs. computational complexity, 13:47-68, 2004. Google Scholar
  13. Maria Luisa Bonet, Toniann Pitassi, and Ran Raz. On interpolation and automatization for Frege systems. SIAM Journal on Computing, 29(6):1939-1967, 2000. Google Scholar
  14. Peter Bürgisser. Completeness and reduction in algebraic complexity theory. Algorithms and Computation in Mathematics, 2000. Google Scholar
  15. Samuel R Buss. Bounded arithmetic. Princeton University, 1985. Google Scholar
  16. Samuel R Buss. Relating the bounded arithmetic and polynomial time hierarchies. Annals of Pure and Applied Logic, 75(1-2):67-77, 1995. Google Scholar
  17. A Cobham. The intrinsic computational difficulty of functions. In Proc. 1964 Congress for Logic, Methodology, and the Philosophy of Science, pages 24-30. North-Holland, 1964. Google Scholar
  18. Stephen Cook. Relating the provable collapse of 𝐏 to NC¹ and the power of logical theories. In Proof Complexity and Feasible Arithmetics, pages 73-91, 1996. Google Scholar
  19. Stephen Cook and Jan Krajíček. Consequences of the provability of NP ⊆ 𝐏/poly. The Journal of Symbolic Logic, 72(4):1353-1371, 2007. Google Scholar
  20. Stephen Cook and Phuong Nguyen. Logical Foundations of Proof Complexity. Cambridge University Press, 2010. Google Scholar
  21. Stephen A. Cook. Feasibly constructive proofs and the propositional calculus. In Proceedings of the Seventh Annual ACM Symposium on Theory of Computing, pages 83-97, 1975. Google Scholar
  22. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. Logic, Automata, and Computational Complexity, 1979. Google Scholar
  23. Ben Davis and Robert Robere. Colourful TFNP and Propositional Proofs. In 38th Computational Complexity Conference (CCC 2023), volume 264 of Leibniz International Proceedings in Informatics (LIPIcs), pages 36:1-36:21, 2023. URL: https://doi.org/10.4230/LIPIcs.CCC.2023.36.
  24. Susanna De Rezende, Or Meir, Jakob Nordström, Toniann Pitassi, Robert Robere, and Marc Vinyals. Lifting with simple gadgets and applications to circuit and proof complexity. In 61st Annual Symposium on Foundations of Computer Science (FOCS), pages 24-30, 2020. Google Scholar
  25. Susanna F de Rezende, Mika Göös, and Robert Robere. Proofs, circuits, and communication. ACM SIGACT News, 53(1):59-82, 2022. Google Scholar
  26. Merrick Furst, James B Saxe, and Michael Sipser. Parity, circuits, and the polynomial-time hierarchy. Mathematical Systems Theory, 17(1):13-27, 1984. Google Scholar
  27. Ankit Garg, Mika Göös, Pritish Kamath, and Dmitry Sokolov. Monotone circuit lower bounds from resolution. In Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing, pages 902-911, 2018. Google Scholar
  28. Azza Gaysin. Proof complexity of CSP. arXiv preprint, 2022. URL: https://arxiv.org/abs/2201.00913.
  29. Azza Gaysin. Proof complexity of universal algebra in a CSP dichotomy proof. arXiv preprint, 2024. URL: https://arxiv.org/abs/2403.06704.
  30. Joshua A Grochow. Polynomial identity testing and the Ideal proof system: PIT is in NP if and only if IPS can be p-simulated by a Cook-Reckhow proof system. arXiv preprint, 2023. URL: https://arxiv.org/abs/2306.02184.
  31. Joshua A Grochow and Toniann Pitassi. Circuit complexity, proof complexity, and polynomial identity testing: The ideal proof system. Journal of the ACM (JACM), 65(6):1-59, 2018. Google Scholar
  32. Tuomas Hakoniemi. Feasible interpolation for Polynomial Calculus and Sums-of-Squares. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020), 2020. Google Scholar
  33. John Håstad. Almost optimal lower bounds for small depth circuits. In Proceedings of the Eighteenth Annual ACM Symposium on Theory of Computing, pages 6-20, 1986. Google Scholar
  34. Russell Impagliazzo and Avi Wigderson. 𝐏 = BPP if 𝐄 requires exponential circuits: Derandomizing the XOR lemma. In Proceedings of the Twenty-Ninth Annual ACM Symposium on Theory of computing, pages 220-229, 1997. Google Scholar
  35. Emil Jeřábek. Dual weak pigeonhole principle, Boolean complexity, and derandomization. Annals of Pure and Applied Logic, 129(1-3):1-37, 2004. Google Scholar
  36. Emil Jeřábek. Weak pigeonhole principle, and randomized computation. PhD thesis, Faculty of Mathematics and Physics, Charles University, Prague, 2005. Google Scholar
  37. Emil Jeřábek. Approximate counting in bounded arithmetic. The Journal of Symbolic Logic, 72(3):959-993, 2007. Google Scholar
  38. Valentine Kabanets and Russell Impagliazzo. Derandomizing polynomial identity tests means proving circuit lower bounds. Computational Complexity, 13(1/2):1-46, 2004. Google Scholar
  39. Erfan Khaniki. (Im)possibilty results in Proof Complexity and Arithmetic. PhD thesis, Faculty of Mathematics and Physics, Charles University, Prague, 2023. URL: https://dspace.cuni.cz/handle/20.500.11956/187614.
  40. Erfan Khaniki. Jump operators, interactive proofs, and proof complexity generators, 2023. Unpublished preprint. Google Scholar
  41. Leszek Aleksander Kołodziejczyk, Phuong Nguyen, and Neil Thapen. The provably total NP search problems of weak second order bounded arithmetic. Annals of Pure and Applied Logic, 162(6):419-446, 2011. Google Scholar
  42. Jan Krajíček. Exponentiation and second-order bounded arithmetic. Annals of Pure and Applied Logic, 48(3):261-276, 1990. Google Scholar
  43. Jan Krajíček. Lower bounds to the size of constant-depth propositional proofs. The Journal of Symbolic Logic, 59(1):73-86, 1994. Google Scholar
  44. Jan Krajíček. Diagonalization in proof complexity. Fundamenta Mathematicae, 182:181-192, 2004. Google Scholar
  45. Jan Krajíček. Implicit proofs. The Journal of Symbolic Logic, 69(2):387-397, 2004. Google Scholar
  46. Jan Krajíček. Consistency of circuit evaluation, Extended Resolution and total NP search problems. In Forum of Mathematics, Sigma, volume 4, page e15. Cambridge University Press, 2016. Google Scholar
  47. Jan Krajíček and Pavel Pudlák. Quantified propositional calculi and fragments of bounded arithmetic. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 36(1):29-46, 1990. Google Scholar
  48. Jan Krajíček, Pavel Pudlák, and Gaisi Takeuti. Bounded arithmetic and the polynomial hierarchy. Annals of Pure and Applied Logic, 52(1-2), 1991. Google Scholar
  49. Jan Krajíček, Pavel Pudlák, and Alan Woods. An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle. Random Structures & Algorithms, 7(1):15-39, 1995. Google Scholar
  50. Jan Krajíček. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. The Journal of Symbolic Logic, 62(2):457-486, 1997. Google Scholar
  51. Jan Krajíček. Proof Complexity. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2019. URL: https://doi.org/10.1017/9781108242066.
  52. Jan Krajíček and Pavel Pudlák. Some consequences of cryptographical conjectures for S¹₂ and EF . Information and Computation, 140(1):82-94, 1998. Google Scholar
  53. Shachar Lovett, Raghu Meka, Ian Mertz, Toniann Pitassi, and Jiapeng Zhang. Lifting with sunflowers. In 13th Innovations in Theoretical Computer Science Conference (ITCS 2022), 2022. Google Scholar
  54. Carsten Lund, Lance Fortnow, Howard Karloff, and Noam Nisan. Algebraic methods for interactive proof systems. Journal of the ACM (JACM), 39(4):859-868, 1992. Google Scholar
  55. Moritz Müller and Ján Pich. Feasibly constructive proofs of succinct weak circuit lower bounds. Annals of Pure and Applied Logic, 171(2):102735, 2020. Google Scholar
  56. Noam Nisan and Avi Wigderson. Hardness vs randomness. Journal of Computer and System Sciences, 49(2):149-167, 1994. Google Scholar
  57. Ján Pich. Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic. Logical Methods in Computer Science, 11, 2015. Google Scholar
  58. Jan Pich and Rahul Santhanam. Towards 𝐏 ≠ NP from Extended Frege lower bounds. arXiv preprint, 2023. URL: https://arxiv.org/abs/2312.08163.
  59. Toniann Pitassi, Paul Beame, and Russell Impagliazzo. Exponential lower bounds for the pigeonhole principle. Computational complexity, 3:97-140, 1993. Google Scholar
  60. Vaughan R Pratt. Every prime has a succinct certificate. SIAM Journal on Computing, 4(3):214-220, 1975. Google Scholar
  61. Pavel Pudlák. Lower bounds for resolution and cutting planes proofs and monotone computations. The Journal of Symbolic Logic, 62(3):981-998, 1997. Google Scholar
  62. Pavel Pudlák. Reflection principles, propositional proof systems, and theories, 2020. URL: https://arxiv.org/abs/2007.14835.
  63. Ran Raz and Pierre McKenzie. Separation of the monotone NC hierarchy. In Proceedings 38th Annual Symposium on Foundations of Computer Science (FOCS), pages 234-243. IEEE, 1997. Google Scholar
  64. Alexander Razborov. Lower bounds on the monotone complexity of some Boolean function. In Soviet Math. Dokl., volume 31, pages 354-357, 1985. Google Scholar
  65. Alexander Razborov. Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic. Izvestiya: mathematics, 59(1):205, 1995. Google Scholar
  66. Alexander A. Razborov. Lower bounds on the size of bounded depth circuits over a complete basis with logical addition. Mathematical Notes of the Academy of Sciences of the USSR, 41(4):333-338, 1987. Google Scholar
  67. Alexander A Razborov. Bounded arithmetic and lower bounds in boolean complexity. In Feasible Mathematics II, pages 344-386. Springer, 1995. Google Scholar
  68. Roman Smolensky. Algebraic methods in the theory of lower bounds for boolean circuit complexity. In Proceedings of the Nineteenth Annual ACM Symposium on the Theory of Computing, pages 77-82, 1987. 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
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact