4 ms·
I seriously doubt mochi's going to be any help for the lean formalization effort. But a lean-assistive llm trained on mochi's work? Ahhh! What an intriguing po
by barfbagginus 2y ago
I seriously doubt mochi's going to be any help for the lean formalization effort.
But a lean-assistive llm trained on mochi's work? Ahhh! What an intriguing possibility!
- Chinjut 2y agoI do not imagine LLMs will be of any use here.
- barfbagginus 2y agoThen it's time to update your LLM reading! https://leandojo.org/ https://leandojo.org/ https://github.com/lean-dojo/LeanCopilot https://github.com/lean-dojo/LeanCopilot https://arxiv.org/abs/2404.07382 https://arxiv.org/abs/2404.07382
- Davidzheng 2y agoThese llm's are usually only proving some trivial lemmas right now. Hopefully it changes soon but...
- barfbagginus 2y agoJust bolting llms onto proof search improves the state of the art. So if you want to improve the state of the art of proof search, bolt some llms onto proof search, and enjoy! As far as making LLMs understand mochi math... I'm going to go out on a limb and say it will probably take less time for us to build an AI that understands mochi than it would take to understand mochi ourselves.
- dimask 2y agoI would bet for this use case LLMs to be worse than random walk, as they would probably disregard certain possibilities in crucial steps, unless we are talking about easier stuff.
- barfbagginus 2y agoLLMs are just fancy adaptive random walks, and they tend to pick more novel candidates, not less. To wit, proof search has done random walks for ages. But proof search accelerated with LLM oracles is pushing the state of the art for automated proof search. The progress isn't insane or miraculous. But it's moving the needle in an otherwise somewhat stagnant area. And that means we need to pay attention and update our beliefs and working theories.