Patrick Nicodemus (Mar 09 2023 at 05:46): Patrick Nicodemus (Mar 09 2023 at 05:46):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.
Enzo Crance (Mar 09 2023 at 07:40):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.
Enrico Tassi (Mar 09 2023 at 09:47):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".
Enrico Tassi (Mar 09 2023 at 12:44):disclaimer: I did not read the paper above
Last updated: Oct 13 2024 at 01:02 UTC