Learning algorithms versus automatability of Frege systems
Ján Pich ( University of Oxford )
- 14:00 11th November 2021 ( week 5, Michaelmas Term 2021 )Lecture Theatre A, Wolfson Building
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 Jerabek’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.
If there is a function h in NE\cap 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.
This is joint work with Rahul Santhanam.
Share this:
