DT-Solver

Stream: Machine Learning for Theorem Proving

[Kaiyu Yang]

Just came across a new machine learning for theorem proving paper: https://aclanthology.org/2023.acl-long.706.pdf published in ACL. It looks like some improvements of HyperTree Proof Search, though I haven't read it in detail yet.

[Heather Macbeth]

Do you know what this means (from Section 4.1):

Baseline methods. ... For the Lean formal environment, besides the original GPT-f model (Polu and Sutskever, 2020), we compare our DT-Solver with PACT (Han et al., 2021) and Expert iteration (Polu et al., 2022) ... All the baseline methods are re-implemented by ourselves since none of them releases the code.

Are the authors indeed comparing their model with their own re-implementation of those other papers' models? Is that a common approach in ML research?

[Jason Rute]

Yes, it is not unheard of and very appreciated in the cases this happens.

[Heather Macbeth]

That sounds very useful. Did they make the code public? I skimmed the paper and couldn't see a link.

[Jason Rute]

Do any of the authors want to comment here? Here are the ones I could find on Zulip: @Zhengying Liu, @LIU Zhengying, @Jianhao Shen

[Kaiyu Yang]

I don't think the code is available right now (not sure if the authors plan to release it). Regarding re-implementing existing methods, yes, sometimes people do that. Depending on the specific method, re-implementing can be extremely difficult or even infeasible, due to various factors such as engineering efforts, private datasets, and the lack of details.

[Min-Hsien Weng]

I appreciate people who open source their project code. We can see how the system works, the data format, and mostly the design decisions by looking at the code. This helps us reproduce results.
@Kaiyu Yang Thank you very much for opensourcing the LeanDojo project.