Zulip Chat Archive
Stream: Machine Learning for Theorem Proving
Topic: Paper: Automated Theorem Proving via Interacting with Pro...
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
Jason Rute (May 10 2020 at 12:49):
Yet another AI for Coq!!!
Jason Rute (May 10 2020 at 12:53):
It's called SmartCoq.
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.
Minchao Wu (May 10 2020 at 13:20):
This one looks a bit like a report of a course project or something
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
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: Dec 20 2023 at 11:08 UTC