Domains for controlled AI setups

Stream: Machine Learning for Theorem Proving

[Ayush Agrawal]

I have been working on AI4Math related areas for sometime. There is one question that I always struggle with: finding the right domain to work on problems such as library learning, conjecturing, discovery etc. Benchmarks such as Putnambench are available but I think they are more suitable for advancing theorem proving and not for the areas I mentioned above. For small scale demonstrations, ideally we use 7B pretrained models. The domains should not be too trivial and also should not be too hard if one needs to see "signs of life". Also, one also needs to think about the background formalisation available such that it should not be very less. Any advice on this would be helpful!

[Gerben Koopman]

Do I understand it right that you're looking for a maths domain that might be suitable for LLMs? Because library learning, conjecturing, etc are new to me, though it looks very interesting, so I'm not sure I parse the question right.

[Ayush Agrawal]

Yes exactly, if the question is still unclear, plz let me know.