Stream: Machine learning and automation

Topic: ML4PG (machine learning for proof general)


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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: May 24 2024 at 22:02 UTC