3
$\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.

$\endgroup$
  • $\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 Jun 28 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 Jun 29 at 2:40
  • $\begingroup$ This answer seems to answer your question. If it answers your question, you should at least upvote it. $\endgroup$ – nbro Jun 29 at 14:03
  • $\begingroup$ I already have, and accepted it. Thanks $\endgroup$ – Frank Bryce Jul 4 at 21:04
  • $\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' Aug 20 at 5:51
3
$\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$
  • 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 Jun 28 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 Jun 28 at 17:59
  • $\begingroup$ An updated paper in which they don't seed their model with human proofs is here. $\endgroup$ – Frank Bryce Jun 28 at 18:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.