Live data from Hacker News

Transformers are inherently succinct

openreview.net

21–30 of 46 posts

Re: Transformers are inherently succinct

#21
post #5

I had no idea that LLMs (or the transformer architecture) were within reach of complexity theory. But if transformers "can be" exponentially more succinct than RNNs, doesn't that mean we're approaching optimality?

No. We have an infinitely more succinct formalism, it's Turing machines. Succinctness is not necessarily a desirable property, it just says where on the capability-tractability tradeoff something is. Turing machines can express literally anything computable, but in exchange we can't use computers to reason about them in general (Rice's Theorem). Regexes are much more limited, they famously can't even recognize HTML, but we get to automatically prove things about them.

Re: Transformers are inherently succinct

#22

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.

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

Re: Transformers are inherently succinct

#23
post #11

My comment in the previous discussion of that paper: https://news.ycombinator.com/item?id=48014197 Authors used LTL (linear temporal logic) to express, basically, non-reduced non-ordered binary decision diagrams. Or just binary decision diagrams, BDDs. BDDs are almost guaranteed to have exponential size because they do not employ reduction (sharing of common expressions). Reduced BDDs are more succinct and reduced or…

Thank you for the explanation, makes it a lot more digestible

Just nit picking a bit:

> Training any model to express some truth table is very hard

What kind of models are you including here? Truth tables can be modeled in regular code very easily and reliably. And I’m sure there are many deterministic models that could do the same. Are you talking about LLMs in particular or a certain category/type of models?

Re: Transformers are inherently succinct

#24
post #11

My comment in the previous discussion of that paper: https://news.ycombinator.com/item?id=48014197 Authors used LTL (linear temporal logic) to express, basically, non-reduced non-ordered binary decision diagrams. Or just binary decision diagrams, BDDs. BDDs are almost guaranteed to have exponential size because they do not employ reduction (sharing of common expressions). Reduced BDDs are more succinct and reduced or…

What?

Reduced Ordered BDDs are likely not as succinct as an arbitrary BDD.

The famous Hidden Weight Bit problem can be more succinctly expressed in arbitrary BDDs (changing the order and revisiting nodes), but are provably EXPSPACE in ROBDDs.

-------

We study ROBDDs because they uniquely reduce to a canonical form. All functions have exactly one (!!!!) ROBDD.

BDDs in general however are really arbitrary, as arbitrary as any codebase can basically get. That makes BDDs in general to difficult to study or do math upon.

Results based on the studies of arbitrary BDDs do NOT apply to the simpler, easier to understand world of ROBDDs. And vice versa.

Re: Transformers are inherently succinct

#25

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.

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

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.

Re: Transformers are inherently succinct

#26
post #7

Paper went over my head but is this in any way related to my experience of Claude Opus 4.8 using increasingly terse language with very short, overloaded words? Lately I've been having trouble parsing the things it writes about my own code, it's using the kind of compressed language that you see typically in git commit message subject lines but relentless, always on.

That's a budget thing. Claude is suffering from huge demand and they're pulling out all the stops to try to keep the lights on: terse tokens, lobotomizing Claude six ways from Sunday, aggressive batching, the works.

Re: Transformers are inherently succinct

#27

Earlier quoted context omitted.

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

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.

That's saying you can't formally verify an LLM, not that LLMs can't be used in formal verification.

Re: Transformers are inherently succinct

#28
post #14
post #5

I had no idea that LLMs (or the transformer architecture) were within reach of complexity theory. But if transformers "can be" exponentially more succinct than RNNs, doesn't that mean we're approaching optimality?

> doesn't that mean we're approaching optimality? No. Transformers are Markov chains [1]. Somewhere around this fascinating site [2] I read that stateful models have an advantage. Author provided an example, a state machine with two states A and B, where at state A transitions are to state A (output 0) and to state B (output 1) with equal probability and at state B the transition is always to state A and output is al…

Huh? Any process on a computer by itself is also a Markov chain.

If you include all the information the LLM uses to produce the next token as part of the state, then of course the LLM is a Markov chain.

So would be any other process for sampling continuations of a text, with finite memory.

Re: Transformers are inherently succinct

#30

Earlier quoted context omitted.

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.

That's saying you can't formally verify an LLM, not that LLMs can't be used in formal verification.

[deleted]
Post reply on HN