Reinforcement Learning of Theorem Proving

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F18%3A00329352" target="_blank" >RIV/68407700:21730/18:00329352 - isvavai.cz</a>

Result on the web

<a href="https://papers.nips.cc/paper/8098-reinforcement-learning-of-theorem-proving" target="_blank" >https://papers.nips.cc/paper/8098-reinforcement-learning-of-theorem-proving</a>

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Reinforcement Learning of Theorem Proving

Original language description

We introduce a theorem proving algorithm that uses practically no domain heuristic for guiding its connection-style proof search. Instead, it runs many Monte-Carlo simulations guided by reinforcement learning from previous proof attempts. We produce several versions of the prover, parameterized by different learning and guiding algorithms. The strongest version of the system is trained on a large corpus of mathematical problems and evaluated on previously unseen problems. The trained system solves within the same number of inferences over 40% more problems than a baseline prover, which is an unusually high improvement in this hard AI domain. To our knowledge this is the first time reinforcement learning has been convincingly applied to solving general mathematical problems on a large scale.

Czech name

—

Czech description

—

Type

O - Miscellaneous

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

<a href="/en/project/EF15_003%2F0000466" target="_blank" >EF15_003/0000466: Artificial Intelligence and Reasoning</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2018

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů