In the paper

Prolog Technology Reinforcement Learning Prover (System Description)

https://link.springer.com/chapter/10.1007/978-3-030-51054-1_33

by Zombori, Urban and Brown, they describe their successful implementation of a Monte Carlo tree search algorithm for proofs in the connection tableau calculus. They argue that Prolog is a very natural setting for implementing this kind of algorithm.

Abstract. We present a reinforcement learning toolkit for experiments

with guiding automated theorem proving in the connection calculus. The

core of the toolkit is a compact and easy to extend Prolog-based auto-

mated theorem prover called plCoP. plCoP builds on the leanCoP Prolog

implementation and adds learning-guided Monte-Carlo Tree Search as

done in the rlCoP system. Other components include a Python inter-

face to plCoP and machine learners, and an external proof checker that

verifies the validity of plCoP proofs. The toolkit is evaluated on two

benchmarks and we demonstrate its extendability by two additions: (1)

guidance is extended to reduction steps and (2) the standard leanCoP

calculus is extended with rewrite steps and their learned guidance. We

argue that the Prolog setting is suitable for combining statistical and

symbolic learning methods. The complete toolkit is publicly released.

I am wondering if it would be realistic to implement an interface like this for Elpi. Of course Elpi is not really itself designed for statistical analysis or machine learning tasks, but would it be reasonable to expose some kind of interface between Elpi and Ocaml or Python for the sake of letting a sophisticated deep-learning algorithm control what step is chosen in proof search?

I have noticed that very many papers in automated theorem proving nowadays are of the form "We used Monte Carlo tree search and used a neural network to predict what branch to take at each step of the search." I think if you could to write a tree search in Elpi that took some guidance from an external source on how to prove theorems, it would be really interesting. I'd like to try it, at least.

Hello.

I am not sure this is the feature you are looking for, but as Elpi is implemented in OCaml, any predicate can be implemented directly in OCaml. In Coq-Elpi, this is done for the `coq.*`

predicates interacting with Coq at a lower level.

If this is what you want, this file in the documentation of Elpi can help you. You basically have to declare your predicates wrapping your implementation in Elpi internal constructors (`MLCode`

, `Pred`

, ...), giving information about the predicate mode (`In`

, `Out`

, ...), the depth of context it requires (`Easy`

, `Full`

, ...), etc. Then the few lines at the end of the file (calls to the `API`

module) load your OCaml code as additional built-ins in the Elpi instance you run, then load your Elpi code and run it.

I concur with Enzo that the simplest way to try it out would be to bind some external APIs, and guard rules with calls to the oracle

```
search Goal Solution :- call-oracle Goal BranchToTake, search-branch BranchToTake Goal Solution.
search-branch 1 Goal Solution :- ... search SubGoal SubSolution ...
search-branch 2 Goal Solution :- ... ....
```

where call-oracle is an external API which decides which branch to take based on Goal and "magic".

disclaimer: I did not read the paper above

Last updated: Jun 06 2023 at 22:01 UTC