2 ms·
Isn't formal analysis exactly the kind of thing LLMs can't do at all? Or do you mean an LLM invoking a proof assistant or something like that?
by pxc 1y ago
Isn't formal analysis exactly the kind of thing LLMs can't do at all? Or do you mean an LLM invoking a proof assistant or something like that?
- tptacek 1y agoYes, I mean LLMs generating proof specs and invoking assistants, not that they themselves do any formal modeling.