6

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.

nbro
  • 39,006
  • 12
  • 98
  • 176
Frank Bryce
  • 163
  • 4
  • This question seems to be very similar to https://ai.stackexchange.com/q/7416/2444 and https://ai.stackexchange.com/q/21382/2444. Can you clarify how your question is different from those? – nbro Jun 28 '20 at 20:55
  • 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. – Frank Bryce Jun 29 '20 at 02:40
  • [This answer](https://ai.stackexchange.com/a/20400/2444) seems to answer your question. If it answers your question, you should at least upvote it. – nbro Jun 29 '20 at 14:03
  • I already have, and accepted it. Thanks – Frank Bryce Jul 04 '20 at 21:04
  • 1
    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! https://www.youtube.com/watch?v=2m3zcGPKqws – k.c. sayz 'k.c sayz' Aug 20 '20 at 05:51

1 Answers1

5

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.

Zimm i48
  • 166
  • 2
  • 1
    Thanks a bunch! I found a few papers via the links you provided which is what I was looking for. – Frank Bryce Jun 28 '20 at 17:46
  • 1
    For anyone interested, [this paper](https://arxiv.org/pdf/1904.03241.pdf) 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](https://github.com/brain-research/hol-light). – Frank Bryce Jun 28 '20 at 17:59
  • An updated paper in which they don't seed their model with human proofs is [here](https://arxiv.org/pdf/1905.10501.pdf). – Frank Bryce Jun 28 '20 at 18:15