Here is one more paper that describes a (deep) learning approach for Coq proof automation. The code for the project, called Proverbot9001, is available on GitHub.
1 Like
Note also that CoqHammer is out for Coq 8.10 (also via OPAM), and the continuously updated Coq OPAM JSON file should have all the data needed to install/process a project from the Coq OPAM repository.
In other words, I think the stage is nearly set for a comparison of automation techniques for Coq 8.10.
@ejgallego @maximedenes I’d be interested in contributing to the development of such API for Machine Learning applications.
Why is building a Python API for SerAPI not good enough? or are there additional hurdles? @ejgallego
Another option could be having OCaml have access to Deep Learning frameworks? Would that help?
related link: https://discuss.ocaml.org/t/is-it-possible-to-use-machine-learning-and-deep-learning-frameworks-through-ocaml/4570
Does anyone know if the HOL Light interface provided by google is any easier to use than Coq? Anyone knows the advantages and disadvantages?
Here’s a nice benchmark suite for lean:
3 Likes
Some interesting progress on sauto/coqhammer by Łukasz Czajka. It would be good to have a some more uniform benchmarks.
Note the linked paper is a submitted version before the review, which I’m going to update substantially taking into account the reviews.
Hi. May i ask if there is any machine learning tool that works well in predicting and using ssreflect tactics for proofs in Coq? From what I have found, most of the tools mentioned that they do not work well with ssreflect. Are there tools that we can use to train with ssreflect/mathcomp library?
CoqHammer has some limited support for MathComp and proofs by reflection out of the box, see the website. However, for arithmetic goals, it’s possible to escape from the MathComp world via mczify. The idea is to first canonize a MathComp arithmetic goal via the zify tactic, and then apply the hammer tactic on the resulting goal (assuming lia with mczify doesn’t do the job directly).
2 Likes
thank you note CoqGym has it’s own discussion forum (and gitissues), that might be a better place to direct your questions about CoqGym and related topics to that project: https://github.com/princeton-vl/CoqGym/discussions
1 Like
Hey all, Alex Sanchez-Stern here, author of Proverbot9001 (which @palmskog graciously mentioned earlier in the thread). My team just put together an extended evaluation which compares our work to CoqGym’s model (ASTactic) and another more recent system by some folks from UMass Amherst (shout out to Emily First, Yuriy Brun, and Arjun Guha), TacTok. You can check it out here. Gist of it is, on the CoqGym benchmarks, we can automatically produce significantly more proofs than both tools combined!
More specifically for the topic of conversation here, our system is built without modifying Coq at all, and currently works out-of-the-box for Coq 8.9, 8.10, 8.11, and 8.12. We do this through a custom python module which launches a Serapi instance, and communicates to it through standard in and out. This has the advantage of allowing us to work on many Coq versions, and not requiring any custom building, but it can be kind of brittle at times; support for a more stable python API would be awesome, but I’m also happy to help anyone use/extend the one we’ve built.
Very nice!
The CoqGym was a bit restricted due to the problems mentioned here. Has this been addressed?
Also, you’re comment ““coquelicot” Failed (needs Coq 8.7)” seems surprising.
Yeah, I was a little surprised too, but their webpage says that 8.7 is the latest supported version, and I wasn’t able to get it to build on 8.9/8.10 at all.
As for the CoqGym issues stated, I’m not sure if we’ve addressed them, but I think that Proverbot9001 has a different approach to extracting data which might make those issues moot, or at least less of a problem. With CoqGym, there is an instrumented version of Coq, run by the authors on the projects to be used, producing a canonical set of json data. Users are expected to download and work with this data, so it’s useful for it to have a direct connection to the Coq source from which it was extracted. With Proverbot9001 however, there is no canonical extracted dataset; Proverbot9001 runs directly on uninstrumented Coq, and the user can extract data directly from any Coq source file that they can build (command line options specify a prelude directory where the _CoqProject file is sourced). Therefore, when they have extracted data, it should correspond to source files that they have directly in front of them, so there is less of a need for some other direct connection.
However, I imagine that some users would want to be able to emulate the CoqGym approach in the future, so if someone ends up doing that, and wants the ability to embed metadata in the extracted proofs which points to a git repo, I’m happy to add that support.
The coquelicot website is outdated:
http://coq.io/opam/coq-coquelicot.3.2.0.html
The observation about CoqGym is more that their database is skewed, and may not be a good benchmark.
1 Like
As pointed out by Bas, the website is outdated. (That is kind of the issue with institutional websites on which you do not have complete control.) That said, if you actually follow the link “download the latest version”, you will get Coquelicot 3.2.0, which supports all versions of Coq from 8.8 to now.
If you need a version of Coquelicot that supports Coq 8.7, you can use Coquelicot 3.0.2 (or 3.0.1). If you are using Opam, it will automatically take care of choosing a version of Coquelicot compatible with your version Coq.
Ah, great! I’ll use the source from the opam page to build, and update the results graph webpage when it finishes running.