[Proof Complexity] new paper

[Jan Pich]

Dear colleagues,

a new preprint, "Learning algorithms versus automatability of Frege systems", by Rahul Santhanam and myself, is available at https://users.ox.ac.uk/~coml0742/papers/learaut.pdf. Comments, corrections and suggestions are welcome.
Best wishes,
Jan Pich

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,

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. 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 ∈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.