4 ms·
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 e
by dfabulich 4mo 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 4mo agoThat's saying you can't formally verify an LLM, not that LLMs can't be used in formal verification.
- deleted 4mo ago[deleted]
- nextos 4mo agoBut, 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.
- _0ffh 4mo agoGood news! On the current trajectory, I am very hopeful nonlinear RNNs could make a comeback. Which would incidentally help to ease the memory pressure for inference tasks.