This is a truly important paper. It formalizes the intuition that many in the field have. We can stop wasting time doing formal analysis of LLMs. If you have a problem that requires formal verification, don't use an LLM. You can use an LLM to help you build such a system, but the LLM can't be the system.

▲

AlotOfReading 3 hours ago | parent | next [-]

I'm not sure that's a great takeaway. Lots of problems are undecidable and have reasonably effective solutions in practice (e.g. finding bugs -> testing, static analysis, etc). Mind you, I don't expect we'll find anything like that for transformers, but there's a surprisingly large gap between what's possible in general and what's possible in the cases we care about.

▲

suddenlybananas 5 hours ago | parent | prev [-]

I don't really see the relationship to your comment and the paper's content. Could you elaborate a little?

▲

dfabulich 5 hours ago | parent [-]

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.

	▲	nextos 2 hours ago \| parent \| next [-]
		But, if I have understood correctly on a quick read, they also claim transformers have pretty low expressive power. In particular, they claim they are limited to star-free subregular languages, whereas RNNs can recognize any regular language/simulate finite automata. This doesn't imply you can't get aid from a LLM to e.g. implement a function that has a formal specification (an application I think is very promising), but surely it has some profound implications on how much of a large system can be understood by a LLM at once, without supervision.
	▲	4 hours ago \| parent \| prev [-]
		[deleted]