Machine learning and hammers for Coq

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 very much! :slight_smile: thank you @spitters for your response as well. :slight_smile:

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.

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.

Hi! I am curious, what are the issues? sorry I’m not a coq expert so I don’t fully understand it. Is it a coq issue or a coqgym issue?

(is it this link? Generated JSON data does not contain any link to the sources of the packages. · Issue #804 · coq/opam-coq-archive · GitHub)

It was a database issue. Coqgym pulled the urls from the wrong fields, thus leaving out many big libraries.
The databases have changed now; see above, but I don’t think coqgym has been updated to reflect that, which is a pity.

Thanks to the helpful comments here, I was able to get coquelicot running as part of the evaluation; I’ve updated the comparison page here to include coquelicot 3.2.0

I would be very interested what your tool does on the corn and math-classes libraries. They are very big complex libraries that were not included in CoqGym because of the indexing issue stated above.