Learning algorithms versus automatability of Frege systems
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,<br> - Provable learning. P proves efficiently that p-size circu...
| Main Authors: | , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Schloss Dagstuhl - Leibniz-Zentrum für Informatik
2022
|
| _version_ | 1826308268763381760 |
|---|---|
| author | Pich, J Santhanam, R |
| author_facet | Pich, J Santhanam, R |
| author_sort | Pich, J |
| collection | OXFORD |
| description | 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,<br>
- Provable learning. P proves efficiently that p-size circuits are learnable by subexponential-size circuits over the uniform distribution with membership queries.<br>
- 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 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 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 p-size circuit lower bound) in p-time in the length of the shortest proof of a closely related but different formula (expressing an average-case subexponential-size circuit lower bound).<br>
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. |
| first_indexed | 2024-03-07T07:15:33Z |
| format | Conference item |
| id | oxford-uuid:91de963d-25ae-46f4-9e20-5e9ad8cefbab |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T07:15:33Z |
| publishDate | 2022 |
| publisher | Schloss Dagstuhl - Leibniz-Zentrum für Informatik |
| record_format | dspace |
| spelling | oxford-uuid:91de963d-25ae-46f4-9e20-5e9ad8cefbab2022-08-12T07:59:53ZLearning algorithms versus automatability of Frege systemsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:91de963d-25ae-46f4-9e20-5e9ad8cefbabEnglishSymplectic ElementsSchloss Dagstuhl - Leibniz-Zentrum für Informatik2022Pich, JSanthanam, RWe 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,<br> - Provable learning. P proves efficiently that p-size circuits are learnable by subexponential-size circuits over the uniform distribution with membership queries.<br> - 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 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 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 p-size circuit lower bound) in p-time in the length of the shortest proof of a closely related but different formula (expressing an average-case subexponential-size circuit lower bound).<br> 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. |
| spellingShingle | Pich, J Santhanam, R Learning algorithms versus automatability of Frege systems |
| title | Learning algorithms versus automatability of Frege systems |
| title_full | Learning algorithms versus automatability of Frege systems |
| title_fullStr | Learning algorithms versus automatability of Frege systems |
| title_full_unstemmed | Learning algorithms versus automatability of Frege systems |
| title_short | Learning algorithms versus automatability of Frege systems |
| title_sort | learning algorithms versus automatability of frege systems |
| work_keys_str_mv | AT pichj learningalgorithmsversusautomatabilityoffregesystems AT santhanamr learningalgorithmsversusautomatabilityoffregesystems |