Anyone interested in a full paper list of AI mathematics?

Stream: Machine Learning for Theorem Proving

[fzyzcjy]

Hi friends, I am considering to create and maintain a full paper list for the AI4Math area, and would like to know whether you are interested in it or have any suggestions.

Currently, there are some very helpful resources (I downloaded all papers from those lists and many thanks!), such as https://github.com/zhaoyu-li/DL4TP and https://github.com/j991222/ai4math-papers. However, it seems that they do not cover all subfields of AI mathematics. For example, I read https://arxiv.org/abs/2312.07622 to find more AI math papers and it seems some papers are not on the GitHub paper list. I guess it is because those papers are out of the scope of the existing paper lists.

The reason why I (personally) needs a full paper list is as follows. I heard several times that, if you have a research idea, then you need to carefully "blanket search" all existing papers, ensuring no one paper has done something same as you. Those papers can not only be on top conferences, but also can be hidden somewhere deep... Therefore, I guess the first step is to find all papers of AI mathematics, and read/filter them afterwards. I choose to open-source this, because I guess this may be helpful for other researchers in the AI mathematics field. Since I am new to research, it may be completely wrong (e.g. I do/should not need to do this?), and I would appreciate it for any suggestions!

My very naive thoughts to construct the list is as follows, and again would appreciate it for any suggestions!

• Scrape the metadata of all arxiv/ICML/NeurIPS/ICLR/ACL/... AI papers.
• Use regular expressions and some machine learning (probably LLM fine-tune or prompting) to find out the ones related to AI math. (The manual reading in the next step will provide data for this step's machine learning as well)
• Then, read the title/abstract of each and every paper manually as an extra filter.
• The output will be a JSON + a human-readable text, such that you can both directly read it (via text) and import it to your workflow (via JSON).

[Ralf Stephan]

You might want to do this rigorously systematically, i.e., algorithmically. See https://arxiv.org/abs/2402.08339 where I describe the Snowballing literature collection method formally (it's not complicated but was never formalized before). I also maintain a desktop app that implements Snowballing and helps with organizing: https://github.com/rwst/LitBall. Your project seems exactly to fit its use case.

[fzyzcjy]

@Ralf Stephan Thank you and that looks interesting! I wonder whether it can be used as a script/python library instead of GUI? (looks like it is kotlin compose so I guess no :( )

[Ralf Stephan]

Only if you have a second filtering step that uses abstracts and where you are confident that it nearly 100% gives you the right yes/no answer. You will still miss out on those articles where the publisher doesn't provide the abstract (I don't know the percentage in computer science but it's probably still >10%). I'm skeptical about even the best LLMs getting near the 100%.

Let me add that this filtering has to be performed probably >10^5 times, so you better have that LLM locally or some funds ready.

[fzyzcjy]

I see, thanks all the same!

[Jason Rute]

This is challenging. I've attempted it before and did a reasonable job on papers up to 2022, but then the field snowballed and there are so many papers. (I might send you a DM with my research.) Also, there are other complexities:

• There are a lot of AI for Math papers about things like adding numbers in transformers. Is this even interesting?
• There are also a lot of papers on "reasoning" in LLMs. Some are quite good. Others not so much.

• A lot of good "works" are just AITP submissions. LISA prover and the PISA dataset are from AITP.
  The results of DeepMind's Hindsight Experience Replay for Mizar are also only in AITP. But a lot of other AITP papers are just half-baked ideas that no one did any work on.

• There are papers dating back to the 90s (if not later). It is hard to know which are relevant and which are just historical curiosities.

• There are a lot of papers that don't use neural methods but still use machine learning. Hammers have some premise selection (using for example Naive Bayes). The early work of Josef Urban usually used non-neural methods. TacticToe, Tactician and others are non-nueral but quite good nonetheless.
• There are also a lot of related works like planning, robotics, and anything with the word reasoning in it. (Heck, even the field of AI for ITP and AI for ATP is very splintered.)

[Jason Rute]

Also, check out this document:

Talia Ringer said:

Yep that document! Direct link: https://docs.google.com/document/d/1kD7H4E28656ua8jOGZ934nbH2HcBLyxcRgFDduH5iQ0/edit?usp=sharing

[Jason Rute]

And this survey: #Machine Learning for Theorem Proving > A Survey on Deep Learning for Theorem Proving

[Jason Rute]

fzyzcjy said:

The reason why I (personally) needs a full paper list is as follows. I heard several times that, if you have a research idea, then you need to carefully "blanket search" all existing papers, ensuring no one paper has done something same as you.

I'm not convinced of this. It is of course good to stay up-to-date, but if someone made an obsure paper (or AITP abstract) that is similar to your idea and you miss it, then it is possible by retrying that idea you will succeed more than they did. (Very few results in this field have made much progress.) Of course, if you later find that paper, you should cite it, but I wouldn't let it stop you from getting started.

[fzyzcjy]

@Jason Rute Thank you so much for the insights! Now I see more about the difficulties...

I'm not convinced of this. It is of course good to stay up-to-date, but if someone made an obsure paper (or AITP abstract) that is similar to your idea and you miss it, then it is possible by retrying that idea you will succeed more than they did. (Very few results in this field have made much progress.) Of course, if you later find that paper, you should cite it, but I wouldn't let it stop you from getting started.

I agree. But I am worried that, if my idea and that paper's idea are quite similar, does it still have innovations? If not, then it seems to mean months' work on the idea is just wasted because someone has done it before :(

[Alex Meiburg]

fzyzcjy said:

The reason why I (personally) needs a full paper list is as follows. I heard several times that, if you have a research idea, then you need to carefully "blanket search" all existing papers, ensuring no one paper has done something same as you. Those papers can not only be on top conferences, but also can be hidden somewhere deep... Therefore, I guess the first step is to find all papers of AI mathematics, and read/filter them afterwards.

I think this is more true in some fields than others. I get the impression that biology/medicine/psychology is generally quite strict about thoroughly canvassing what's been done before. I think this in part because people care about replication, and cherry picking: it could be easy to select a few related studies that support your claim, and skip the ones with counter-evidence. And because establishing intellectual priority ends up being a big thing for patent reasons, which has bled over into standards in scientific publishing.

This is different from e.g. math, where priority is usually pretty clear (at least for anything published in the last thirty years). If you prove a theorem last year, and then this year I (unaware of your work) prove the same result... well, my work is mostly redundant, but there's no question that you proved it first. Compare this with medicine, where (say) the claim "Alzheimers is caused by an inflammatory response in glial cells" could be something that people come to believe and "prove" only over the course of forty separate studies trying to get separate circumstantial evidence. Many of those forty papers will individually claim that have ... well, they wouldn't say "proof", but that they have "strong evidence" for their claim.

[Alex Meiburg]

There have been lots of results in AI where someone took an old, 'failed' idea and tried it again with some "subtle" change that made it work splendidly. (Sometimes that change is just, "oh, we needed to run it with 100x more compute for it to get good, but then it got really good".) So I don't think that being aware of everything that has come before is a strong necessity...

[fzyzcjy]

I see, thank you very much!