6
$\begingroup$

Coq exists, and there are other similar projects out there. Further, Reinforcement Learning has made splashes in the domain of playing games (a la Deepmind & OpenAI and other less well-known efforts).

It seems to me that these two domains deserve to be married such that machine learning agents try to solve mathematical theorems. Does anyone know of any efforts in this area?

I'm a relative novice in both of these domains, but I'm proficient enough at both to take a stab at building a basic theorem solver myself and trying to make a simple agent have a go at solving some basic number theory problems. When I went to look for prior art in the area I was very surprised to find none. I'm coming here as an attempt to broaden my search space.

Improve this question
$\endgroup$
5
  • $\begingroup$ This question seems to be very similar to ai.stackexchange.com/q/7416/2444 and ai.stackexchange.com/q/21382/2444. Can you clarify how your question is different from those? $\endgroup$
    – nbro
    Commented Jun 28, 2020 at 20:55
  • $\begingroup$ well, I found those questions and they didn't really answer what I was looking for. Reading the answers, they were answering much different parts of the question. They are more interested in "is this possible? and if so, how?" and I'm more wondering about prior efforts to do this so I don't have to start from scratch. The answer given was pretty much perfect for me, so I'm glad it worked out. $\endgroup$
    – Frank Bryce
    Commented Jun 29, 2020 at 2:40
  • $\begingroup$ This answer seems to answer your question. If it answers your question, you should at least upvote it. $\endgroup$
    – nbro
    Commented Jun 29, 2020 at 14:03
  • $\begingroup$ I already have, and accepted it. Thanks $\endgroup$
    – Frank Bryce
    Commented Jul 4, 2020 at 21:04
  • 1
    $\begingroup$ i'm just going to leave this here: i hesitate to submit it as an answer since i am not in a position to evaluate the talk, but there is evidence that people are working on it! youtube.com/watch?v=2m3zcGPKqws $\endgroup$
    – k.c. sayz 'k.c sayz'
    Commented Aug 20, 2020 at 5:51

1 Answer 1

Reset to default
5
$\begingroup$

Artificial Intelligence for Theorem Proving is an active research area as witnessed by the existence of the AITP conference and of many publications on the topic. Some papers are mentioned in this thread: https://coq.discourse.group/t/machine-learning-and-hammers-for-coq/303. I haven't read these papers myself, so I cannot point you to a paper using reinforcement learning specifically, but given the important activity in this domain, I would be very surprised if it hadn't been attempted.

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ Thanks a bunch! I found a few papers via the links you provided which is what I was looking for. $\endgroup$
    – Frank Bryce
    Commented Jun 28, 2020 at 17:46
  • 1
    $\begingroup$ For anyone interested, this paper is essentially what I was looking for. It has a benchmark, a.k.a. theorems that ought to be proved by the "theorem solver" with success rates for a few architectures they tried out. It also has an environment integration with an existing theorem solver "HOL Light" to build your own RI models against. The repository linked in their paper is here. $\endgroup$
    – Frank Bryce
    Commented Jun 28, 2020 at 17:59
  • $\begingroup$ An updated paper in which they don't seed their model with human proofs is here. $\endgroup$
    – Frank Bryce
    Commented Jun 28, 2020 at 18:15

You must log in to answer this question.

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