46 ms·
We connect and strengthen these results by identifying a variant of first-order logic with counting quantifiers that is simultaneously an upper bound for fixed-
by sharemywin 4y ago
We connect and strengthen these results by identifying a variant of first-order logic with counting quantifiers that is simultaneously an upper bound for fixed-precision transformer encoders and a lower bound for transformer encoders.
not sure what a fixed precision transformer is?
- eutectic 4y agoI think it means the analysis accounts for rounding error.
- ftxbro 4y agoYes it's this. They have identified an expressivity level that they are calling FOC[+;MOD] which is intuitively supposed to capture the expressivity that transformers and transformers-with-rounding have in common. More formally they are trying to track down exactly how this level compares to that of transformers, transformers-with-rounding, simplified stateless counter machines, and uniform TC(0), and they have done it with partial success and they are reporting their results.
- bmc7505 4y agoSee Merrill & Sabharwal (2023) [1]: A transformer N is a specific kind of a computation graph family over vectors of floating-point numbers with p precision. We work with fixed-precision transformers, i.e., we take p to be constant with respect to the input sequence length n. In practice, transformers typically use p = 32, and, several newer, larger transformer language models use p = 16 (Brown et al., 2020; Zhang et al., 2022), even while allowing larger context lengths n than their predecessors. [1]: https://arxiv.org/pdf/2210.02671.pdf#page=7 https://arxiv.org/pdf/2210.02671.pdf#page=7
- DaiPlusPlus 4y agoPlease exclude my ignorance, but what would happen if network weights were modelled with arbitrary-precision numerics, such as a rational type, instead of IEEE floats? (Other than drastically slowing things down, of course)
- bmc7505 4y agoWith arbitrary-precision, you can essentially replace the entire neural network with a single trainable parameter. [1] Likewise, in model checking, one often uses bounded-length bitvectors, because even a PDA with two stacks is Turing-equivalent. The poor separability between theoretical and physically-realizable models of computation is one of the weaknesses of the Chomsky hierarchy and classical approximation theory, and why more descriptive theories to characterize function complexity, e.g., circuit complexity, algebraic complexity theory and/or logical expressivity, are often needed. [1]: https://arxiv.org/pdf/1904.12320.pdf https://arxiv.org/pdf/1904.12320.pdf
- pizza 4y agoI guess wrt ieee floats, it depends on how often these cases happen and their consequences in the model: - rounding errors in arithmetic between small and large numbers, large and large numbers, or small and small numbers - unrepresentable numbers (eg 0.1) - non-associativity of arithmetic making order of evaluation relevant - residual connections can introduce, quite easily, arithmetic errors (heard this from research I can’t find atm): x + f(x) happens a lot in transformers, and the terms might be prone to cancellation or inadvertent rounding - layernorm blocks introducing some error - gradients might get added with error if too small or too big On the bright side, some people have suggested that ieee float problems are usually not so terrible that you can see them instead as introducing slightly beneficial regularization