search

albertqjiang / INT

Official code for paper: INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving
MIT License
36 stars 5 forks source link

(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`? #3

Open fzyzcjy opened 1 year ago

fzyzcjy commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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

fzyzcjy commented 1 year ago

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 commented 1 year ago

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

fzyzcjy commented 1 year ago

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