Abstract
We connect learning algorithms and algorithms automating proof search in propositional proof systems: for every sufficiently strong, wellbehaved propositional proof system P, we prove that the following statements are equivalent,
 Provable learning. P proves efficiently that psize circuits are learnable by subexponentialsize circuits over the uniform distribution with membership queries.
 Provable automatability. P proves efficiently that P is automatable by nonuniform circuits on propositional formulas expressing psize circuit lower bounds. Here, P is sufficiently strong and wellbehaved if I.III. holds: I. P psimulates 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 psimulate 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 psize circuit lower bound) in ptime in the length of the shortest proof of a closely related but different formula (expressing an averagecase subexponentialsize 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.
BibTeX  Entry
@InProceedings{pich_et_al:LIPIcs.ICALP.2022.101,
author = {Pich, J\'{a}n and Santhanam, Rahul},
title = {{Learning Algorithms Versus Automatability of Frege Systems}},
booktitle = {49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
pages = {101:1101:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959772358},
ISSN = {18688969},
year = {2022},
volume = {229},
editor = {Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16442},
URN = {urn:nbn:de:0030drops164427},
doi = {10.4230/LIPIcs.ICALP.2022.101},
annote = {Keywords: learning algorithms, automatability, proof complexity}
}
Keywords: 

learning algorithms, automatability, proof complexity 
Collection: 

49th International Colloquium on Automata, Languages, and Programming (ICALP 2022) 
Issue Date: 

2022 
Date of publication: 

28.06.2022 