(Willing to PR) Enhance `INT` by features of `Equations` from `HyperTree Proof Search for Neural Theorem Proving`, and extra inequalities from `Formal Mathematics Statement Curriculum Learning`?

[fzyzcjy]

Hi, thank you for the wonderful INT dataset and environment! Recently, there is a paper https://arxiv.org/abs/2205.11491 which also contains a simple environment, Equations (mainly see chapter 3, 7.1.3, and appendix B of the paper). (I guess I do not need to introduce more about the paper, since you are supervised by Lample and he seems to be the author of that paper as well ;))

Since the Equations environment is not open sourced, and the INT looks quite promising and extensible, I wonder whether it is possible to extend INT with more features mentioned in Equations?

I am willing to make a PR! (As can be seen from my homepage, I created several open-source libraries and made dozens of PR to Google Flutter)

[albertqjiang]

Thanks for the issue! I'm happy to merge PRs!

From HTPS, since their equations do not have to have a graph representation and everything is a string, the generation process can be further simplified (by a lot). I think that'd be the best way to go.

[fzyzcjy]

Thanks!

do not have to have a graph representation and everything is a string, the generation process can be further simplified (by a lot). I think that'd be the best way to go.

Sorry do not quite get it. IMHO the internal representation has to be an AST instead of a raw String?

[albertqjiang]

Ah yes, I guess I meant that there's certainly room for improvement when implementing new stuff! I made quite a clunky implementation doing the generation. With proper pattern matching etc. it should be easier to generate ASTs going forward.

[fzyzcjy]

@albertqjiang Thank you! I will dig more into the codebase and report more thoughts here.

[fzyzcjy]

Update: When reading Formal Mathematics Statement Curriculum Learning (chapter 5, appendix D), seems that they also do some updates to INT. For example, they support Cauchy and many inequalities, as well as porting to Lean.

By the way, seems that one author, Mantas Baksys, is also from Cambridge. So is it possible they open-source and PR to this library for their changes? I have long been in the open-source community and is new to neural theorem prover field, so feels a bit weird to see people not open-sourcing things, especially when they base their work on an open-source lib :/

[albertqjiang]

I don't think they could because it's most likely that OpenAI owns the code for that.

[fzyzcjy]

I see. Sad to see "open" AI is so "closed" (though they were already closed given the GPT3 event) :/