Zulip Chat Archive

Stream: Machine Learning for Theorem Proving

Topic: Paper: Automated Theorem Proving via Interacting with Pro...


view this post on Zulip Jason Rute (May 10 2020 at 12:49):

Automated Theorem Proving via Interacting with Proof Assistants by Dynamic Strategies by Guangshuai Mo, Yan Xiong, Wenchao Huang, Lu Ma

view this post on Zulip Jason Rute (May 10 2020 at 12:49):

Yet another AI for Coq!!!

view this post on Zulip Jason Rute (May 10 2020 at 12:53):

It's called SmartCoq.

view this post on Zulip Jason Rute (May 10 2020 at 12:58):

It mentions CoqGym (I don't know if it means just the ASTactic solver or if it uses the CoqGym environment). It doesn't mention ProverBot9001. (Is there something about the ProverBot9001 paper that I don't know?) I still need to look more at this paper.

view this post on Zulip Minchao Wu (May 10 2020 at 13:20):

This one looks a bit like a report of a course project or something

view this post on Zulip Minchao Wu (May 10 2020 at 13:22):

It seems that the premise selection part (what they call global arguments I believe) is not done by DQN but some fixed strategies

view this post on Zulip Minchao Wu (May 10 2020 at 13:27):

If I understand it correctly, they first generate the search tree, then use DQN to choose correct paths


Last updated: May 09 2021 at 22:13 UTC