Document

# Learning Algorithms Versus Automatability of Frege Systems

## File

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

## 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 As

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

## 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.
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.
3. A. Atserias and M. Müller. Automating resolution is NP-hard. IEEE Symposium on Foundations of Computer Science, 2019.
4. E. Binnendyk, M. Carmosino, A. Kolokolova, R. Ramyaa, and M. Sabin. Learning with distributional inverters. Algorithmic Learning Theory, 2022.
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.
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.
7. S. Buss. Bounded arithmetic. Bibliopolis, 1986.
8. M. Carmosino, R. Impagliazzo, V. Kabanets, and A. Kolokolova. Learning algorithms from natural proofs. IEEE Symposium on Computational Complexity, 2016.
9. A. Cobham. The intrinsic computational difficulty of functions. Proceedings of the 2nd International Congress of Logic, Methodology and Philosophy of Science, 1965.
10. S.A. Cook. Feasibly constructive proofs and the propositional calculus. ACM Symposium on Theory of Computing, 1975.
11. S.A. Cook and N. Thapen. The strength of replacement in weak arithmetic. ACM Transactions on Computational Logic, 7(4):749-764, 2006.
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.
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.
14. M. Göös, S. Koroth, I. Mertz, and T. Pitassi. Automating cutting planes is NP-hard. ACM Symposium on Theory of Computing, 2020.
15. E. Jeřábek. Dual weak pigeonhole principle, Boolean complexity and derandomization. Annals of Pure and Applied Logic, 129:1-37, 2004.
16. E. Jeřábek. Weak pigeonhole principle and randomized computation. Ph.D. thesis, Charles University in Prague, 2005.
17. E. Jeřábek. Approximate counting in bounded arithmetic. Journal of Symbolic Logic, 72:959-993, 2007.
18. J. Krajíček. Bounded arithmetic, propositional logic, and complexity theory. Cambridge University Press, 1995.
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.
20. J. Krajíček. On the weak pigeonhole principle. Fundamenta Mathematicae, 170(1-3):123-140, 2001.
21. J. Krajíček. Forcing with random variables and proof complexity. Cambridge University Press, 2011.
22. J. Krajíček. Proof complexity. Cambridge University Press, 2019.
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.
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.
25. M. Müller and J. Pich. Feasibly constructive proofs of succinct weak circuit lower bounds. Annals of Pure and Applied Logic, 2019.
26. I.C. Oliveira and R. Santhanam. Conspiracies between learning algorithms, circuit lower bounds, and pseudorandomness. IEEE Symposium on Computational Complexity, 2017.
27. J. Pich. Learning algorithms from circuit lower bounds. preprint, 2020.
28. A.A. Razborov. On provably disjoint NP pairs. BRICS, 1994.
29. A.A. Razborov. Bounded arithmetic and lower bounds in boolean complexity. Feasible Mathematics II, pages 344-386, 1995.
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.
31. A.A. Razborov. Pseudorandom generators hard for k-DNF Resolution and Polynomial Calculus. Annals of Mathematics, 181(2):415-472, 2015.
32. A.A. Razborov and S. Rudich. Natural proofs. Journal of Computer and System Sciences, 55(1):24-35, 1997.
33. R. Santhanam. Pseudorandomness and the Minimum Circuit Size Problem. Innovations in Theoretical Computer Science, 2020.
34. L. Valiant. A theory of the learnable. Communications of the ACM, 27, 1984.
35. R. Williams. Non-uniform ACC circuit lower bounds. IEEE Symposium on Computational Complexity, 2011.
X

Feedback for Dagstuhl Publishing