Patrick Nicodemus (Mar 28 2023 at 11:55): Patrick Nicodemus (Mar 28 2023 at 11:55):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.
Karl Palmskog (Mar 28 2023 at 12:07):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.
Karl Palmskog (Mar 28 2023 at 12:09):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
Patrick Nicodemus (Mar 28 2023 at 14:31):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.
Karl Palmskog (Mar 28 2023 at 15:03):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: Oct 13 2024 at 01:02 UTC