3 ms·
Now if we can get LLMs to do that, they might code better. Proofs are a lot of work, but might keep LLMs on track.
by Animats 1y ago
Now if we can get LLMs to do that, they might code better. Proofs are a lot of work, but might keep LLMs on track.
- mprast 1y agoI was thinking the same thing!
- Nevermark 1y agoIn any other industry the “worker class” would be sabotaging the machines. In the merry software world, the challenges of improving our potential replacements are far too interesting and satisfying to leave room for any worry about consequences! :)
- bcheung 1y agoThe problem is the training corpus tends towards mediocre code. But with an agentic loop that analyzes the code against those criteria and suggests changes then I think it might be possible. I wouldn't try to get it to generate that right off the bat.
- AIPedant 1y agoMost proof assistants do a good job with autogenerating a (deterministically correct) proof given a careful description of the theorem. Working on integrating this into mainstream languages seems much more worthwhile than training an LLM to output maybe-correct proof-seeming bits of text.
- purplesyringa 1y agoIME, LLMs are completely incapable of reasoning about anything remotely difficult. All you'll get are proofs by assertion, not anything rigid you can trust.