3 ms·
I've had extremely poor results attempting to get current LLMs to generate proofs, for code or otherwise.
by AlotOfReading 4y ago
I've had extremely poor results attempting to get current LLMs to generate proofs, for code or otherwise.
- ogogmad 4y agoCombining it with AutoGPT (or the ideas it's based on) and a formal prover like Lean might be the answer. Have you tried? Basically, if you don't allow GPT to iteratively write, execute, criticise and then correct its code, you won't get good results.
- rqtwteye 4y agoI think it probably needs to be a specialized combination of LLM and hardcoded knowledge.