| ▲ | dfabulich 5 hours ago | |||||||||||||
It's the last line of the abstract. > As a consequence of this succinctness, we show that basic verification problems for transformers, such as emptiness and equivalence, are provably intractable: specifically, EXPSPACE-complete. | ||||||||||||||
| ▲ | platinumrad 4 hours ago | parent [-] | |||||||||||||
That's saying you can't formally verify an LLM, not that LLMs can't be used in formal verification. | ||||||||||||||
| ||||||||||||||