5
$\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?

Improve this question
$\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

1 Answer 1

Reset to default
1
$\begingroup$

It is feasible, even though we are at the level of high-school mathematics at the moment. But there is room for scaling. Examples are:

HyperTree Proof Search for Neural Theorem Proving (2022)

DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search (2024)

The first paper use a generalization of AlphaZero, while the second build a much more complex pipeline including supervised training, MCTS and reinforcement learning.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .