Transformers are inherently succinct

> 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.

  > What kind of models are you including here?

The truth tables? Predict zeroth bit in enwik9 from, say, bits of 64 previous bytes. Or multiply two 16 bit numbers and predict bit 16 of the multiplication result.

Ingo Wegener's "Branching Programs and Binary Decision Diagrams" copyright year 2000, is considered the introductory work on all BDD related matters. On the front cover are two BDDs: BOTH of these implement the hidden weighted bit function (HWB-4) introduced in the first chapter, and is basically the main example used throughout the whole book.

Please locate a copy of the front cover ASAP, before continuing with my post.

-----------

Now that you've found the book cover, look at it carefully and understand the HWB-4 function. (Just traverse it by hand, dotted lines represent "x1 == 0", while solid lines represent "x1 == 1").

Both BDDs fail to be ROBDDs: the left diagram explores the variables in this order: x1, x2, x3, x4, and then (depending on path), x1/x2/x3. That is, the variables x1/x2/x3 are explored _TWICE_ (breaking the rule for ROBDDs).

The example on the right also fails to be a ROBDD. The variable orderings are seemingly random: one branch covers x4, x1, x2, x3. The other branch is x4, x3, x1, x2. This fails the "ordered" property as the different branches cover different orderings.

BOTH are BDDs however. Both clearly implement the HWB-4 function efficiently (less than EXP-space. Indeed, its a very small graph for the front cover of a book). If these were actually ROBDDs, they'd be ridiculously large and unable to fit.

-------

ROBDDs are again, studied due to the unique property (and proof), that for any given function, there can only be one ROBDD ever generated (!!!!). For the verification problem of circuits, this is extremely useful. Different circuits might implement the same function, despite one circuit being smaller or using less power (or other useful properties).

To "prove" that the circuits output the same function, you simply create an ROBDD. Because functions ALWAYS result with the same ROBDD, you can ALWAYS use this process to prove circuit equivalence.

ROBDDs aren't succinct. No: their usefulness is the opposite. Exactly one ROBDD to ever find for any binary function that has ever existed or will ever exist.

Edit: Actually nevermind. If UHAT could be compiled into LTL w/ polynomial overhead then that would also work for the languages that have exponential overhead in LTL but since they don't there is a strict separation.

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.