3 ms·
('Sure, it can now read and write natural language with LaTeX math and do Python programming, solving many challenging problems from elite college STEM curricul
by gwern 4y ago
('Sure, it can now read and write natural language with LaTeX math and do Python programming, solving many challenging problems from elite college STEM curricula autonomously, offline from large natural datasets, without any hand-engineering to teach it the specific algorithms, but you can't easily verify it, now can you? So overhyped.')
- yuhuai 4y agoThat's one of the future direction we're pursuing! We hope to utilize the power of autoformalization (http://arxiv.org/abs/2205.12615 http://arxiv.org/abs/2205.12615) and provably verify the solution with formal systems. As I wrote in my tweet, in the long run, I am expecting a great synergy between a strong natural language math model and an autoformalizer to tackle challenging mathematical theorems!
- visarga 4y agoMath and code can be verified, I think they can surpass human level eventually by an AlphaZero style approach. By the way, any intention to deploy this model as a math tutor?
- algo_trader 4y agonever rhe less, why arent we making even FASTER progress on formal domains? Where is the alphazero moment for LLMs + search? Either the reward space is truelly sparse. Or maybe the dataset of existing formulas is actually quite small?
- visarga 4y agoYes, reward space is sparse, they need to train on human demonstrations (same with the recent Minecraft model) to bootstrap more meaningful exploration.
- gwern 4y agoThe AlphaZero for LLMs+search is GPT-f, which most recently did https://openai.com/blog/formal-math/ https://openai.com/blog/formal-math/