Document Open Access Logo

Learning Algorithms Versus Automatability of Frege Systems

Authors Ján Pich, Rahul Santhanam

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2022.101.pdf
  • Filesize: 2.37 MB
  • 20 pages

Document Identifiers

Author Details

Ján Pich
  • University of Oxford, UK
Rahul Santhanam
  • University of Oxford, UK

Funding

  • Pich, Ján: This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodovska-Curie grant agreement No 890220. Ján Pich received support from the Royal Society University Research Fellowship URF$$1R1$$1211106.
  • Santhanam, Rahul: Rahul Santhanam is partially funded by the EPSRC New Horizons grant EP/V048201/1: "Structure versus Randomness in Algorithms and Computation".

Acknowledgements

We would like to thank Moritz Müller, Jan Krajíček, Iddo Tzameret and anonymous reviewers for comments on a draft of the paper.

Cite AsGet BibTex

Ján Pich and Rahul Santhanam. Learning Algorithms Versus Automatability of Frege Systems. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 101:1-101:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ICALP.2022.101

Abstract

We connect learning algorithms and algorithms automating proof search in propositional proof systems: for every sufficiently strong, well-behaved propositional proof system P, we prove that the following statements are equivalent, - Provable learning. P proves efficiently that p-size circuits are learnable by subexponential-size circuits over the uniform distribution with membership queries. - Provable automatability. P proves efficiently that P is automatable by non-uniform circuits on propositional formulas expressing p-size circuit lower bounds. Here, P is sufficiently strong and well-behaved if I.-III. holds: I. P p-simulates Jeřábek’s system WF (which strengthens the Extended Frege system EF by a surjective weak pigeonhole principle); II. P satisfies some basic properties of standard proof systems which p-simulate WF; III. P proves efficiently for some Boolean function h that h is hard on average for circuits of subexponential size. For example, if III. holds for P = WF, then Items 1 and 2 are equivalent for P = WF. The notion of automatability in Item 2 is slightly modified so that the automating algorithm outputs a proof of a given formula (expressing a p-size circuit lower bound) in p-time in the length of the shortest proof of a closely related but different formula (expressing an average-case subexponential-size circuit lower bound). If there is a function h ∈ NE∩ coNE which is hard on average for circuits of size 2^{n/4}, for each sufficiently big n, then there is an explicit propositional proof system P satisfying properties I.-III., i.e. the equivalence of Items 1 and 2 holds for P.

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • learning algorithms
  • automatability
  • proof complexity

Metrics

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

Related Versions

References

  1. M. Alekhnovich, M. Braverman, V. Feldman, A. R. Klivans, and T. Pitassi. Learnability and automatizability. IEEE Symposium on Foundations of Computer Science, 2004. Google Scholar
  2. B. Applebaum, B. Barak, and D. Xiao. On basing lower bounds for learning on worst-case assumptions. IEEE Symposium on Foundations of Computer Science, 2008. Google Scholar
  3. A. Atserias and M. Müller. Automating resolution is NP-hard. IEEE Symposium on Foundations of Computer Science, 2019. Google Scholar
  4. E. Binnendyk, M. Carmosino, A. Kolokolova, R. Ramyaa, and M. Sabin. Learning with distributional inverters. Algorithmic Learning Theory, 2022. Google Scholar
  5. M.L. Bonet, C. Domingo, R. Gavaldá, A. Maciel, and T. Pitassi. Non-automatizability of bounded-depth Frege proofs. Computational Complexity, 13(1-2):47-68, 2004. Google Scholar
  6. M.L. Bonet, T. Pitassi, and R. Raz. On interpolation and automatization for Frege proof systems. SIAM Journal of Computing, 29(6):1939-1967, 2000. Google Scholar
  7. S. Buss. Bounded arithmetic. Bibliopolis, 1986. Google Scholar
  8. M. Carmosino, R. Impagliazzo, V. Kabanets, and A. Kolokolova. Learning algorithms from natural proofs. IEEE Symposium on Computational Complexity, 2016. Google Scholar
  9. A. Cobham. The intrinsic computational difficulty of functions. Proceedings of the 2nd International Congress of Logic, Methodology and Philosophy of Science, 1965. Google Scholar
  10. S.A. Cook. Feasibly constructive proofs and the propositional calculus. ACM Symposium on Theory of Computing, 1975. Google Scholar
  11. S.A. Cook and N. Thapen. The strength of replacement in weak arithmetic. ACM Transactions on Computational Logic, 7(4):749-764, 2006. Google Scholar
  12. S. de Rezende, M. Göös, J. Nördstrom, T. Pitassi, R. Robere, and D. Sokolov. Automating algebraic proof systems is NP-hard. IEEE Symposium on Computational Complexity, 2020. Google Scholar
  13. M. Garlík. Failure of feasible disjunction property for k-DNF resolution and NP-hardness of automating it. Electronic Colloquium on Computational Complexity, 2020. Google Scholar
  14. M. Göös, S. Koroth, I. Mertz, and T. Pitassi. Automating cutting planes is NP-hard. ACM Symposium on Theory of Computing, 2020. Google Scholar
  15. E. Jeřábek. Dual weak pigeonhole principle, Boolean complexity and derandomization. Annals of Pure and Applied Logic, 129:1-37, 2004. Google Scholar
  16. E. Jeřábek. Weak pigeonhole principle and randomized computation. Ph.D. thesis, Charles University in Prague, 2005. Google Scholar
  17. E. Jeřábek. Approximate counting in bounded arithmetic. Journal of Symbolic Logic, 72:959-993, 2007. Google Scholar
  18. J. Krajíček. Bounded arithmetic, propositional logic, and complexity theory. Cambridge University Press, 1995. Google Scholar
  19. J. Krajíček. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. Journal of Symbolic Logic, 66(2):457-486, 1997. Google Scholar
  20. J. Krajíček. On the weak pigeonhole principle. Fundamenta Mathematicae, 170(1-3):123-140, 2001. Google Scholar
  21. J. Krajíček. Forcing with random variables and proof complexity. Cambridge University Press, 2011. Google Scholar
  22. J. Krajíček. Proof complexity. Cambridge University Press, 2019. Google Scholar
  23. J. Krajíček and P. Pudlák. Some consequences of cryptographical conjectures for S¹₂ and EF. Information and Computation, 140(1):82-94, 1998. Google Scholar
  24. J. Krajíček, P. Pudlák, and G. Takeuti. Bounded arithmetic and the polynomial hierarchy. Annals of Pure and Applied Logic, 52:143-153, 1991. Google Scholar
  25. M. Müller and J. Pich. Feasibly constructive proofs of succinct weak circuit lower bounds. Annals of Pure and Applied Logic, 2019. Google Scholar
  26. I.C. Oliveira and R. Santhanam. Conspiracies between learning algorithms, circuit lower bounds, and pseudorandomness. IEEE Symposium on Computational Complexity, 2017. Google Scholar
  27. J. Pich. Learning algorithms from circuit lower bounds. preprint, 2020. Google Scholar
  28. A.A. Razborov. On provably disjoint NP pairs. BRICS, 1994. Google Scholar
  29. A.A. Razborov. Bounded arithmetic and lower bounds in boolean complexity. Feasible Mathematics II, pages 344-386, 1995. Google Scholar
  30. A.A. Razborov. Unprovability of lower bounds on the circuit size in certain fragments of bounded arithmetic. Izvestiya of the Russian Academy of Science, 59:201-224, 1995. Google Scholar
  31. A.A. Razborov. Pseudorandom generators hard for k-DNF Resolution and Polynomial Calculus. Annals of Mathematics, 181(2):415-472, 2015. Google Scholar
  32. A.A. Razborov and S. Rudich. Natural proofs. Journal of Computer and System Sciences, 55(1):24-35, 1997. Google Scholar
  33. R. Santhanam. Pseudorandomness and the Minimum Circuit Size Problem. Innovations in Theoretical Computer Science, 2020. Google Scholar
  34. L. Valiant. A theory of the learnable. Communications of the ACM, 27, 1984. Google Scholar
  35. R. Williams. Non-uniform ACC circuit lower bounds. IEEE Symposium on Computational Complexity, 2011. 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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact