3 ms·
Humans tend to put up a bit of a fight if you accuse them of producing incorrect program code; you know you're in good company if they pull-out Z3, slam out a f
by DaiPlusPlus 3y ago
Humans tend to put up a bit of a fight if you accuse them of producing incorrect program code; you know you're in good company if they pull-out Z3, slam out a few lines in their terminal keyboard, and show you rigid mathematical proof that their code is correct. LLMs don't do that.
...yet.
- lostmsu 3y agoYou can skip this above comment. GPT4 will absolutely double down when it knows it's right. The parent is clueless.
- BoorishBears 3y agoLLMs can do that with chain of thought in a way that generalized to multiple tasks
- DaiPlusPlus 3y agoOnly in a vague way. Even with train-of-thought, feedback loops, and other neat tricks, I've never seen an LLM produce valid theorems for Z3 (beyond trivial examples).