# Learning algorithms versus automatability of Frege systems

arXiv: https://arxiv.org/abs/2111.10626 · HTML: https://mlsanity.com/paper/2111.10626/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 2 of its 43 references that are in the map.
- First posted on arXiv 20 Nov 2021.

## Builds on (most cited first, 2 of 2)

- [Conspiracies between Learning Algorithms, Circuit Lower Bounds and Pseudorandomness](https://mlsanity.com/paper/1611.01190/) (2016)
- [Automating Resolution is NP-Hard](https://mlsanity.com/paper/1904.02991/) (2019)

## Abstract (arXiv)

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 Jevr'abek'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∈ NEcap coNE which is hard on average for circuits of size 2n/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.