3 ms·
A key aspect in AlphaProof was how to find good training problems. For AlphaProof they managed to scrape 1 million "International Mathematical Olympiad (IMO) st
by thomasahle 2y ago
A key aspect in AlphaProof was how to find good training problems. For AlphaProof they managed to scrape 1 million "International Mathematical Olympiad (IMO) style" problems.
Here Bengio seems to just suggest using estimated entropy `E_P(t|T(S))[− log P(t | T(S))]` of the theorem to find interesting/surprising theorems to try and prove.
This reminds me of the early work in estimating LLM uncertainty/hallucinations using perplexity. It didn't work very well.
Actually generating good "exercises" for the system to "practice" on, and theorems to try and prove, still seems like the biggest road block for an AI mathematician.
It connects to the philosophical question of why we are doing math in the first place?
- nickpsecurity 2y agoThis might be where expert-crafted, training data comes in. I previously proposed training them like children with K-12 resources, games, stories, and exercises. Maybe add math tutoring with formal proofs at different levels. Then, let them generate many types of problems themselves, have experts correct them, and further train on that.
- thomasahle 2y agoExpert-crafted, training data is great. But it won't take you above human expert level. If you are truly trying to make an "AI mathematician" it has to be able to propose it's own problems to solve.
- nickpsecurity 2y agoI think being able to do that is itself a skill we might be able to teach with the right data. Also, the training data I mentioned could be produced partly by programs that generate such examples. The templates for them could be made from human exercises. There’s already tools that generate test data from grammars or algebraic rules. Maybe encode which math problems can be mixed together using those.