Learning algorithms versus automatability of Frege systems
Ján Pich, Rahul Santhanam · Journal of Mathematical Logic · 2024
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, (1) Provable learning. P proves efficiently that p-size circuits are learnable by subexponential-size circuits over the uniform distribution with membership queries. (2) 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. hold: 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 [Formula: see text], then Items 1 and 2 are equivalent for [Formula: see text]. We use the following modified notion of automatability in Item 2, the automating circuits output a P-proof of a given formula (expressing a p-size circuit lower bound for a function f) in non-uniform p-time in the length of a shortest P-proof of a closely related but different formula (expressing an average-case subexponential-size circuit lower bound for the same function f). If there is a function [Formula: see text] which is hard on average for circuits of size [Formula: see text], 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.