2 ms·
Of course they are. LLMs are routinely used to generate Lean proofs, so of course they can also be used to generate verified software. They probably aren't bein
by naasking 5mo ago
Of course they are. LLMs are routinely used to generate Lean proofs, so of course they can also be used to generate verified software. They probably aren't being used that way, yet, but they will be:
* A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants, https://arxiv.org/abs/2508.18587v1 https://arxiv.org/abs/2508.18587v1
* CoqPilot, a plugin for LLM-based generation of proofs, https://dl.acm.org/doi/10.1145/3691620.3695357 https://dl.acm.org/doi/10.1145/3691620.3695357