Has anybody used ML4PG and wants to comment on it? There is a Github for it but it has not been updated in a few years. Did anyone find it helpful? I don't understand exactly the information it provides to the user.
I think they were the first to perform learning on Coq proof terms. I never used it, but we compared to ML4PG in related work section of our paper that used Coq terms via SerAPI.
the PG-based toolchain is in my view obsolete by now, but the ML parts could probably be repurposed on top of SerAPI or Coq-lsp
That makes sense. I haven't looked into the internals but working with SerAPI it might be easier to rewrite it in Python, now that Python is so widely used in machine learning tasks.
you could probably interface with coq-lsp from Python, or use SerAPI's toplevel from Python (see Proverbot9001), or use pycoq (https://github.com/ejgallego/pycoq)
Last updated: Nov 29 2023 at 21:01 UTC