4
$\begingroup$

Theorem proving is basically a turn-based game with perfect information: you start from a given gamestate (a proposition) and make moves that lead to other valid gamestates. A piece of software can check whether the moves you make are legal and whether you reached a valid solution completing the game.
That doesn't sound very different from Go, although of course the search space is much larger.

A similar game seems perfect for RL; for an algorithm like AlphaZero. We could generate an unlimited amount of theorems by combining existing ones (possibly aided by a model trained to generate interesting or difficult theorems), and train a model to solve them.

In the past years I've followed this field, and I've seen the birth of a bunch of tools (my favorite is LeanDojo), as well as a lot of research (using Lean, Metamath, Agda, Coq, as well as human-generated non-formal proofs). Nevertheless I haven't seen any noteworthy attempt at using Reinforcement Learning in combination with a theorem prover to create a powerful proving model.

I'm thus wondering whether it's feasible with today's technology to automate Theorem Proving (up to human-level) via Reinforcement Learning?

If feasible, I'd love to see some research on the problem by respectable organizations. While if it's not, I'd like to understand what the issues are: is it just because the search space is so large, or are there other challenges I can't see?

$\endgroup$
1
  • $\begingroup$ I've also wondered about this. Not a mathemetician, but math researchers probably care more about proving or disproving particular conjecture than obtaining a huge number of true statements. With that in mind, I expect it will be much harder to evaluate whether a particular state of your theorem prover is close or far to your target theorem than it will be to determine if a particular state of Go is winning or losing. Especially because those regions of state space will not have been explored in existing data (if they were, we might have proved/disproved the theorem already). $\endgroup$
    – bogovicj
    Commented Mar 16 at 15:12

0

You must log in to answer this question.

Browse other questions tagged .