3 ms·
That's saying you can't formally verify an LLM, not that LLMs can't be used in formal verification.
by platinumrad 4mo ago
That'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.