Transformers are Efficient Compilers, Provably
Authors: Xiyu Zhai
Runlong Zhou
Liao Zhang
Simon Shaolei Du
Venue: COLM 2025 (2025)
Keywords: Transformers
Expressive Power
Programming Language
Attention Mechanism
Compiler
TL;DR: We prove transformers can efficiently act as compilers.

Abstract: Transformer-based large language models (LLMs) have demonstrated surprisingly robust performance across a wide range of language-related tasks, including programming language understanding and generation. In this paper, we take the first steps towards a formal investigation of using transformers as compilers from an expressive power perspective. To this end, we introduce a representative programming language, **Mini-Husky**, which encapsulates key features of modern C-like languages. We show that if the input code sequence has a bounded depth in both the Abstract Syntax Tree (AST) and type inference (reasonable assumptions based on the *clean code principle*), then the number of parameters required by transformers depends only on the *logarithm of the input sequence length* to handle compilation tasks, such as AST construction, symbol resolution, and type analysis. A significant technical challenge stems from the fact that transformers operate at a low level, where each layer processes the input sequence as raw vectors without explicitly associating them with predefined structure or meaning. In contrast, high-level compiler tasks necessitate managing intricate relationships and structured program information. Our primary technical contribution is the development of a domain-specific language, **Cybertron**, which generates formal proofs of the transformer's expressive power, scaling to address compiler tasks. We further establish that recurrent neural networks (RNNs) require at least a linear number of parameters relative to the input sequence, leading to an exponential separation between transformers and RNNs. Finally, we empirically validate our theoretical results by comparing transformers and RNNs on compiler tasks within **Mini-Husky**.

Published as a conference paper at COLM 2025
Transformers are Efficient Compilers, Provably
Xiyu Zhai
Runlong Zhou
University of Washington
University of Washington vectorzhēcs. washington edu
xiyuzhaiēcs. wwwzhai@cs..ashingtooooo. washington.ccmmm edu
Liao Zhang
Simon S. Du
University of Innsbruck
University of Washington ssduêcs. washington. .dd
zhangliao71 40g.a711@ com
Abstract
Transformer-based large language models (LLMs) have demonstrated prisingly robust performance across wide range of language-related tasks, including programming language analysis and generation. In this paper, we take the first steps towards formal investigation of using transform- ers as compilers from an expressive power perspective. We introduce a representative programming language, Mini-Husky, which encapsulates key features of modern C-like languages. We show that if the input code sequence has bounded depth in both Abstract Syntax Tree (AST) and type inference, then the number of parameters required by transformers depends only on the logarithm of the imput sequence length to handle compilation tasks, such as AST construction, symbol resolution, and type analysis. A signifi- cant technical challenge stems from the fact that transformers operate a low level, where each layer processes the input sequence as raw vectors without explicitly associating them with predefined structure or meaning. Our primary contribution is the development of a domain-specifit language, Cybertron, which generates formal proofs of the transformer's 's expressive power for compiler tasks. We further establish that recurrent neural net- works (RNNs) require linear number parameters relative the input sequence, leading to an exponential separation between transformers and RNNs, Finally, we empirically validate our theoretical results by comparing transformers and RNNs on compiler tasks within Mini-Husky.
1 Introduction
Transformers (Vaswani, 2017) have demonstrated remarkable proficiency across various do- mains, achieving near-expert performance in solving International Mathematical Olympiad problems (Google Deepmind, 2024) and excelling in complex reasoning tasks in science, coding, and mathematics (OpenAT, 2024a). They also handle routine coding tasks with high precision and have been integrated into code editors to significantly boost programmers' productivity (cur, 2024; Taelin, 2023a). Despite these advancements, the full extent of their underlying capabilities remains only partially understood.
In this paper, we aim to deepen our understanding of transformers' abilities to perform compilation tasks. Empirically, transformer-bases LLMs have shown rapid progress code generation and compilation. For example, MetaLL (Cummins et al., 2024) enables LLMs to optimize code by interpreting compiler intermediate representations (IRs), assembly language, and optimization techniques. Gu (2023) highlights the ability of LLMs to generate high-quality test cases for Golang compilers. Surprisingly, Taelin (2023b) demonstrates that models like Sonnet-3.5 can compile legacy code into modern languages like TypeScript, outperforming the now obsolete AgdaJS compiler (Agda Development Team, 2024). In parallel, Armengol-Estapé & O'Boyle (2021) investigates the application of a sequence-to- sequence Transformer model for translating source code into corresponding x86 assembly instructions, demonstrating its performance through training and empirical evaluation. Guo

---

Published as a conference paper at COLM 2025
& Moses (2022) highlights the superior performance of LLMs in optimizing low-level code generated from C programs, surpassing traditional compiler-base optimization techniques.
To formally study this problem in controlled setup, designed C-like programming language called mini-husky, which encapsulates key features of modern C-like languages such (Flanagan, 2011) and Rust (Klabnik & Nichols, 2023). We focus three represen- tative compilation tasks: abstract syntax tree (AST) construction, symbol resolution, and type analysis. The AST is a recursive structure that represents the input as a tree. From the perspective of programming language design, the AST is considered the true representation of the input, with the textual code serving merely as a convenient interface for human users (Alfred et al., 2007). All syntactic and semantic processing can then be interpreted as specific operations on these trees. Symbol resolution involves verifying the validity of references to entities and flagging errors for undefined symbols. Type analysis encompasses both type inference, which assigns types to variables without explicit annotations, and type checking, which identifies mismatches between actual and expected types.
We demonstrate that under the clean code principle (Martin, 2008), transformers can efficiently perform AST construction, symbol resolution, and type analysis, where efficiency means that these tasks can be conducted by transformers with a number of parameters that scale logarithmically with the input code length. To our knowledge, this is the first theoretical demonstration that transformers can function as compilers in a parameter-efficien manner.
We further compare transformers and recurrent neural networks (RNNss) By connecting the type analysis task with the associative recall, we show even under the clean code princi- ple (Martin, 2008), RNNs require memory size that scales linearly with the input sequence length to successfully perform type analysis. Consequently, for type analysis in compilation, transformers can be exponentialy more efficient than RNNs. We also empirically validate our theoretical findings by demonstrating the superiority of transformers.
Technical Challenges and Our Technique.
Proving that transformers can perform compilation tasks presents several challenges:
Transformers operate at too low level. Transformers process sequences of floating- piiiit
vectors, akin to raw bits in computers, and proving their ability perform specific tasks is similar to writing specialized parallel machine code. Previous work (Yao et al., 2021) often resorts to graphical illustrations for readability, even for basic tasks.
Compilers are exceedingly high-level. Compilers are among the most complex program- ming endeavors of our time. Compilation involves numerous sophisticated procedures, some of which are undecidable or computationally expensive, such as code optimiza- tion (Alfred et al., 2007)) and type analysis (Pierce, 2002). For example, type analysis in complex type systems poses significant challenges, often requiring the development of advanced logical frameworks (Dunfield & Krishnaswami, 2019).
To overcome these challenges, we design a domain-specific language (DSL.) called Cybertron to serve as the proof vehicle, i.e., major part of our proof consists of reasoning about type- correct code in Cybertron that represents a transformer. Without using Cybertron, writing an equivalent natural language proof would be too complex and intractable. Using code to prove propositions is not new to computer science; it is, in fact, the norm in interactive theorem proving (ITP) (Harrison et al., 2014). To the best of our knowledge, we are the first to apply this approach to understanding neural networks.
Contributions. We summarize our contributions below:
We introduce Mini-Husky, a simple yet representative C-like programming language, designed to formally assess transformers' capabilities in programming language processing. We anticipate that Mini-Husky will become standard testbed for this purpose.
A testbed for compilation tasks:
Expressive power theory of transformers for several compilation tasks: We provide a formal proof that, when the input code sequence has bounded AST depth and inference depth, the number of parameters in transformers only needs to scale logarithmically with the input sequence length to handle compilation tasks such as AST construction,
2

---

Published as a conference paper at COLM 2025
symbol resolution, and type analysis. To the best of our knowledge, this is the first study exploring the power of transformers for these compilation tasks.
Transformers RNNs: Theoretically, we demonstrate negative result, showing that the number of parameters in RNNs must scale linearly with the input sequence length to perform type analysis correctly. This result establishes exponential separation between transformers and RNNs. We further empirically confirm the advantage of transformers for the type analysis task.
A Domain-Specine Language for Proofs:
Given the challenges in formal proofs, we design a domain-specific language, Cybertron, serve as a proof vehicle. We believe that Cybertron, and the general approach of using DSLs for analysis, can have broader applications understanding transformers and other architectures.
2
Related Work
Expressive Power of Transformers. A line of work studies the expressive power of attention- based models. One direction focuses on the universal approximation power (Yun et al., 2019; Bhattamishra et al., 2020b;c; Dehghani et al., 2018; Pérez et al., 2021). More recent works present fine-grained characterizations of the expressive power for certain functions in different settings, sometimes with statistical analyses (Edelman et al., 2022; Elhage et al., 2021; Likhosherstov et al., 2021; Akyürek et al., 2022; Zhao et al., 2023; Yao et al., 2021; Anil et al., 2022; Barak et al., 2022; Garg et al., 2022; Von Oswald et al., 2022; Bai et al., 2023; Olsson et al., 2022; Akyürek et al., 2022; Li et al., 2023; Hao et al., 2022; Pérez et al., 2019; Strobl, 2023; Chiang et al., 2023; Wei et al., 2022; Wang et al., 2022; Feng et al., 2023; Li et al., 2024). There are also characterizations of transformers to be as powerful as universal computers put in looped context (Giannou al., 2023). The most related one is Yao et al. (2021) where the authors prove constructively that bounded depth Dyck language can be recognized by encoder-only hard attention transformers, which has similarities to our settings of bounded depth programming language recognized encoder-only hard attention transformers. The major difference is that we introduce concepts and tasks from programming language theory Pierce (2002) to study the semantic powers of transformers.
Transformers vs. RNN. It is important to understand the comparative advantages and disadvantages of transformers against RNNs. Empirically, synthetic experiments have shown an advantage of transformers against RNNs for long range tasks (Bhattamishra et al., 2023; Arora et al., 2023). Theoretically, there has been rich line of work focusing on comparing transformers and RNNs in terms of recognizing formal languages (Bhattamishra et al., 2020a; Hahn, 2019; Merrill et al., 2021), which show that the lack of recursive structure of transformers prevent them from recognizing some formal languages that RNNs can recognize. However, the gap can be mitigated when we consider the bounded length of input or bounded grammar depth (Liu et al., 2022; Yao et al., 2021), which is quite reasonable in practice and used in this paper. On the other side, prior work (Jelassi et al., 2024; Wen et al., 2024) proves à representation gap between RNNs and Transformers in repeating long sequence. In summary, memory perform badly at tasks which requires information retrieval. Our paper shows that semantic analysis for programming languages is such task.
somehow intuitive that recursive structures with limited
DSLs for Transformers. We note that we are not exactly the first one to employ a domain- specific language understand the expressive powers of transformers. Previously, DSLs with simple typings like RASP (Weiss et al., 2021) were proposed to prove constructively that transformers can do various basic lequence-to-sqquene (2023) writes a compiler that compiles RASP into actual transformers, Friedman et al. (2023) shows that RASP can be learned, and Zhou et al. (2023) uses RASP to prove that simple transformers can perform certain algorithms. The major difference between RASP and our DSL Cybertron is that Cybertron has a powerful algebraic type system that helps prove complicated operations beyond simple algorithms.
operations. Lindner et al.
3

---

Published as a conference paper at COLM 2025
3
Preliminaries
The major innovation in the transformer architecture is that it uses self-attention solely without conjunction with a recurrent network (Vaswani, 2017), which processes input tokens in distributed manner. This capability enables the model to handle raggrange dependencies, a crucial feature for language tasks. We use hard attention and simplified position encoding to simplify our theoretical reasoning.
Attention. In practice, attention heads use soft attention. Given model dimension model number of heads H, and finite set of token positions Pos, attention layer with simplified position encoding is defined as a function fattn PR Xdmadel
R xdmadel given by
Vp E Pos, fatmn( (x) = Wo Concat (Attn (1) (x) pr. Attn (H) (X)
(1)
where the htth attention head is defined using soft attention as: Attn (k) (x), = EpepPos a
(h) ((t)) The attention weights a (i) ",p"
p.p given by: a p.p
expl O k +A
where Wo E Remodel Xd are trainable parameters,
EyMeros exp 0p0) <() +20h) (""p)) (1) 0 p
((h) E Rdladd//1l are linear transformations of Xp, A(h) E IR² depends on the
9 head, and Wg 19>0
E R² accounts for relative position.
For theoretical convenience, we use average hard attention, commonly used in theoretical analysis of transformer (Yao et al., 2021; Hao et al., 2022; Pérez et al., 2019). Average hard attention can be viewed as the limit of soft attention when the attention logits become infinitely large. The hard attention head is defined as:
Attn (k) (X)
1
Σ P'ESp
(hh) p' where Sp = arg max P'EPos
(0f K + +1 (
(2)
S
In other words, hard attention selects the positions p' that maximize the attention score for each position and averages the corresponding value vectors vy
Although our analysis employs hard attention, it can be viewed as theoretically grounded approximation of soft attention in settings where a single attention logit significantly out- weighs the others. In such cases, the softmax function assigns exponentially diminishing weights to non-maximal logits as the gap increases. In the limit, soft attention approaches one-hot distribution, effectively becoming hard attention. This approximation adopted in theoretical studies (Yao et al., 2021) and aligns with empirical observations, particularly when attention distributions are sharply concentrated due to scaling effects or learned sparsity.
commonly
Feed-Forward Layer.
Given model dimension dmodel, and a finite set of token positions Pos, a feed-forward layer is fully connected layer applied independently to each position, defined function fin R xdmmdde - R Pos xdmedell given by
Vp E Pos, [x)(X)p W20RELU (WiXp + b1) + bz.
where W1 E Rd Xolmmee and W22 E R xdlin are trainable weight matrices, by E R and b2 @odel are trainable bias vectors, dim is the hidden dimension of the feed-forward layer, chosen to be 2d as commonly used in practice, UReLU is the ReLU activation function.
Encoder-Only Transformer. Encoder-only transformers consist solely of the encoder stack, making them ideal for tasks like classification, regression, and sequence labeling that do not require sequence generation. Each encoder layer includes a multi-head self-attention mech- anism and a feed-forward network, allowing the model to capture complex dependencies and contextual information.
4

---

Published as a conference paper at COLM 2025
Compiler
Raw Text
Token Stream
AST
Semantic Analysis
Tokenizer
Transformer
Figure 1: Programming language processing pipeline.
One can define using the following recurrence,
The input is given by: x = X.
For each layer =
L: Compute attention output: 811) = x(1-1)
+ (()) (X (!)
-Compute feed-forward output: x(I) x() + Itm ((1))
In the above, (!!) the attention layers, and fin are the feed-forward layers, with the same model dimension dmodel, number of heads H, and set of token positions Pos. For simplicity, layer normalization is ignored. See Appendix C for full details of transformers and other architectures.
Programming Language Processing and The Target C-Like Language: Mini-Husky
Recently, transformers have expanded to support code analysis and generation (Nijkamp et al., 2023; Chen et al., 2021; Anysphere, 2023). Programming languages offer cleaner foundation for studying language understanding, as their syntactic and semantic tasks are precisely defined. To formally study the language processing capabilities of transformers, we design Mini-Husky, representative mix of modern C-like languages with strong typing and typical syntactic features. It supports user-defined types (e.g., structs, enums) and enforces strict type equality, disallowing implicit conversions. Lexical scoping, including shadowing, ensures proper variable accessibility based on block structures, type inference, and type checking. These features make compiling Mini-Husky representative task to evaluate transformers' capabilities in syntactic and semantic tasks like symbol resolution and type checking. See Appendix E for the full details of Mini-Husky.
The standard pipeline of processing programming languages shown in Figure (Alfred et al., 2007). The input text is initially decomposed into sequence of lexical elements such as literals, identifiers, punctuation symbols, and language keywords; this sequence is referred to the token stream.. Subsequently, the token stream is parsed into hierarchical, tree-structured representation that reflects the grammatical structure of the input. Finally, syntactic and semantic analyses are conducted on the resulting tree verify correctness and extract meaningful information. Afterward, an intermediate language program is generated based on the syntactic and semantic analysis, which is further optimized and finally transformed into targeted machine code. To simplify the presentation, we assume the tokenizer has been provided a priori. Below we describe the programming language processing tasks investigated in the paper.
Abstract Syntax Tree Construction. Abstract Syntax Tree (AST) hierarchical, tree-like representation of the syntactic structure of source code in a programming language. Unlike the raw text of the code, the AST abstracts away surface syntax details, capturing the essential elements and their relationships in structured form. Each node in the AST corresponds to a construct occurring in the source code, such as expressions, statements, or declarations. This representation is central to various stages of language processing, enabling efficient syntax checking, semantic analysis, and code generation. The formal definition of ASTs is standard in the programming language literature but is lengthy, so
5

---

Published as a conference paper at COLM 2025
defer it to Appendix A. The AST construction task's final output is the collection of all AST nodes. We will show transformers can construct AST efficiently.
Symbol Resolution. In programming languages, symbols are functions, types, generics, variables, macros, etc. They are defined somewhere and can be used by reterring to the corresponding identifier path in certain scope. The scope be within certain tree of modules, or within a certain curly braced scope within one module. For simplicity, we only consider curly braced scope. In Mini-Husky, the following showcases symbol resolution.
fn ro fn f1O (
let 1; x a: let
let
{ let a
let y aa;
11
12
2 a:;
13
}
14
80 FF
The outer function f is accessible everywhere in the body of function g. However, the inner function fi can only be used inside the body of f as it is defined within the body. For variables with the same identifier a , a from line 4 is accessible from line 5, the second is accessible from line 12, the third is accessible from line 10, and the fourth is not accessible from anywhere. Thus x l, 3,z 2.
The output of the symbol resolution task is the collection of symbol resolution results on all applicable tokens. More concretely, the output is sequence of values of type Option-SymbolReeoottinn where Option-SymbolRRsoluttonn is the type SymbolResolution
with a null value added for non-applicabillty and SymbolResolution is the type storing the result of the symbol resolution, being either success with a resolved symbol of type Symbol or a failure with an error of type SymbollkesolutionEEro: We shall prove that transformers can do symbol resolution and that attention is crucial.
Type Analysis. In general, types are essential for conveying the intended usage of the written functions and specifying constraints. As first exploration of this topic, try to make the type analysis in Mini-Husky as simple as possible yet able to bring out the essential difficulty. The type system consists of four sequential components: (1) Typee definition, (2) Type specification, (3) Type inference, and (4) Type checking. Due to the page limit, here we only introduce (4) Typpe checking because it is the final step and this is crucial step which separates transformers and RNNs. See Appendix E.1 for details of (1) Type definition, (2) Type specification, and (3) Type inference.
Type checking ensures that the typed expressions agree with its expectations. For simplicity, we do not allow implicit type conversion, so the agreement means exact equality of types. The arguments of function calls are expected to have types according to the definition of the function. The operand type of field access must be a struct type with field of the same name. The type of the last expression of the function body or the expr in the return
statement must be equal to the return type of the function. For variables defined in the let statement, the types are annotated, the types of the left-hand side and right-hand side should be in agreement.
Type the return type "132", yet the last expression is type "322" Fn f(a: 132) >> 132 1.1.)
struct xx: 132
gO
// Type Error: "x" is of type f32 but it's assigned by value of type "13" Type Error: first argunent "P" expected type but gets literal instead let x: f32 f(1.1);
// Type Error: Field "y"

---

Published as a conference paper at COLM 2025
y 1.y:
12
The above incorporates typical examples of type disagreements that count as type errors. A compiler should be able to report these errors.
The type analysis task's final output is the collection of all type errors. More concretely, the output is sequence of Option<lypeErroo>> where Option=IypeErroo> denoted the type Typešrror will null value added and TypeError is the type storing the information of type error. The position of type errors agrees with the source tokens leading to these errors.
5 Expressive Power of Transformers as Efficient Compilers
In this section we discuss main theoretical results about the expressive power of transformers to perform compilation tasks: AST construction, symbol resolution, and type analysis. In Section 5.4, we discuss Cybertron, DSL specifically designed for our proof.
resulls
5.1 Abstract Syntax Tree Construction
We start with a definition that characterizes low-complexity code.
Definition 1 (code with Bounded AST-Depth). Let MiniHusky p be the set of token sequences that can be parsed into valid ASTs in Mini-Husky with depth less than D.
D in the above definition is small for all programming languages in practice, and a linear dependency on D is acceptable, but the linear dependency on the length of the token sequence L is not.
The bounded depth assumption is both practically reasonable and theoretically grounded. In practical software development, the clean code principle (Martin, 2008) requires one to write code with as little nested layer as possible for greater readability. Readability is of the utmost importance because "Programs are meant to be read by humans and only inci- dentally for computers execute" (Abelson al., 1996). Moreover, while real-world code can exhibit significant depth-and in extreme cases, can even be NP-hard to analyze-in in practice, most codebases maintain relatively shallow nesting for the sake of readability and maintainability. For example, although the Linux kernel comprises tens of millions of lines of code, the majority of its functions are short and have limited structural depth. Theoretically, the bounded-dephl assumption is essential for understanding the limitations models. The transformer architecture inherently supports only finite-
of transformer-basee depth computation. This limitation has been discussed in prior work, such (Yao et al., 2021), which highlights the importance of architectural depth when modeling more complex behaviors.
This assumption of bounded hierarchical depth is not limited to just programming lan- guages, but is often seen as applicable to natural languages (Frank et al., 2012; Brennan & Hale, 2019; Ding et al., 2017), motivating Yao et al. (2021) to have a similar boundedness assumption. Below is the main result for AST construction using transformers.
Theorem 1. There exists a transformer encoder of model dimension and number of layers being O(log L D) and number of heads being O(1) that represents a function that maps any token sequence of length L in MiniHusky D to ils absiract syntax tree represented as a sequence.
We note log is small because 64-bit computers can only process context length at most 264 and D is small by assumption. Therefore, there exists transformer with an almost constant number of parameters that is able to process comparatively much longer context length. See full proof details in Appendix F.
5.2 Symbol Resolution
Next, we show that transformers can effectively perform symbolic resolution as log L and D almost constant compared with context length l.. The proof details in Appendix G.
7

---

Published as a conference paper at COLM 2025
Theorem 2. There exists transformer encoder of model dimension and number of layers being (log D) and number of heads being O(1) that represents a function that maps any token sequence of length L in MiniHuskyp to its symbol resolution represented as sequence of values of type
5.3 Type Analysis
We need an additional definition to characterize the complexity of code for type analysis.
Definition 2 (code with Bounded AST-Depth and Type-Inference-epthh
We use to denote the subset of MiniHusky D with the depth of type inference no more than H. The depth of type inference is the number of rounds of computation needed to infer all the types using the type-inference algorithm (described in Appendix E.1).
In practice, H is significantly smaller than the context length for reasonably written code because it is upper bounded by the number of statements in function body which is required to be small according to the clean code principle (Martin, 2008). Below, we present the main result of using transformers for type analysis. See full details in Appendix H.
Theorem 3. For L, D, H E N, there exists a transformer encoder of model dimension, and mumber of layers being (log L + D H) and number of heads being ((1) that represents function that maps any token sequence of length I. in MiniHusky Annotated D,H to its lype errors represented as a sequence of values of type Option<TypeError>>
5.4 Proof Vehicle: Cybertron, a Domain-Specific Language
Here we highlight our main proof technique. Proving that transformers can express com- plex algorithms and software like compilers is a significant challenge due to the inherent differences between how transformers operate and the nature of high-level tasks they are ex- pected to perform. Transformers process input low level, where each layer manipulates raw token sequences as vectors without predefined structure or meaning. However, high- level tasks-such as constructing ASTs and performing type and symbol analysis analysis-require handling complex, structured information that depends on long-ran oaggrange relationships and interactions across the input. Bridging the gap between this raw, unstructured processing and the structured, multi-step logic required for these tasks introduces significant difficulty, Compilers, for instance, typically rely on rule-based, step-by-step operations that are ab- stract and sequential, which transformers must simulate through their attention mechanisms and feedforward layers. The challenge is further compounded by the need to formally prove that transformers can handle such tasks efficiently and accurately, despite operating in fundamentally different manner. To address these challenges, we propose a domain-speciff language (DSL) called Cybertron, which allows are capable of expressing complex algorithms while maintaining sufficient readability.
systematically prove that transformers
key feature of Cybertron its expressive type system, which provides strong correctness guarantees. The type system ensures that every value is strongly typed, making it easier to reason about function composition and ensuring the validity of our proofs. This type system is crucial for managing how transformers represent and manipulate both local and global types-where where local types correspond to individual tokens and global types refer to sequences of tokens, encapsulating broader program information.
What transformers output a representation in sequences of vector of sequences of values in these types. As types are mathematically interpreted in this paper discrete subset of a vector space, Cybertron allows us to construct transformers guarantees if the Cybertron code is type-correct.
automatic value validity
In Cybertron, complex functions are broken down into "atomic" operations through propo- sitions on function compositions and computation graphs (Propositions 11,13,14,2). It is straightforward to prove that these " "atomic" operations are representable by transformers, either by feedforward layers attention layers. For example:
8

---

Published as a conference paper at COLM 2025
Feedforward layers: boolean operations like AND (Proposition 6), OR (Proposition 7),
NOT (Proposition 5), or operations over option types like Option:or (Proposition 9) being applied to each token sequence.
Attention layers: operations that require information transmission between tokens such as nearest_left and reihest that collect for each token the nearest left/right non-nil information (Propasition 15).
This approach allows us to break down complex operations into primitive tasks that trans- formers can simulate. Feedforward layers handle local operations on individual tokens, while attention layers manage Longrrange dependencies and interactions between tokens, simulating the multi-step reasoning required for higher-level tasks.
Cybertron's 's expressive type system and function composition framework help bridge the gap between the low-level processing transformers perform and the high-level reasoning necessary for complex tasks like compilation. For full details, including the mathematical foundations of Cybertron's 's type system and function composition, see Appendix D.
6
Comparisons between Transformers and RNN
Now compare transformers and RNNs from both theoretical and empirical perspectives.
6.1 A Lower Bound for RNNs for Type Checking
Previously, has shown that RNN provably less parameter efficient than transformers for associative recall (Wen et al., 2024). Observing that the type checking step covers associative recall, we obtain the following lower bound for RNNs.
Theorem 4. For L, D, H E N, any RNN that represents function that maps any token sequence of length L in MimiHHussyAmmotttedd
with D,H = O(1) to its type errors represented as a sequence of values of type Option<TyypError>> then its state space size least ((L).
Theorem 3 and give a clear separation between transformers and RNNs in terms of the compilation capability. If the input codes satisfy D, & L, which is typically the case under the clean code principle (Martin, 2008), then transformers at most need O ((log L + D + H)) number of parameters, which significantly smaller what RNNs require, (((L).
6.2 Empirical Comparison between Transformers and RNNs
We validate our theoretical results by conducting experiments on synthetic data.
Dataset construction. The synthetic dataset is parameterized by и (the number of data pieces), f (the number of functions in a data piece), a (the maximum number of arguments of any function), c (the maximum number of function calls involved in any function), d (the minimum distance between the declaration and the first call of a function, as well as the minimum distance between its consecutive calls), v (the probability of using variable in function call), and (the error rate of using an incorrect type in a function call).
The names of the functions are drawn randomly and uniquely from list of English words. For each of the arguments of any function, its symbol is randomly drawn from another list English words and its type is randomly drawn from {Int, Float, Bool]. All the called functions must be declared and not called by at least d functions ahead of the current one. For each argument of any function call, with probability v, the argument variable of the enclosing function is used regardless of its type, with probability (1 (1- (1 e),, a literal of the correct type is used, and with probability (1 uoe an incorrect type literal is used. For integers, the literals are from {0, 1,.,, 99); for floats, the literals are from {0.1, 1.1, ... 99.1}; for booleans, the literals are from (rree, false). The training dataset and evaluation dataset use disjoint lists for function names and argument symbols. See Appendix J for example.

---

Published as a conference paper at COLM 2025
1300020-404455
74000330 20l-900000dddd100000000000
205
350
28
130 20
304
Figure 2: Figures depicting the accuracy of the expected type (see Section across different models, measured by their number of trainable parameters. Training accuracies are better indicators of the expressive power of the models (instead of generalizability) than evaluation accuracies. We also report evaluation accuracies in Appendix
We use synthetic data instead of real code because our paper is theoretically focused, and the experiments only serve validate our theory. Hence, using synthetic data gives a clean, controllable setting to compare transformers and RNNs.
Model and training. We use customized BERT models (Devlin et al., 2019) and bidirectional RNN models (Schuster & Paliwal, 1997) in our experiments. To control the model size (i.e., the number of trainable parameters), we adjust only the hidden sizes while keeping other hyperparameters constant. Detailed model specifications can be found in Table 1. For both transformers and RNNs, we use the hyperparameters listed Table 2 in Appendix). J.
Results. We experimented with multiple combinations of models (Table 1) and datasets (Table 2). For each combination, we conducted independent runs using a fixed set of random seeds. When plotting the figures, we took the top & 5 training/ evaluation losses/accural accuracies from each run and averaged over all the k x values. We plotted separate figures for each dataset and separate sub-figures for each metric. In each sub-figuu sub-figure, the x-axis represents the number of trainable parameters, and the y-axis represents the averaged values. Results are shown in Figure 2. They demonstrate that customized BERT models are able to perform better at type checking than bidirectional RNN models when both scale up, corroborating our theories. Other results are Appendix..
Conclusions and Future Work
We demonstrated that transformers can efficiently handle number of syntactic and seman- tic analysis tasks in C-like languages, using Cybertron to prove their capacity for tasks like AST generation, symbol resolution, and type analysis. We showed theoretical and empirical advantages of transformers over RNNs, particularly in their ability to manage long-range dependencies with logarithmic parameter scaling.
Future research directions include extending our theoretical framework to encompass universal transformers, which may eliminate the current reliance on the assumption of bounded program depth in our analysis Shaw et al. (2024). Another promising avenue the generalization of our approach from foundational forms of static code analysis to more comprehensive categories of static analysis, potentially incorporating asynchronous constructs and related features. Lastly, a valuable line of inquiry involves formalizing practical aspects of code generation with the goal of rigorously characterizing the expressive power of wransfomer-basee models in such contexts.
Acknowledgement
XZ acknowledges the support of NSF through awards DMS-2031883 and PHY-2019786. LZ acknowledges the ERC PoC project FormalWeb3 no. 101156734 and the University of Innsbruck doctoral scholarship promotion of young talent. SSD acknowledges the support of NSF DMS 2134106, NSF CCF 2212261, NSF iis 2143493, NSF IIS 2229881, Sloan Fellowship, the AI2050 program at Schmidt Sciences, Amazon, and Apple.
10

---

Published as a conference paper at COLM 2025
References
Cursor: Ai-powered code editor, 2024. URL httht:::://ww..crrrr Accessed: Septem- ber 29, 2024.
Harold Abelson, Gerald Jay Sussman, and with Julie Sussman. Structure and Interpretation of Computer Programs. MIT Press/ McGraw-Hill, Cambridge, 2nd editon edition, 1996. ISBN 0-262-01153-0.
Agda Development Team. Agda compilers manual v2.6.4.,, 2024. URL https: readthedocs. io/en/v2.6.4. wtt...../oll/////oooooooooooloot htt.ttoos//ooolsssss....o wtt.aaaaaaarppp-aaeeedddddd
Ekin Akyürek, Dale Schuurmans, Jacob Andreas, Tengyu Ma, and Denny Zhou. What learning algorithm in-context learning? investigations with linear models. arviv preprint ar arXiv:2211.1561, 2022.
V Aho Alfred, S Lam Monica, and D Ullman Jeffrey. Compilers principles, techniques & tools. pearson Education, 2007.
Cem Anil, Yuhuai Wu, Anders Andreassen, Aitor Lewkowycz, Vedant Misra, Vinay Ra- masesh, Ambrose Slone, Guy Gur-Ari, Ethan Dyer, and Behnam Neyshabur. Exploring length generalization in large language models. ar preprint ar arXit:2207.0400 2022.
Anysphere. Cursor, 2023. URL http::tt////wt /ttpr/////////////.o...oooo/ooon
Jordi Armengol-EEsapp and Michael FP O'Bolle. Learning x86 translation: An experi- ment in neural compilation. Xrv preprint ar Xfte:22108.0763, 2021.
Simran Arora, Sabri Eyuboglu, Aman Timalsina, Isys Johnson, Michael Poli, James Zou, Atri Rudra, and Christopher R'e. Zoology: Measuring and improving recall in efficient language models. ArXiv, abs/ abs//232.04927, 2023. URL https: //api. semanticscholar org/
26rpusID: 143322.
Yu Bai, Fan Chen, Huan Wang, Caiming Xiong, and Song Mei. Transformers as statisti- cians: Provable in-context learning with in-context algorithm selection. arv preprint ar arXiv:2306.04637 2023.
Boaz Barak, Benjamin Edelman, Surbhi Goel, Sham Kakade, Eran Malach, and Cyril Zhang, Hidden progress in deep learning: Sgd learns parities near the computational limit. Advances in Neural Information Processing Systems, 35:21750-21766 2022.
S. Bhattamishra, Kabir Ahuja, and Navin Goyal. On the ability and limitations of transform- ers to recognize formal languages. In Conference on Empirical Methods in Natural Language Processing, 2020a. URL https: / /api. semanticscholar. httpcicccchoaaooooororrrrruueeee org//orrpuSD::22225555
Bhattamishra, Arkil Patel, Phil Blunsom, and Varun Kanade. Understanding in-context learning in transformers and Ilms by learning to learn discrete functions. ArXiv, abs//310.03011, 2023. URL httts::/api..smmatiicchooo////
S. Bhattamishra, Michael Hahn, Phil Blunsom, and Varun Kanade. Separations in the repre- sentational capabilities of transformers and recurrent architectures. ArXiv, /2042047999 2024. URL https: /api. semanticscholar org hngg/CorppSID: (t0rppuuII:22444000000 278440803.
Satwik Bhattamishra, Kabir Ahuja, and Navin Goyal. On the ability and limitations of transformers to recognize formal languages. arXiv preprint ar Xix::2009.11266 11264, 2020b.
Satwik Bhattamishra, Arkil Patel, and Navin Goyal. On the computational power of transformers and its implications in sequence modeling. arXiv preprint x=Xio:2006.09286 2020c.
Jonathan Brennan and John Tracy Hale. Hierarchical structure guides rapid linguis- tic predictions during naturalistic listening. PLoS ONE, 14, 2019. URL https://api. htt.:cccchooooooooooo/ops//////0
semanticscholaat .org/CorppuID::2653333299
11

---

Published as a conference paper at COLM 2025
Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde De Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al. Evalu- ating large language models trained code. at Xiv preprint ar (ktu:21070033777 2021.
David Chiang, Peter A. Cholak, and Anand Pillay. Tighter bounds on the expressivity of transformer encoders. In International Conference Machine Learning, 2023. URL semanticscholar
httpsss//ap...emnnniicchoool wrg/CorpusID: 256231094.
Chris Cummins, Volker Seeker, Dejan Grubisic, Baptiste Rozière, Jonas Gehring, Gabriele Synnaeve, and Hugh Leather. Meta large language model compiler: Foundation models of compiler optimization. ArXiv, /b4/ 2407.02524, 2024. https: //aii semanticscholar.
org/CorpusID: (t00rpuuuI::202243333 270924331.
Valentin David. Language Constructs for C++-like languages. PhD thesis, University of Bergen, 2009.
Mostafa Dehghani, Stephan Gouws, Oriol Vinyals, Jakob Uszkoreit, and Lukasz Kaiser. Universal transformers. arXiv preprint ar fio:1807.03819 2018.
Jacob Devlin, Ming-Wei. Chang, Kenton Lee, and Kristina Toutanova. Bert: Pre-training of deep bidirectional transformers for language understanding, 2019. URL https://arxiv. org/abs/18) /1800. 04805.
Nai Ding, Lucia Melloni, Xing Tian, and David Poeppel. Rule-based and word-level statistics-based processing of language: insights from neuroscience. Language, Cognition and Neuroscience, 32:570 575, 2017. URL https://apt semanticscholar.... org/CorpusID: 46747073.
Alexey Dosovitskiy, Lucas Beyer, Alexander Kolesnikov, Dirk Weissenborn, Xiaohua Zhai, Thomas Unterthiner, Mostafa Dehghani, Matthias Minderer, Georg Heigold, Sylvain Gelly, et al. An image is worth 16x16 words: Transformers for image recognition at scale. arv preprint ar drXiv=2010.11929, 2020.
Jana Dunfield and Neelakantan Krishnaswami. Sound and complete bidirectional type- checking for higher-rank polymorphism with existentials and indexed types. Proceedings of the ACM on Programming Languages, 3(POPL):1228, 2019.
Benjamin L Edelman, Surbhi Goel, Sham Kakade, and Cyril Zhang. Inductive biases and variable creation in self-attention mechanisms. In International Conference on Machine Learning, pp. 5793-5831. PMLR, 2022.
N Elhage, N Nanda, Olsson, T Henighan, N Joseph, B Mann, A Askell, Bai, A Chen, T Conerly, et al. A mathematical framework for transformer circuits. Transformer Circuils Thread, 2021.
Husna Farooqui. The curry-howard correspondence. pommattiicccolar..rg//oopppupu orgg/CrppssI:: 240pppu8. 244268761.
2021.
URL https://api.
Guhao Feng, Yuntian Gu, Bohang Zhang, Haotian Ye, Di He, and Liwei Wang. To- wards revealing the mystery behind chain of thought: a theoretical perspective. ArXiv, abs/2305.15408, 2023. URL httph::/tapppp semanticscholatt org. (C:
David Flanagan. JavaScript: The definitive guide: Activate your web pages. " "O'Reilly Media,
Bryan Ford. Parsing expression grammars: a recognition-based syntactic foundation. In Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 111-122, 2004.
S. Frank, Rens Bod, and Morten H. Christiansen. How hierarchical is language use? Pro- ceedings of the Royal Society B: Biological Sciences, 279:4522 4531, 2012. URL https: //api. www.steeaaattiooollo.omm htt.hooo.....oo//rorouii::11/11 19691111.
12

---

Published as a conference paper at COLM 2025
Dan Friedman, Alexander Wettig, and Danqi Chen. Learning transformer programs. ArXiv, abs/2306.01128, 2023, URL https://aps seemantisscoola..rgg//ooooe :05.rppus1::2990433244 259064324.
Shivam Garg, Dimitris Tsipras, Percy $ Liang, and Gregory Valiant. What can transformers learn in-context? case study of simple function classes. Advances in Neural Information Processing Systems, 35:30583-30598, 2022.
Angeliki Giannou, Shashank Rajput, Jy yong Sohn, Kangwook Lee, Jason D. Lee, and Dimitris Paapalliopoulos. Looped transformers programmable computers. ArXiv, abs/2301.1311 2023, URL hatp::/pppi semanticscholar org org//CorpSSID:225336666 256389656.
Google Deepmind. Ai achieves silver-medal standard solving international mathemat- ical olympiad problems, July 2024. URL https: http://deeeee.n///// owt.:/nino...ogg///dissovvrrroor ai bi-solin bolsolles-an ine--iio--poor propless-attttttee at- -edee-
Qiuhan Gu. Llm-based code generation method for golang compiler testing. Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foun- dations of Software Engineering, 2023, URL https: www.nticscholiioo. wrg//orppslDD 265509921.
Zifan Carl Guo and William Moses. Enabling transformers to understand low-level programs. In 2022 IEEE High Performance Extreme Computing Conference (HPEC), pp. 1-9. TEEE, 2022.
Michael Hahn. Theoretical limitations of self-attention in neural sequence models. Trans- actions of the Association for Compulational Linguistics, 8:156-171, 2019. URL https:
coamanticccholar.orgg.
189.1:::11118888 89928186.
Sophie Hao, Dana Angluin, and Roberta Frank. Formal language recognition by hard attention transformers: Perspectives from circuit complexity. Transactions of the Association for Computational Linguisties, 10:800-810, 2022. URL https://apt: semanticscholas
CorpusID: 248177889.
John Harrison, Josef Urban, and Freek Wiedijk. History interactive theorem proving. In Handbook of the History of Logic, volume 9, pp. 135-214. Elsevier, 2014.
Samy Jelassi, David Brandfonbrener, Sham M. Kakade, and Eran Malach. Repeat after me: Transformers are better than state space models at copying. ArXiv, 0bs//442.00003) 2024. URL https://api semanticscholas
I 2674866677.
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order con- current separation logic. Journal of Functional Programming, 28, 2018. URL https: //api. cittmnanticcchllar wwt.chooa...rrroorropooetoe wwtg//orpssssi22/....oom 2023423.
Steve Klabnik and Carol Nichols. The Rust programming language. No Starch Press, 2023.
Shuai Li, Zhao Song, Yu Xia, Tong Yu, and Tianyi Zhou. The closeness of in-context learning and weight shifting for softmax regression. Xiv preprint arXiv:2304.1327, 2023.
Zhiyuan Li, Hong Liu, Denny Zhou, and Tengyu Ma. Chain of thought empowers trans- formers to solve inherently serial problems. In The Twelfth International Conference on Learning Representations, 2024. WtLp:tts://
Valerii Likhosherstov, Krzysztof Choromanski, and Adrian Weller. On the expressive power of self-attention matrices. Xrv preprint arXiv:2106.03764, 2021.
David Lindner, J'anos Kram'ar, Matthew Rahtz, Tom McGrath, and Vladimir Mikulik. Tracr: Compiled transformers as laboratory for interpretability. ArXiv, abs/2231.05062 2023.
URL https://api semanticscholar wwtp//orgs//ai./ C 255749893.
Bingbin Liu, Jordan T. Ash, Surbhi Goel, Akshay Krishnamurthy, and Cyril Zhang. Transformers learn shortcuts to automata. ArXio, abs/2210.10749, 2022. URL https: //api. wwwanti wtt.eeatttttttt....ooooooooooooa ortg://rrpssSD:252227755
13

---

ort.r//oo.....oor/o/oorooooaaaa. Published as a conference paper at COLM 2025
Robert C. Martin. Clean Code: A Handbook of Agile Software Craftsmanship. Prentice Hall PTR, USA, edition, 2008. ISBN 0132350882.
Patrick Massot.
Teaching mathematics using lean and controlled natural language. In Interna- fional Conference on Interactive Theorem Proving, 2024. URL nttps://api. semanticscholar.
org/CorpusID:210 272330159,
The mathlib Community. The lean mathematical library. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019. URL https:
//api. semanticscholar. hwt.ooaar..rrr/oorusss22222000
William Merrill, Ashish Sabharwal, and Noah A. Smith. Saturated transformers are constant- depth threshold circuits. Transactions of the Association for Computational Linguistics, 10: 843-856, 2021. URL https://apt wemanti wwwpllarrr.rggorooutttooooo 24800P08 248085924.
Erik Nijkamp, Hiroaki Hayashi, Caiming Xiong, Silvio Savarese, and Yingbo Zhou. Code- gen2: Lessons for training Ilms on programming and natural languages. ICLR, 2023.
Catherine Olsson, Nelson Elhage, Neel Nanda, Nicholas Joseph, Nova DasSarma, Tom Henighan, Ben Mann, Amanda Askell, Yuntao Bai, Anna Chen, et al. In-context learning and induction heads. arXiv preprint arXiv:2209.1189) 11895, 2022.
OpenAl. Openai ol system card, September 2024a. openai-ol-system-ccae
URL https://openai..omm
OpenAL. Sora: Creating video from text, February 2024b. URL https:///ppenai.com/ sora/.
Jorge Pérez, Javier Marinkovic, and Pablo Barceló. On the turing completeness of mod- ern neural network architectures. ArXiv, abs/1901.03429, 2019. URL https://api.
Jorge Pérez, Pablo Barceló, and Javier Marinkovic, Attention is turing complete. The Journal of Machine Learning Research, 22(1):3463-3497, 2021.
Benjamin C Pierce. Types and programming languages. MIT press, 2002.
The Univalent Foundations Program. Homotopy type theory: Univalent foundations of mathematics. arXiv preprint arXiv:1308.077 0729, 2013.
Mike Schuster and Kuldip K Paliwal. Bidirectional recurrent neural networks. IEEE transactions on Signal Processing, 45(11):2673-2681, 1997.
Peter Shaw, James Cohan, Jacob Eisenstein, Kenton Lee, Jonathan Berant, and Kristina Toutanova. Alta: Compiler-based analysis of transformers. arXiv preprint arXit:2410.18077 2024.
Lena Strobl. Average-hard attention transformers are constant-depth uniform threshold circuits. ArXio, abs/2308.03212, 2023, URL https://api. sewaaticcoaaan...rrrr.... wwtp:/orp//o/oll/oo/oooo 260680416.
Victor Taelin. Ai and the future of coding.
-oter-uuuuur--o-ooo----------- c3dd3, 2023a. Accessed: 2024-10-01.
Victor Taelin. Agda to typescript compilation with sonnet-3.5, 2023b. URL https: //x. com/ Accessed: September 29, 2024.
A Vaswani. Attention is all you need. Advances in Neural Information Processing Systems, 2017.
Johannes Von Oswald, Eyvind Niklasson, Ettore Randazzo, João Sacramento, Alexander Mordvintsev, Andrey Zhmoginov, and Max Vladymyrov. Transformers learn in-context by gradient descent. arXiv preprint ar XT11:221..07677,, 2022.
14

---

Published as a conference paper at COLM 2025
Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc Le, Ed Huai hsin Chi, and Denny Zhou. Self-consistency improves chain of thought reasoning in language models. ArXiv, Abs/2203.11171, 2022. URL https://app semanticscholar ott.aaatttccccoo..oooooooooooooo /ttpCCorpusSD2225552222
Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Ed Huai hsin Chi, F. Xia, Quoc Le, and Denny Zhou. Chain of thought prompting elicits reasoning in large language models. ArXiv, /ttp//2201.1103,, 2022. URL https://appi semanticscholar. wwwpscchooaa..ooooroouuoueeeee org/CorpusID: 246411621.
Gail Weiss, Yoav Goldberg, and Eran Yahav. Thinking like transformers. ArXiv, abs/2106.06981, 2021. URL httpps:/aapp..smmttiicooooooooo
semanticscholar wrw.aarussrCC/CI
23:mpp1 235421638
Kaiyue Wen, Xingyu Dang, and Kaifeng Lyu. Rnns are not transformers (yet): The
key bottleneck in-context retrieval. ArXiv, abs/2402.18510, 2024. URL https:
s/api
org/Corpussuts 268041425.
Shangda Wu, Xu Tan, Zili Wang, Rui Wang, Xiaobing Li, and Maosong Sun. Beyond language models: Byte models are digital world simulators. ArXio, abs/2402.191555 2024.
URL https://api semanticscholar wrggCorppsID: :2280p243 268063492.
Shunyu Yao, Binghui Peng, Christos H. Papadinitriou, and Karthik Narasimhan. Self- attention networks can process bounded hierarchical languages, In Annual Meeting of the Association for Computational Linguistics, 2021. URL pttps://app: semanticscholar.co org/
CorpusID: CorpuSID:235166333 235166395.
Chulhee Yun, Srinadh Bhojanapalli, Ankit Singh Rawat, Sashank Reddi, and Sanjiv Kumar. Are transformers universal approximators of sequence-to-sequence functions? arXic preprint arXi::1912.1007 2019.
Haoyu Zhao, Abhishek Panigrahi, Rong Ge, and Sanjeev Arora. Do transformers parse while predicting the masked word? arXiv preprint ar Xii::330.008117, 2023.
Hattie Zhou, Arwen Bradley, Etai Littwin, Noam Razin, Omid Saremi, Josh Susskind, Samy Bengio, and Preetum Nakkiran. What algorithms can transformers learn? study in length generalization. ArXiv, abs/2310.16000 2023. URL https: / //api. semanticscholar. org/CorrpusDD:22443911
15

---

Published as a conference paper at COLM 2025
A Tree
Trees one of the most fundamental objects to study in computer science. However, its exact definition differs for different domains. The trees used in "abstract syntax tree" (Section B) more restrictive than that in mathematics, which we call "typed tree", that one can define recursive computation more rigorously.
A.1 What are Trees
Trees in data structures have slightly additional meaning as compared trees in mathemat- ics. In this paper, all trees are trees in data structures. For clarity, we lay down the precise definition of trees in data structure.
Definition (Tree). A tree a set of nodes storing elements such that the nodes have a parent- child relationship that satisfies the following:
If T is not empty, it has a special node called the root that has no parent.
Each node of T other than the root has unique parent node w; each node with parent is a child of w.
We denote the nodes T as N(T).
Definition 4 (Recursive Definition of a Tree). A tree T is either empty or consists of a node r (the root) and possibly empty set of trees whose roots the children of
However, the above definition is too permissive. We shall define a typed version as follows:
Definition 5 (Typed Tree). A tree type consists of a set of values V and set of relationships CCV N, and typed tree under this type any tree such that for each node, a value v E V is assigned such that (v, n) E C where n is the number of the children of the node.
All trees in this paper are typed.
Example (Abstract syntax tree (AST) as Typed Tree). Consider an AST for a simple arithmetic expression. Let the set of values V be:
V
num
add
sub mul dio
and the set of relationships C C V x N specify the allowed number of children for each value:
C= num ,0), addd ,2), (sub ,2), (mdd) 2), div 2)}
An example AST for the arithmetic expression (3 - 5) x 2 is the following typed tree:
The root node is labeled mul (multiplicaatio)), and it has two children.
The left child is labeled add (addition), and it has two children:
* The left child of add is labeled num with the value 3.
The right child of add is labeled mum with the value 5.
The right child of mul is labeled num with the value 2.
This tree conforms to the typing rules because:
num has 0 children,
add has 2 children,
mul has children, all of which satisfy the relationships in C.
16

---

Published as a conference paper at COLM 2025
A.2 Representations of Trees
It's also important to talk about tree representations. We are studying transformers, and then it's necessary to represent large trees sequence, otherwise the model dimension is not large enough to contain the information locally. Let's first talk about the classical arena pattern used in system programming for representing trees and shall slightly adapt it to our use case for studying transformers.
Arena Pattern. To represent trees efficiently in memory, especially when trees are fre- quently modified (such as insertions or deletions of nodes), an arena pattern is often used. The arena pattern provides way to manage memory allocation for tree structures, allowing for efficient memory usage and avoiding fragmentation. Here's s how the arena pattern works in the context tree representation:
Definition 6 (Arena Pattern in Tree Representation), In the arena pattern, tree is represented by an array (or vector) of nodes, called an arena. Each node in the arema contains:
An element or value stored in the node.
References (often indices pointers) to the node's children and possibly to its parent.
The key characteristics of the arena pattern are:
Memory Contiguity: All nodes stored contiguously in memory within the arena, which allows for efficient traversal and modification operations.
Fixed Capacity: The arena has fixed or dynamically resizable capacity, and nodes are added sequentially. This avoids the overhead of allocating individual nodes the heap.
Index- References: Instead of using pointers, the nodes reference each other using indices within the array, which simplifies memory management and can lead to cache- friendly operations.
Efficient Allocation and Deallocation: Nodes can efficiently allocated and deallocated within the arena without requiring complex memory management techniques like garbage collection or reference counting.
The arena pattern is particularly useful in scenarios where the structure of the tree is highly dynamic or when performance critical. It allows for a simple and efficient way to manage and traverse trees without the typical overhead associated with more traditional pointer- based tree representations.
Adaptations for Transformers For transformers, inputs, intermediate values and outputs are all sequences. So the trees are represented as sequences of nodes with node reference representable by token position encoding. Based on the representation, transformers will be able to perform various kinds of recursive tree operations, as we shall see.
B Context Free Grammar
In this section, we lay down the well-known definitions of context free grammar, derivations, and parse trees. To define an abstract syntax tree (AST), one commonly resorts generation rules, such as context-free grammars (CFG) (Alfred et al., 2007) and parsing expression grammars (PEG) (Ford, 2004). In most cases, just generation rules themselves are not sufficient to define properly a language. Many practical languages like C and C++ cannot be solely described by these rules (David, 2009) so that they can reuse the limited set of special characters on the keyboard. Furthermore, semantic constraints like type correctness are intrinsically contextual and cannot be expressed through CFG or similar rules. However, CFG other rules provide valuable construct, the AST. With an AST, one refine the language definition by putting restrictions on the syntax tree through tree operations. Effectively, language can be seen subset of trees, not subset of strings. Semantic
17

---

Published as a conference paper at COLM 2025
analysis like symbol resolution and type checking can be described effectively based on trees. In short, CFG standalone hardly practical but it provides useful and clear foundation to build definitions upon.
context-free grammar (CFG) is defined as a 4-tuple G (V,,, where:
a finite set of variables (non-terminal symbols).
Σ is a finite set of terminal symbols, disjoint from Sequences of Σ, i.e, elements of nx are called (literal) strings.
R V x (VUZ) WU)" is finite set of production rules, where each rule is of the form + a, with A E and (VUE)*
S E V the start symbol.
Given context-free grammar G (V, define derivation as follows:
A derivation is sequence of steps where, starting from the start symbol S, each step replaces a non-terminal with the right-hand side of production rule.
Formally, we write u = v = aAβ and v = an for some production A + in R, where a, (VUE)* and A
A leftmost derivation is derivation in which, at each step, the leftmost non- terminal is replaced.
A rightmost derivation a derivation in which, each step, the rightmost non- terminal is replaced.
We denote a derivation sequence as S + w, where w E Σ* is string derived from S in zero or more steps.
parse tree (or syntax tree) for a context-free grammar G (V, V, is a tree that satisfies the following conditions:
The root of the tree is labeled with the start symbol S.
Each leaf of the tree is labeled with terminal symbol from Σ or the empty string
Each internal node of the tree is labeled with a non-terminal symbol from V.
If an internal node labeled with non-terminal A and has children labeled with
X1, X2,...,, Xn, then there is production rule A + X₁ ... X,, in R.
The yield of the parse tree, which is the concatenation of the labels of the leaves (in left-to-right order), forms string in E" that is derived from the start symbol
C Neural Architectures
In this section, we lay down the precise mathematical definitions neural architectures we going to use in our proof.
Definition 7 (Single-Layer Fully Connected Network with 4x Intermediate Space).
Given model dimension dmodett. a single-layer feed-forward network with an intermediate space expanded to 4 times the input dimension is a function from Remd to RRdmotd denoted by ffm and defined as follows:
given X E Rdmmde, weights W1 E IR 4olmodd X modde W2 E Roddd x 4dlmadd, and biases Bj E RR Radmmadd
B2 E Rmasdd the output fjen (X) is computed as:
fan = WOOReLU B1) + B2,
where UReLU Adumee + mdulel is the Rectified Linear Unit activation function applied element- wise, defined by:
18

---

Published as a conference paper at COLM 2025
ORLLU(Z) (max(z1, 0), max .)..., max (Ad (sdmeer))) 0))²
for z (Z), 22,........ ................................ madmmats) ) R-ldmadel
The choice of 4x intermediate space is common in practice, often used in Transformer architectures. Interestingly, this empirical choice turns out to have useful theoretical property: it allows the network to express any affine transformation, as we'll see in the following proposition.
Proposition 1. A single-layer fully connected network with 4x intermediate space, defined previously, express any affine map from RRamdd to Rodddd.
Proof. Let f Roddel Ramddel be any affine map given by f(X) AX b, where E RRdmoded xdmodel and b E Rdmmaeel We will construct weights W1 E TR Xdeawdel
W2 E Rdmodd x 4dmodel and biases B1 E R Radmodel, B2 E R Reddel such that fie(()) = f(X)
for all X E R9dodde
Define:
Idmodel
W1 =
modded
B1 =0 IR 4lodeel
where Lamodel is the model x dmodel identity matrix, and 0 represents zero matrices of appro- priate dimensions. Set:
W2 = (A A 0), B2 = b.
For any X E Rodell compute:
fia(()= W2 ReLU (WiX + B1) + B2
-X
(A - A 0 0) R
+ b
0
0
CReLU (X)
ØReLU (-X)
(A A 0 0)
+ b
0
0
A TRRLU (X) AOReLU (-X) + b.
Note that dReLU (X) TRCLU (-X) X, we have:
fien (X) = AX + xx=
Therefore, the network can represent any affine map from RRdmodel to Rdmodel,
Definition (Single-Layer Feed Forward Network with 4x Intermediate Space). Given
model dimension &madd and position set Pos, the Transformer Feed Forward Network is a function fy.: R xdmmadd - Ros xdmadel defined as follows:
For an input X E Pos xdmatd, the output frn (X) is computed by applying the single-layes feed- forward network fjen (as defined previously) independently to each position:
fgu (X), = (Xp) Vp E Pos
where Xp E RRumsddd is the p-th row of X, corresponding to the p-th position in the input sequence.
19

---

Published as a conference paper at COLM 2025
Next, define the attention mechanism, which is a key component of the Transformer architecture. This definition presents a hard attention layer with a simplified position encoding. We use hard attention here for theoretical simplicity, it represents discrete limit of the more commonly used soft attention mechanism. Hard attention forces the model to make clear choice about which inputs to focus on, which simplify analysis and provide clearer insights into the model's behavior. It can be viewed as the limiting case of soft attention as the temperature approaches zero, where the softmax operation becomes increasingly peaked and eventually converges to one-hot vector.
Definition (Hard Attention Layer with Simplified Position Encoding). Given model di- mension model, number of heads H, and number of layers L, transformer with simplified position encoding and hard allention defined to be function fattn IR xdwsid - IR xdmadd defined by
vp E Pos, faun (X)p = WoConcal
(Atn!) (X])))-)A)
(4)
where the hth attention head uses hard attention, defined as:
1
vhh p'
Attn (X)p
Σ
(5)
Spp
p P'ESp
where
Wo E Rinddd Xdmaddi are trainable parameters;
arg max pa (O
+1 (1))Tp xp-pp) with Q,"h) K/ v/(), (1()),10) A000, Yg defined
Sp
K p'
by
- - = w(th Xp, Kp wh()) Xp are vectors of dimension dmoaet/ / H, with trainable parameters with) whtl) R H) mmmit
vith w! Xp are vectors of dimension / / H, linear transformations of Xp with trainable parameters w(() IR (dmmsee / H) xdadds
-k) E I2 are constants depending only on head count h;;
4g IR2 are 2-dimensional veclors depending relative position q but not on head
count h. It is explicitly defined as
Yg yy= (1200)
(1=010)))
9
(6)
This formulation allows for both past and future masking.
Having defined the basic components, we can now proceed to describe the full Transformer architecture. This definition builds upon the previously introduced concepts, incorporating them into a complete model structure.
Definition 10 (Transformer). A Transformer is function fy: IRPos xdmase - IR Pos x dd
that maps an input sequence to an output sequence through series of layers, each consisting of multi-head attention mechanism and a pusition-wis feed-forward network (MLP).
Given:
Input sequence X E Pos x xdmald, where Pos the set of positions and d is the model dimension.
Number of layers L..
Number of attention heads H.
The Transformer computes the output Y = (I)) through recursive application of attention and feed-forward layers:
20

---

Published as a conference paper at COLM 2025
Initialization is given by:
x X.
For each layer = 1,2,...,
Compute attention output:
X10 = -x(1111) + (x((-1))
Compute feed-forward output:
x = 811) +
(l)) fffr (X(1)
Here:
attn are hard attention layers with simplified position encoding as previously defined.
It operates on x(!-1) and produces output in IR xdmiiee
fin are feed-forward networks with 4x intermediate space as previously defined. It operates position-wiss wise on x()) and produces an oudput in IRPos xdmaad!
Remark 1. For simplicity, we have omitted the Layer Normalization component typically present Transformer architectures. This simplification allows us to focus on the core attention and feed-forward mechanisms while maintaining the essential structure of the Transformer.
We use TFimndel to denote the set of transformers of model size model, number of heads H and number of layers L as functions from dudded to mode!!
For purpose proof, we shall also need residual multi-layer perceptron. Functions over local types are first represented by multi-layer perception, then by Proposition 2 applications of these functions over sequences can be representable by transformers. Residual multi-layer perceptron can be assembled through composition computer graph, as we shall see.
Here's the definition of a residual MLP Network.
Definition 11 (Residual Multi-Layer Perceptron). A Residual Multi-Layer Perceptron (ResMLP) is function fresmdp: Rmdmad + Rdmade defined recursively by
( = X, x = x(1-1) + fyen (x 1 fresmip (X) = X(L)
where X E Ausded is the imput vector, L is the total number of layers, and ffon Romaee Ramddel is the Single-Layer Fully Connected Network with 4x Intermediate Space previously defined in Definition 7.
We use ResMIpmaade maddel C @mdde IR model
to represent the set of residual MLPs with dimension modeel and L layers, defined in Definition 11.
The following proposition is quite basic. It demonstrates that any function representable by ResMLP can be applied position-wise by Transformer.
Proposition (Position-wiss ResMLP Application is Representable by Transformers). Let f amdrd + Rmmas be a function representable by a Residual Multi-Layer Perceptron (ResMLP)
as defined in Definition 11. Then the function F PoPos xdmsid + Pos xdmats, defined by applying f position-wise,
F(X); = f(p)), Vp E Pos,
is representable by Transformer defined in Definition 10.
21

---

Published as a conference paper at COLM 2025
Proof. Since f representable by ResMLP with L layers, it is defined recursively by x X, x(1) x(1-1) + ften (x(l-1)) for I I,...,L,
and
((x)= =
where fren
Rd - Rd the Single-Layer Fully Connected Network with 4x intermediate space (Definition 7).
We construct Transformer with L layers such that, for any input sequence X E R Pos x model, the output = (x) satisfies Yp = fXpp) for all E Pos.
To achieve this, configure the Transformer that the attention mechanism outputs zero at each layer. This can be done by setting the attention weights to zero, ensuring fattn (x((-1)) = 0. Consequently, the update equations simplify to
x0) x 1),
We then set the feed-forward network ftm in the Transformer to have the same weights and biases as fien in the ResMLP. The Transformer layer update becomes
x (1) = 00) + ftm (XD) ((-11) + (fren (x, (x) PEPos
This recursion matches that of the ResMLP applied position-wise to X. Therefore, after layers, the Transformer output satisfies fu(X), = f(Xp) for all p Pos.
D Cybertron
D.1 Introduction
It's often difficult to directly prove that transformers or in general other low level forms of computation can express complicated algorithms and even complex software. There are way too many details compared with typical mathematical proofs in machine learning theory. Hence, we propose the domain specific language Cybertron, where we can system- atically prove transformers can express complicated algorithms and complex software with sufficient readability.
(Note: Cybertron is fundamentally different from Mini-Husky! Mini-Husky is the target lan- guage that we want transformers to analyze yet Cybertron is the domain specific language use prove that transformers
do that.)
RASP (Weiss et al., 2021) is quite close to Cybertron terms of its design purpose. However, Cybertron is more powerful with advanced algebraic type system, global and local function constructions, etc. These additional mechanisms replace significant part of the chore in proofs with automatic type checking. Thus, using Cybertron one can argue operations more complicated than simple algorithms can be simulated by transformers.
In the broader perspective of computer science, it's common to use code to prove things. In fact, in the formal verification community, mathematical proofs are viewed as special case of a much larger universe of possible proof systems (mathlib Community, 2019; Massot, 2024) and constructive proof using code (Harrison et al., 2014; Farooqui, 2021; Jung et al., 2018) is far more applicable with great soundness to the most general settings. In our case, our code doesn't t serve the whole proof but as an important part that contains most of the chores. However, it's totally possible to build a full-fledged formalized proof, despite might be too costly for single paper to do.
Essentially, Cybertron works as follows:
1. one builds complicated functions from the composition of smaller functions. We have lemmas that prove that the composed functions are representable by certain architectures given that smaller functions representable.
22

---

Published as a conference paper at COLM 2025
2. there is an algebraic type system and every value is strongly typed and immutable, making it highly readable and easy to reason about;
3. there is distinction between global and local types/ /functtonssss. Local types are those information hovered over single token, and global types are sequences of local types, i.e., the collection of information over the whole token stream. One can define global function by mapping local function.
4. there are many functions that is defined externally, requiring external explanation that they can be represented by transformers.
It's implemented as a subset of the Rust programming language that can be understood as computation graphs over sequences. It can be executed for testing purposes and we've tested our implementation for range of inputs and validated its correctness.
D.2 Philosophy: Sequential Representation of Everything
Before going through the full details, let's first talk about the fundamental philosophy behind fransformer and Cybertron.
One of the fundamental reasons transformers can be easily adapted across multiple modal- ities, including NLP and CV, is their prruence-to-squeene operation. Everything can be represented as an arbitrary-length sequence. Texts are sequences of words, images are se- quences of image patches, videos are sequences of spacetime patches (OpenAI, 2024b), and even graphs with sparse spatial structures can be represented as sequences of indexed nodes with additional information like parent node indices. Since inputs of various modalities can be cast into vector sequences, transformers can be applied to different domains without modifications to their architecture (Dosovitskiy et al., 2020).
Interestingly, this sequence-based thinking is not new. We've actually been representing everything as sequences since the very early days of computer science. This has been the foundation of how data is stored and processed in computers. However, sequence repre- sentations were traditionally viewed as low-level and sometimes inefficient for practical use, prompting the development of higher-level abstractions for programming. The rise of transformers, with their scalable learning capabilities, encourages us to reconsider the significance of sequence-based representations.
From systems perspective, viewing everything as a sequence the foundational approach in computer science. Data in computer is stored continuous stream of bits. Whether it's text, images, videos, or graphs, this data is represented in computer memory as an ordered sequence of bits. This aligns with how transformers handle different types of input by transforming them into sequences of vectors. Thus, the sequence-based operation of transformers mirrors the sequence-basee representation of data in computer memory.
In essence, if a data structure can be represented in computer memory using N bits, it can be processed as sequence of bits of length N. This natural sequence representation in memory is consistent with how transformers process data, which makes them particularly flexible across different modalities. For example, recent state-of-the-art approaches Wu et al. (2024) show that transformers can even be trained directly on raw bits of data, further emphasizing this connection.
Moreover, this sequence-based viewpoint offers fresh insights when applied to the domain of programming, particularly in areas such as code generation and analysis. With tools like ChatGPT and Copilot being widely used by developers, the impact of transformers on programming workflows is growing. Understanding the complexity algorithms and programs expressed in sequence form becomes an interesting area of study, as it reveals new possibilities for how we approach computation.
In comparison to traditional systems like CPUs and human cognition, transformers are highly parallel but shallow in their operation. A transformer processes data in a fixed number of layers, while a CPU executes 10 cycles per second, and humans may take days to process information like reading book. Transformers, therefore, represent
23

---

Published as a conference paper at COLM 2025
fundamentally different computational model that is worth studying further in the context of sequence-based operations.
Example 2. Image to Sequence: In computer memory, an image is typically stored as continuous block of pixel values, often in row-major order, where each pixel's value encoded as bits in sequence. When a transformer processes an image, it divides the image into patches (e.g., 16 x 16 pixels), and each patch is flattened into a vector of pixel values. This creates a sequence of patches, where each patch corresponds to vector. The way transformers represent these patches as sequence closely aligns with how the image data is sequentially stored in computer memory.
Example 3. Video to Sequence: A video is stored in computer memory as a sequence of frames, where each frame is essentially an image. In a similar manner to images, these frames are stored as continuous pixel values. Transformers process videos by dividing the frames into spacetime patches, where each patch captures a small region of space over short segment of time. These spacetime patches are flattened and arranged into a sequence for the transformer to process. The sequential ordering of these patches matches how video frames and pixel data are stored in computer memory.
Example 4. Graph to Sequence: In computer memory, a graph is typically stored using an adjacency list or adjacency matrix, where nodes and their connections (edges) are stored sequentially in a data structure. Transformers process graphs by representing each node and its features as a vector, and then creating sequence of these vectors. The sequence may also encode additional information, such as the parent-child relationships between nodes. This sequence-basee based representation of graphs is consistent with how graph data stored in memory, where nodes and edges are arranged in structured order.
Example 5. Text to Sequence: Text is naturally stored in computer memory as sequence of characters or words, where each character is encoded as a sequence of bits (such as ASCII or Unicode values). When transformers process text, they convert each word into a word embedding, which is vector of real numbers. The sequence of word embeddings corresponds to the sequence of characters or words stored in memory. This natural sequential representation of text in both memory and transformers ensures efficient handling of linguistic data.
In computer memory, an abstract syntax tree (AST) is typically stored as a tree-like structure, where each node represents a component of the program (e.g., operators, variables, statements). However, this tree can be linearized into sequence by traversing it in a specific order (egg, pre-order traversal). When transformers process an AST, they convert it into a sequence of tokens, where each token corresponds to a node in the tree. This sequential representation of the tree in transformers mirrors how the tree is stored as nodes and edges in memory, and how it can be flattened into a linear sequence.
Example 6. AST (Abstract Syntax Tree) to Sequence:
In conclusion, the sequence-based representation in transformers is not just novel approach for deep learning but is deeply rooted in how data has been stored and processed in computer memory since the early days of computing. This consistency between how data is stored in memory and how transformers process data as sequences is key factor in their adaptability across different domains.
D.3 Local and Global Types
Now we define the type foundation of Cybertron.
Types are fundamental objects for programming language theory. Here we use types to faciliate our proofs. Type signatures contain rich information that help guarantee correctness of the program. Here, we choose a mathematical definition of types that is most convenient for the discussion in this paper. We introduce the notion of "local type". Roughly speaking, they are types without heap allocation and intended to be represented with model over a single token. For more complicated heap-allocated data structures like trees, graphs, etc., we shall represent them by sequences of these "local type"s, s, which translate directly to vector sequences for transformers.
Definition 12 (Local Type). Given a base space B with at least two elements and a countably infinite identification space Y, local type T over B is a finite set S together with an embedding & from S to Bd and some fixed d E IN and identification up E Y.
24

---

Published as a conference paper at COLM 2025
For convenience, define Set (7) S, dt d and ΦT 4 and 4T And let Og, and 1B be two different elements of B. And B == {0g} so that B¹| = |B]' holds for all i IN.
We need B to be at least size 2, that B can be as large large enough.For typical computer representation, we can take to be = {0,1}. For transformers neural networks in general, we take to be R if we ignore precision. we don't ignore precision, B should be some finite set of floating point numbers. Thus, we shall keep the generality of B throughout our discussion as all of these settings are important.
Remark 2.
want for d
The role of identification yf E Y is to make two types mathematically different even if they have the same underlying set, encoding dimension, and encoding. Basically we are establishing specialized type of theory tailored towards the expressive power of transformers upon a foundation of intuitive set theory.
Remark 3.
Example (Finite Set). In mathemalics, we have the finile set denoled by [n] {0, 1,, 1, -1].
Here we use slightly different notation for a type with underlying set [n]] and some encoding.
Example (Position Encoding). Position encoding can be viewed the encoding of a type denoled by Pos (πt with the underlying set being [n] where n is the context length. Although it has the same underlying set as type [n], is different type for a different purpose and might have different encoding.
If B is IR then the position encoding can be understood as the encoding of type [L] where the context length. More explicitly, we have
((x) = (c u1x (
viewed d dimensional RRvector through the natural conversion of C to R2, since d is even.
It's too cumbersome to manually give the underlying set and the encoding. Here we introduce classical concept from programming language theory Program (2013) that makes it super easy to construct new types and make things fairly readable.
Definition 13 (Finite Algebraic Data Type, Mathematical Forms). We define two ways of creating types by combining existing types:
1. Sum type. Given types T; (S 15,,4i.e d;) over base space B for i = 1,..., n, we define the sum type of Ti, denoted by
Σ Tú, as follows,
let ({1} x S1) U... ([n} Sn);
let d[d] + max" de
let S + Bd be such that
Bdt C Bd vi [n].s s (i,s(( P[m (i) (ss))=
(8)
Note that [S] =1 [s,), thus the name sum type.
2. Product type. Given Local Types T; (S;, Di, d;) over base space B for = 1,... we define the product type of Ti, denoted by [I Te, as follows,
let S x ... Sni
let Dn dig
let Φ S Bdd be such that
vs = (s sn) E S, (5.)(ss)))))))))))) ( e (n(s)) E Bd.
(9)
Note that [S] [ S thus the name product type.
Although we can define things and refer to things in terms of mathematical equations, it's sometimes cumbersome to do so. So we shall frequently refer to types using programming language form, like CybertronFormm or more complicated things like Option<T> a builtin generic type.
25

---

Published as a conference paper at COLM 2025
Definition 14 (Unit Type). The unit type is type with {0} and Φ : B,, Og. In Cybertron, it's denoted as (
Definition 15 (Array Type). Given a type T, the array type T with length E IN is the type with S = S(T)), d EdT and Φ S + Biår, (s1))..,88) + 4T(s)) ( t.... @ fT (st). It's denoted by T In Cybertron, it's denoted as [T:N]
Definition 16 (Vector Type of Finite Capacity). Given type T, the vector type of finite capacity of with maximal length E IN is the type with U Set (T),, & : B +låT, (s))...,,:) + (1q(1) @ (s) @ ... (T())) @ Og @ ... @ Og with just enough number of copies of Og such that the dimensionality matches. It's denoted by T In cybertron, it's denoted as VoundedVec<T,N>>>
d[d + ldy and
However, it's cumbersome and obtuse to define and operate in mathematical forms only. So shall give definition closer to actual programming that is more convenient and easy to read.
Definition 17 (Finite Algebraic Data Type, the Code Forms). We define fwo ways to create new types:
1. Enum type. An enum type is the sum type of a finite set of variant types. Each variant type is associated with a different identifier and can be
unit like, unit type;
struct like, a product of several types, each called a field of the variant, and associated
with an identifier;
tuple like, product of several types, each called a field of the variant, but not associated with an identifier.
Syntactically, an enum type is specified as follows,
enun <type-nane>
<identifier>
variant, struct
<identifierr: <type>, /1 1st naned field of 1st variant <identifier:: <type>, 2nd naned field of 1st variant
). <identifier>
variant, struct like cidentifiers: <type>, // 1st field of 2nd variant
). <identifiers c
11 3rd variant, tuple like
<type?,
11 1st tuple field of 3rd variant
13
<type>,
1/ 2nd tuple field of 3rd variant
15
<idencifiers,
variant, unit
For example,
enum Expr (arishhe(IdentToken), Binary {
variant, tuple like
3
// 2nd variant, struct like
lapd: ExprId,
5
opr: Hinarytprroken,
ropd: ExprId.
8
Prefix (
// 3rd variant, struct like
cor: Prefix0prToken. opd: ExprId,
10
Suffix (
11 4th variant, struct like
opd: ExprId, opr: fixdixcpr
15
variant, unit
17
26

---

Published as a conference paper at COLM 2025
2. Struct type. A struct type is just the product type of
struct <type-nane> {
<identifier>: <tyge>, <idencifler>: <type>,
struct
2
8: 132
To show how convenient this is, we can define the very useful option type as follows, Definition 18 (Option type). For a local type T wo can define an option type as
Option<T>
STme(T),
Definition 19 (Global Types). Global types are defined to be sequences of local types.
Example 9 (Representation of Graphs). Graphs can be represented sequences of its nodes. We can use position index to use as node references.
D.4 Computation Graph
For convenience, we shall use computation graph as a vehicle to describe complicated computation processes. Computation graph is close to actual computation process and one can derive an understanding of the computation difficulty from the graph's mathematic properties (width, depth, etc.)
Definition 20 (Directed Simple Graph). A directed simple graph G is pair (V,E) where V is finite set, and E C V x V is called edges.
In the following, we shall simplify the "directed simple graph" to just graph.
Definition 21 (Computation Graph). A computation graph is an acyclic directed graph G =
additional (V, E) with additional structures:
1. for each vertex V, there is an associated type, denoted by Toi
2. for each vertex v E with a positive number of incoming edges, let UI,..., Un be the other verlices for the incoming edges, then there is an associated function fo from Toy x Top to T
computation graph naturally generates a function from source vertices to sink vertices.
Let uin .i....., uin be the set of vertices with no incoming edges, and let your ..... your be the set of vertices with no outgoing edges. Then we can construct function from Twpn x T Tiin
to T Too X ... x T pout in the following obvious manner:
1. let (xi xn) Toi .... x Top be input;
2. for each oih assign it with value x;
3. for each vertex E V with all its incoming vertices vi,..., assigned with value, assign it with the value fo Xx,) where Xuy denotes the value assigned to dy
4. repeat the process until all vertices assigned value, then take (X.qut,-... Xogst) as the output.
Our goal is to make a hypothesis class using the above graph. To control the statistical and computational complexity, we put restrictions the choice of Tи and fo, as follows:
27

---

Published as a conference paper at COLM 2025
Definition 22 (Restricted Computation Graph). Let U be set of types, and for any A, B e u, there is set of functions Mor(A, B) from A to B. We require that Ter Th" U and fo E Mor(T To) where T II To'. We also require that the underlying graph satisfies certain d'vEE
conditions (width, depth, etc.)
Definition 23 (Restricted Computation Graph Of Sequences). Lef U be universe such that for set of types Mg all types in li are of the form A" for some type E Mo, and Mor A",, A,, B*) are functions that preserve sequence lengths.
Given a restriction, the class of functions generated by restricted computation graphs is the central object to study in this paper. We shall use an even more restricted computation graph of sequences. We shall argue about the class of functions formed that
1. it's rich enough to contain many interesting operations including SQL, compiler (type inference, static analysis)
2. it's computationally reasonable, and can be represented by transformers with pragmatic bounds
3. it has reasonable statistical complexity
As a corollary, our theories suggest that transformers can possibly learn to do many interest- ing things with reasonable computational and statistical complexity.
To our knowledge, this is the first theoretical paper that gives pragmatic optimistic bounds for the power of transformers in wide range of meaningful language tasks.
Now we introduce theory.
measures that will play key roles in our new complexity
The most basic one the following:
Definition 24 (Depth of Graph). The depth of computation graph is defined to the length of the longest path, denoted by dg-
For convenience, we define the following vertex-wise depth.
Definition 25 (Depth of Graph Vertex). The depth of verlex of a compulation graph is defined as the length of the longest path with end v, denoted by da-
The smaller dG is, the more parallel the computation is.
However, we shall discuss a more nuanced measure, containment, as follows:
D.5 Functions over Local Types
Definition 26 (Functions over Local Types). Given Local Types T, R. the functions from T to R are defined to be just the functions from Set (T) to Set (R).
Remark 4. The domains and codomains are all finite sets, so there aren't 't many constraints we want to enforce here. Basically, these are "discrete" functions.
Definition 27 (Functions over Algebraic Data Types). Let T, ,,,...,, R. be Local Types, and suppose that is an algebraic data type, then we can construct functions from x S ... Sm to R as follows,
1. suppose that 'T is the sum type of Ti.... Tn- Then given functions fi T₁ x S1 Sm for i = 1,...,, we can construct function f, by letting
f((i, t), St..., Sm) = f(.., Sm E Set (Sm)-
(10)
for each E Set (T)), $1 E Set
(Note that we use the pair (i,t) because the underlying set of T is LI {i} x Set (Ti).)
2. suppose that T is the product type of TT...., TT. Then given a function fo Ti x ... Tn S x x Sm for 1,..., n, we can construct function f, by letting f((1...,,, (1), si. Sm) fo (4 .. S1..S...... Sp....5mm)
(11)
28

---

Published as a conference paper at COLM 2025
for each E Set (T)), $1 Set (Si)...., Set (Sm).
It is not enough to just mathematically construct. We should also discuss how neural networks can represent these functions. We define the representation of functions over Local Types formally as follows:
Definition 28 (Representation of Functions over Local Types Using Multi-Layer Perceptions). Let TT, R be Local Types. Given function f from T to R, we say it is representable by MLP of dimension 2 max (dy, ,R) and number of layers L, if there exists f E ResMlpf such that
O RR of f 12 QT,
(12)
where 1 RR Rd and 12 IRAT - Rdd are the canonical embeddings by putting zeros to fit the dimensionalities.
Here are some trivially true facts:
Proposition 3. [Identities are Representable] For any Local Type T, the identity map 1dy is representable ResMlp AT
Proof. Just take w/" = la, w()) = 0, =
= 0. -
Proposition 4. [Fquality is Representable] The equality function for any local type T is representable in ResMlp? 2d where is the encoding dimension of T.
Proof. Let x, be the inputs. We encode them (x),)) (v) E Rd. The equality function can be represented as:
fxg(x,y) = min 1, Σ p (x); - 4 (x)=
where A is large enough positive constant such that the RHS is either or 0. This can be implemented in two-layer ResMLP with dimension 2d.
Proposition 5. [Boolean NOT is Representablel The Boolean NOT function is representable in ResMip].
Proof. It's affine.
Proposition 6. [Boolean AND is Representable] The Boolean AND function is representable in ResMip
Proof. Represent each Boolean value as a binary flag within 1-dimensional vector. Then AND is just taking the minimum. By min b) 0ReLU (b - a), we' 'e done.
Proposition [Boolean OR is Representable] The Boolean OR function is representable in ResMlp
Proof. Represent each Boolean value binary flag within 1-dimensional vector. Then OR is just taking the maximum. By max(a, b) = a + &ReLU (b a), we're done.
Proposition 8. TTHENSOMM is Representable] The function Bool:then_some Bool T
Option T returns Some t if the boolean is true and None otherwise. This function is representable in ResMlp d+1
29

---

Published as a conference paper at COLM 2025
Proof. Encode the boolean binary flag in (d+ 1)dimmesiion vector, where the first component indicates the boolean value and the remaining components hold the value of type T The residual MLP fremlp constructs the output Option I by assembling the flag and the value split into positive and negative parts influenced by the flag:
X1 rresmpp (X) (oRALL (I2nd Axi) ReLU (-x2-/11 -x11)
Here, A is vector of dimension with all entries positive and large enough to ensure proper thresholding. Specifically, each entry of A should be larger than the maximum absolute value that can be represented in the corresponding dimension of type T This ensures that when x1 = 1, the subtraction x will always be negative, and when
X1 = 0, it will not affect the value.
When the flag is true (x1 = 1), ReLLU (X2.4+1 A) = 0 and ReLU (- 22d+1 A) retains the negated value, resulting in Some When the flag is false (x1 0), both ReLU terms preserve the value, yielding None Thus, fresmip effectively implements Bool:then some within single layer of the MLP.
Proposition 9. [Option Or is Representable] Let T be local type, let Option:or be the function that maps two values a,b of type Option T to value of type Option T such that is equal to when a is not none, and equal to b otherwise. Then Option:or is representable in ResMlp 2(d+1)
(d + 1)ddieensional vector, where the first compo- nent is binary flag indicating the presence (1 for Some 0 for None), and the remaining components encode the value. Given inputs a, Option T, the residual MLP fresmip processes the concatenated vector
Proof. Each Option T is represented
Aflag
Qval
X
baag
bval
The MLP designed to separate bval into positive and negative parts (b+,b- respectively) influenced by Alaa. Specifically, it computes:
fremmpp (X) aval + RRLLU (b+
Aanag)
RRRLU
(b-
AdAag
(13)
dval + ØReLU
(bval
AAnag)
UReLU
-byaal - AAnag)
where A is vector with large positive entries that ensures the ReLU activation zeroes out the non-selected parts based on the flag. When faag 1, the terms involving b are suppressed, resulting in Conversely, when Aflag = 0, the positive part of remains, effectively selecting Thus, fresmip accurately implements the Option:or function, demonstrating that 2(d+1)
representable within ResMIp 2(sM)p((d+1)
Proposition 10 (Field Access Is Representable in ResMlp). For algebraic data type, either struct field access, enum discriminator, and variant field access can be represented in ResMIp where is the encoding dimension.
Proof. Obvious because these operations are linear.
Proposition 11. [Composition of Functions Representable in ResMlp] For local types S,S,P R, d2 with maps f T S and map g S + R representable in ResMlp; and ResMlp respectively. Then go f is representable in MesMilpaaxddhaa) d2)
30

---

Published as a conference paper at COLM 2025
ΦT (x)
L1 layers MLP
fs(((x))
Le layers MLP
(
Figure 3: Transformation from (x) to (s(f(x)) to ΦR (8(f(x))) with MLP layers.
Proof. Obvious by using the first L layers to map from T to and using the rest L2 layers to map from S to R. The process can be visualized as in Figure 3.
Proposition 12. [Compulation Graph of Functions Representable in ResMip] Let G be compu- tation graph, with each veriex being of some local type To, and the construction functions are representable in ResMlpL; For convenience, if v is source verlex, du is defined to be the encoding dimension of To and La 0. Then the function induced by the computation graph is representable Encg in PesMippephiie [ (max.sg 1++1)++
Proof. We construct a global residual multi-layer perceptron (ResMLP) that simulates the computation graph by aggregating and updating the states of all vertices simultaneously. Let D = Loeg dy be the total dimension, where dy is the dimension associated with vertex v. The global ResMLP will have depth of Depth(9) (max, L. 1).
Consider the concatenated state vector ((t) E RD, which is a concatenation of the states of all vertices:
(
(x())
DEg'
where x!" Rd is the state of vertex at layer f.
Initialization occurs at depth zero, corresponding to the source vertices of the computation graph. The state vector (0) is set by assigning the input vectors to the source vertices and initializing all other vertices to zero. Formally, if Vi denotes the set of source vertices, then:
Xxo 0
if o E Vo, otherwise,
where xa E Rd is the input to source vertex v. Because x is of dimensionality dp equal to the encoding dimension, this agrees with our convention for representing functions over local types.
We proceed inductively over the depth levels of the computation graph. For each depth level k = ,,2, 9), we perform the following steps in the global ResMLP.
1. Input Aggregation Layer. We apply linear transformation to gather the outputs from the predecessor vertices of each vertex at depth k and feed them as inputs to
these vertices. Specifically, we define a linear mapping wik) E RDxD such that:
(())
w(k)) x((x-)),
where 4-11 is the layer after processing depth k - 1, and (()) is the aggregated input for the vertices at depth k. The matrix ((k) rearranges and combines the outputs from predecessor vertices to provide the correct inputs to each vertex at depth k. Specifically, for each vertex a at depth k, and for each predecessor u of v in
the computation graph, the matrix wi(k) contains entries that copy the output of into the input positions of v. All other entries in (i(k) appropriate.
"agg are set to zero or identity as
31

---

Published as a conference paper at COLM 2025
2. Local Computation Layers. For each vertex at depth k, simulate its local ResMLP of depth Lp. Since the depths Le may vary, we pad the local ResMLPs to have uniform depth L max, Ly by adding identity mappings where necessary. The updates for vertex v are computed as:
x 11] x(t))
+ frenz (X!+))
X x((tt)) x((++(-1) frono (x)ttH--)), for k' = 2,...,, Lo
x((+tt x((++k-11 for K = Lo I,..,,
Here, ftens denotes the single-layer fully connected network (as per Definition 7) for vertex v.
3. State Update. After completing the local computations for depth k, update the global state vector X L) by concatenating the updated states of all vertices:
x(++ = xtft LL)
VEg
The total number of layers added for depth k layer and the L layers simulating the local ResMLPs.
accounting for the input aggregation
By repeating this process for each depth level k 1,2, ... Depth simulate the entire computation graph within global ResMLP of depth Depth (max, Ly + 1).
Lastly, we use the final layer to perform linear mapping so that the output is in the correct linear representation, clearing out the intermediate values.
Therefore, the function computed by the global ResMLP is equivalent to the function induced by the computation graph 9, and is representable in
L,+1))
Remark 5. We only prove things around MLPs here. Later, we shall show that this will imply that the induced map operation over sequences can be represented by transformers.
D.6 Functions over Global Types
The task want transformers to express is too complicated to be cleanly described in one shot. So we introduce the following lemma to significantly simplify things. The lemma shall be useful for future papers this topic.
Proposition 13. [Composition of Functions Representable in Transformers] For local types T, S, R, with maps f T > S" and g S" + RR representable in TFh Then the composition g o is representable in Tpmax(d, "max(H,,H2)44
H,.4 and Tp2 respectively. H2,42
Proof. This is basically the same as the proof Proposition 11.
Proposition 14. [Compulation Graphs of Functions Representable in Transformers] Suppose we have a compulation graph G -(V, with types To ту logether with encoding map 4o T > d and decoding map Φ. -R - To, satisfying db th = idy,, and there exists some positive integer do such that for each V, fo can be represented in
Tel TftLL
Let be the function generated by the computation graph. Then f can be represented in TFe if d > E. du + Hdg. I. > | dg where de is the depth of the graph.
Remark 6. This doesn't t really cover the above. The bound in Proposition 14 isn't always tight for model dimension when the computation graph is deep and Proposition 13 complements it.
32

---

Published as a conference paper at COLM 2025
Proof. WLOG, assume that d
Loev do + Hdo. Then
R"
- ADEV
R
- bE(H
Rd
(14)
Here C stands for "cache" used for storing computed values, and stands for "active" used for storing intermediate computation results.
Make an order of all the nodes in the graph, say V = UI, Vi,..., G such that Depth(u;) - (D) if f j.
We now imagine the transformer computation process as gradually evaluating the value of each vertex, starting from 2y to lI Every max, La layers form a layer group, and after each layer group, at most H vertices are assigned values. The equation 14 implies that we have enough memory to cache the computed values and intermediate values in small transformers.
Now let this process continue until we compute all the values. It must be finite because after each layer group, at least one of the vertices is computed. But this bound too loose. We claim the following:
Claim: the number of layer groups where less than H vertices are assigned values is smaller than De).
Sketch of Proof of Claim: for any layer group where less than H vertices are assigned, all the vertices that aren't 't assigned after this layer group must have larger depth than any vertices that are assigned values before this layer group, otherwise such a vertice can be evaluated in this layer group. Define the depth of any layer group to be the smallest depth of vertices evaluated in this layer group. Then for any unsatiated layer group, it must have larger depth than the previous layer group. But depth can only increase Depth(G) times, thus there are at most Depth(Q G)) unsatiated layer groups.
Proof of Claim: let Vi...., Vú be the vertices evaluated at each layer group, Note that is different symbol than and means that the number of layer groups rather than the number of layers.
For convenience, let D, be the minimum of the depths of vertices V₁.
Suppose that the ith layer group is unsatiated, then i < J. We want to show that D, < D, 1+ Suppose otherwise, i.e,, D; = D Because the ith layer group is unsatiated, for any Vi+1 must have dependencies that haven't been evaluated before the ith layer group. Choose Do E V,, V E Vi+1 such that Depth = Depth(o1) = D; = Di+1. Note that any dependency of V1 must have smaller depths than vo, then must have already be evaluated before the ith layer group. Contradiction!
Now given the claim, we have that for all but most Depth(G) choices of i 1, 1,...,I, we have Vi| H, then we have
|G|
V 2 (1 Depth(G))
(15)
Then I < G H + Depth(G).
Then max Ly
G + +e)pth(G) maX
Proposition 15. [Nearest Left/Right] For any local type T, consider the function that maps a sequence of type Option<T> to nearest left/right neighbors that are not none. It's representable in T
33

---

Published as a conference paper at COLM 2025
Proof. There is only one layer and one head needed, omit the layer and head index.
WLOG, we consider the nearest left case.
We just need to make the attention exponential look like this:
0 y + +A p'-p A'l.gp'' pp-000
(16)
where Alagg'' E {0,1) indicates whether the value at position p' is some or none.
We set Vp to represent the value of type Option<T>>
For the starter token po, we make it such that
0 AY Po 1,
(17)
and
po 0,
(18)
so that when there some to the left, it will give none.
Proposition 16. [Nearest Two Left/Right] For any local type T consider the function that maps sequence of type Option<T> to nearest two left/right neighbors that are not none. It's representable in ( where d is the encoding dimension of T (11),0(())
Proof. We can utilize Proposition 15 and 14.
The nearest two left right is equivalent to first computing the nearest left/right, and then packing them together into one and compute its nearest left right. The process is represented by small constant computation graph, then we're done.
D.7 Syntax and Semantics of Cybertron
Having laid the necessary mathematical foundation behind Cybertron, we now turn to explaining its surface-itt syntax and semantics. Cybertron serves syntax sugar for expressing local and global computation graphs, which are the vehicles used to demonstrate the expressive power of transformers. In Cybertron, computations divided into two layers: the local world and the global world. These layers play distinct but complementary roles in constructing computation graphs.
D.7.1 Local World
The local world in Cybertron corresponds to the feed-forward layers of transformer, focusing on computations over local types. Local types represent individual tokens or data points, and computations in this world handle operations on tokens independently of their surrounding context.
Data Types. Local types in Cybertron include basic types such as Bool, Idx Pos
Finen> BoundedVec<T, N etc. These types are essential for building local computa- tion graphs that operate over individual tokens. Compound types, like structs and enums, can also be defined for more complex token representations. These types serve as the building blocks for the local computation graphs that transform data at the token level.
struct Node
Idx,
position: Pos.
}
erun Ogeration {
1hs: Pas,
Pos,
34

---

Published as a conference paper at COLM 2025
11
Multiply
12
factor: Fos,
15
14
Functions in the local world define operations upon information over individ- ual tokens. These operations form nodes in the local computation graphs. For instance, operations like binary or unary expressions, conditionals, and matches on token types are transformed into computation graphs by handling each individual token's data.
Functions.
process_ast(astt (ast: AstData) >> Option<Rlle>
match ast
AstData: :etinit pattern, initial_value, :eeefole::Letttti { pattern, initial_value
AstData::Letinit
AstData: :Defn keyward, ident, Sone(natch keyword {
Defrkkeyword::Stree => (ole::StructDeef((ddm)))
Befrkeyword: sEnun => Role: :Enumbef((ddmtt) defeeyyoor:::Fn Fndenenn)De)))eennt
11
}>
13
>> None,
14
15
Control Flow. In the local world, control flow structures such as if and match are transformed into computation graphs by treating each branch or arm expression that returns an Option based on conditions. These Option values are then combined using the
Option:or function. According Proposition 9, Option:or maps two Option<T> values
and returns the first non- None value, or the second one otherwise. This allows conditional branches to be represented in computation graphs sequential option evaluations, where the first matching condition provides the result.
D.7.2 Global World
The global world extends beyond individual tokens sequences of tokens, represented as global types. These global types are denoted Seq<T> where local type. The global world represents the full transformer, focusing on operations involving sequences of tokens, including variable definitions, expressions involving variable references, and function calls.
Variable Definitions. Variables in the global world are defined using global types, which represent sequences of local tokens. These definitions correspond to nodes in the global computation graph.
Expressions. Expressions in the global world consist of references to variables or function calls. Since the global world operates over sequences of tokens, these expressions are translated into sequence-level operations in the computation graph.
Function Calls. Function calls are key elements of the global world. They are represented by applying global functions to sequences of tokens. Cybertron provides map functions to elevate local functions to global functions by mapping them across sequences. Additionally, attention methods like nearest_led and nearest right handle dependencies between tokens in the sequence by identifying relationships based on their positions.
Iet result www.wus..ea.sss_uuuu..
In the global world, computation graphs are built by composing map functions and atten- tion methods. These graphs, unlike those in the local world, do not include control flow mechanisms.
35

---

Published as a conference paper at COLM 2025
D.8 Dyck Language
This section demonstrates how the local world in Cybertron operates over token-level computations and how the global world handles sequence-level operations. We use Dyck language example to explain the interactions between these two worlds. The example processes sequence of delimiters (like parentheses) and checks for matching pairs.
Local World. In Cybertron, the local world operates on individual tokens. Here, the local
types are simple, such as Delimiter and PreAst, which represent information associated with individual tokens. These types allow for token-level operations like comparisons and transformations.
We define struct to represent delimiter and an enum to classify delimiters as either left or right. These definitions reflect local types, as they hold information over single token.
Define a struct "Deliniter" that uraps a "uB" volue.
#Dderive Clone, Copy, Partialiq, pub struct Deliniter(u8):
// Def'nee enum "Prekst" which represents left or right delimiter.
(edebu., Clone, Copy, PartialEq, Eq)]
pub PreAst {
Leftielime iiii ter (eelimiter), centeelimtterDeeliiiii
10
Here, the local types Delimiter and PreAst define operations upon individual tokens, representing fundamental units of the computation graph at the local level. The local world responsible for handling these small, token-level computations independently of the global sequence.
Global World. In the global world, Cybertron operates on sequences of tokens, treating the collection of local types single unit of computation. The global world introduces global types such as Seq=OOption<<reAss>>>>> which represents sequence of optional delimiters.
The global world handles sequence-level operations by applying functions like nearest_left and nearest_right to capture the relationships between tokens in the sequence.
The following function operates on a sequence of PreAst reducing matched pre-asts. The recursive application of step gives us the classifier for Dyck language.
(pre_ass_s SeypOptionSPrekatt:) SeysOptionnPrekst>>>
let pre_asts.nnarest_lne pro_asts. mas.stttnnarsstlefftt
pre_asts_neares pre_asts. nearest.right() step_aux. apply(pre_ast)))ee (ttocpppratt_eeeeeeeeee leff, pre_asts, pre_ests.nearest.rihh))
Local Worlds. The step_aux function matches tokens based on their nearest neighbors within the sequence, eliminating pre-asts if a match is found.
Fn step_aux(
pre pre_ast_nearest (Idi PreAst)>,
pre_ast: OptionsProAst>,
pre pre.est_neerestrright: Options(Idx, Preast)>
+> Ootion<PreAst>
match pre_ast?
Prest::lefteeiitteerddllttttee
pre_ast, ass__neerest_rriit
Sone((., het.:eiiiiiieeiiiieeeedediiiiiii if deliniterl = deliniter => None, pre_ast,
10
11
Preest::RgheeLLnnteerddditeeee natch pre neeaesttterrett_eefe { Sone((.. Press::LeffDeiinnierrddiiiee if deliniterl deliniter s> None,
12
15
>> pse_
15
36

---

Published as a conference paper at COLM 2025
In this example, the global function step nearest left and nearest right to capture sequence-level dependencies, while the local function step_au aux uses conditional logic to check for matching pairs of delimiters. The local world handles token-level logic, while the global world coordinates operations across the entire sequence. This separation reflects how Cybertron handles computations different levels of granularity.
Thus, this example illustrates how Cybertron leverages both the local and global worlds to build comprehensive computation graphs in convenient, comprehensive yet rigorous manner. The local world performs individual tokenwise operations, and the global world captures relationships between tokens in sequence, demonstrating how Cybertron enables transformers to express complex computations.
E
Mini-Husky Details
Here's the BNF grammar of the Mini-Husky language:
(ast)
(literal)
Lident)
prefix))
binary)
(suffix)
(delimited)
separated_ite __itemi
feall)
(let imit)
if stmt)
else stmt)
defin)
(literal) ==
(ident)
(prefix)- == pprefix_oph) (ast)
(binary) == (ast) (binary (irr (ast)
(suffix) == (ast) 'suffix_opr)
(delimited) == (left (efft_elimmtter) (separated _item)" (right__eett delimiter))
(separated item) == [(stt]] (separator)
(call) :: (ast) (left delimiter) (ast)" (right delimiter)
(let init) == let (ast)
(if_stmt) := if (ast) (delimited)
(else_stmf) == (jf_stmt) else (Idelimited) (else_stmit)
(defn) := (defn_ keyworrd) (ident) (ast)
(prefix_opr) 1
(binary-opr) ==
(suffix_opr) := ++ -
(Jeft_ [eft_deeimiterr) := '(' 1
(right delimiter) := ' [ (separator) :== ;
deefn_keyword) def fn
Below is a sample piece of codes:
struct Dog weight: f32,
Fn see_ (dog: Dog) >> F32 assert dog. wnight 108;
37

---

Published as a conference paper at COLM 2025
nut dog. weight 10.0; Fee +=108.8; return
It should be noted that the above is not the full story. There are additional constraints put on the ASTs. However, these can be easily implemented as tree functions that are easy for transformers to express. As we are focusing higher level language processing capabilities, we ignore the details here.
Additionally, need to require that for semantic correctness, must have proper symbol resolution and type correctness.
E.1 Additional Details about Compiler Tasks.
The outputs of the tasks are defined using Cybertron follows:
The construction of AST task's final output is the collection all AST nodes. More concretely, the output is sequence of Option<Ast> with length equal to the input token sequence's length, where Option<Ast> denoted the type Ast will null value added and Ast is the type storing the information of node, including its parent, and its data of type AstData In Cybertron, we define Ast and AstData explicitly follows:
an /// Each "Ast" nade has reference to its parent node (if any) and holds data (such expressions, statenents, other /// constructs defined in the "AstData" enun).
Represents
Syntax (AST).
///
/// the associated
5
7
/// The index of the parent nade in the AST, if it exists.
///
/// "Sxx)) The nade has parent, and 'Idx' represents its position.
10
/// "None" The node is the root or does nat have parent.
pub parent: Option<idxo,
12
/// The data associated with this AST node.
pub AstData,
14
/// Enuneration representing different of Abstract Syntax Tree (AST) nodes
17
pub enun AstBata
/// Represents literal value (e.g., integer, string)
19
(Lttrrl()
Represents identifier (e-g., variable nane)
(Ident,,,,),
!// Represents binary expression (e.g., "x +.y" Binary
/// Index of the left operand
lopd: Idk,
26
/// Operator in the binary expression (e.g., 147, 187)
opr: DinaryOpr,
/// Index of the right operand
ropd: Idk,
// other variants
The output of the symbol resolution task the collection of symbol resolution re- sults on all applicable tokens. More concretely, the output is sequence of val- of type OptioonSSymbooResottttonn where Opiion is the type SymbolResolution with null value added for non-applicability and SymbolResolution is the type storing the result of the symbol resolution, being either a success with a resolved symbol of type Symbol or failure with error of type SymbollesolutionErrrr In
Cybertron, define SymbolResolution explicitly follows:
// definition, basically tagged union type
2 pub enun SynbolResoolution {
Ok(Symbol), // type variant success resolved symbel
Err(SynbolResalutiooee // enun type variant for failure with an error
38

---

Published as a conference paper at COLM 2025
The type analysis task's final output is the collection of all type errors. More concretely, the output is a sequence of Option<<lypeError>> where Option<1yypEErro> denoted the type TypeError will null value added and Typešrror is the type storing the information of type error. The position of type errors agrees with the source tokens leading to these errors. In Cybertron, we define TypeError explicitly as follows:
// This represents various kinds of type 2 pub enum TypeError {
variant indicates type misnatch !/ "expected" is the type that was anticipated encountered
"actual"
type
TypeMissatth expected: Type, actual: Type ).
One can expand the definition to include other kinds of type errors.
(1) Type definition. Types either identified uniquely by single identifier like <identifier> or builtin generic types Option<<identifeer>>> or Vecccidentifier>>> Users can define custom types without generics like the following (f32 means float32 and i32 means int32 below):
Dog weight:
enun Aninal
Dog.
Cat,
This part is actually part of the AST task and type definition is a variant of the AstData type:
/// Enuneration representing different types of Abstract Syntax Tree (AST) nodes
pub enun Astilata {
Represents function or variable definition
///
/// # defn
Defn {
/// keyword definition (e.a., 'fn", "enun") keyword: Defnkeyword, /// Index the identifier in the definition
10
11
ident_idx: Idx,
13
/// the identifier being defined (e.g., function nane, variable nane)
ident: Ident,
15
/// Index of the content or body of the definition
16
content: Idx,
17
18
}
(2) Type specification. Each appeared variable has unique type, either by specification or speculation. All parameters of a function must be specified explicitly by users. Variables defined by let statements might or might not be specified, as follows:
f(a: type
be specified let x: 132 // type of "x" specified
y a; type "y" unspecified
The return type of functions must be specified. The field type of structs and enum vari- ants must be specified. the type of expressions of function calls and field access will be determined correspondingly.
The output of the task is the collection of all type signatures, represented as sequence of values of type Option<TlypeSignature>> where TypeSignature is the type holding the essential information of type specifications. In Cybertron, TypeSignature is defined as,
pub TypeSignature { pub key: TypeSignatureKkey pub ty: Type,
39

---

Published as a conference paper at COLM 2025
pub enun TypeSignaturekey {
FnParaneter { fn_ident: Ident, rank: Rank ),
Froutpuu fn_ident: Ident 7.
Structfield ty_ident; Ident, field_ident: Ident }
10
(3) Type inference. As discussed above, not all variables have their types specified.
let x: 132 m 1; y x; let =
In the above code, an ambiguous literal that be of type i32, 164, u32, u64 etc, and the types of and z is not specified. However, one easily sees that there exists one
and only one choice of the types of Utilizing this property, the user can opt out of a significant portion of type specification, achieving static guarantees.
and such that the whole code is type correct.
For simplicity, we shall prove transformers can implement simple type inference algorithm: we maintain table of type assignments for variables. We update the entries of the table by means of reduction, i.e., assuming the whole code is correctly typed and infer more and more unspecified types until we encounter errors or all types are inferred. The process is largely parallel, and we call the number of rounds needed the depth of type inference.
Type Inference Algorithm:
In the above code, the first round, we determine that the type of both and the type of y are equal to the type of x which is i32 But we have no way to determine the type of because the type of is unknown at the first round. In the second round, can be determined to be of type 132 because the type of is already inferred.
The output of the task is the collection all types inferred, represented as a sequence of values of type Option<Tlypennference>> where Typelnference is the type holding the inferred type. In Cybertron, TypeSignature is defined as,
pub struct TypeInference ( pub ty: Type,
F Transformer AST Proof
E1 High Level Overview
Proof Skeich of Theorem 1. The idea is to construct ASTs in a bottom-up manner with full parallelism. We shall recursively produce the final ASTs in at most D steps. We shall maintain two values, called pre_asts and asts asts represents ASTs that have already been allocated, although they might not have been fully initialized. pre_asts represents tokens that have yet to form ASTs and new ASTs that have not been fully initialized. For each round, we try to create new ASTs from pre asts and update asts and pse_asts asts For the n-th round, provably allocated all ASTs with depth no more than Then for the D-th round, all ASTs are properly constructed and allocated. Each round can be represented by transformer of (11) number of heads, model dimension O (log + D), and O(1) number of layers. Therefore, the end-to-end process is then representable by transformer of O(1) number of heads, model dimension O(log + D), and O(log L D) number of layers. L
Here give the full details of the proof of transformers being able to parse ASTs.
40

---

Published as a conference paper at COLM 2025
On high level, are going to the parsing of ASTs assembly process. First, we immediately get the atomic ones, like identifiers, literals, etc. Then we assembly all composite ASIs with enough precedence util all tokens are consumed. We prove that at the wthh round, all ASTs with depth no more than и are already constructed. In the process, must keep track of the unconsumed tokens and newly constructed ASTs (to be consumed as children for new ASIs in the next round, as we are going bottom up). We use pre_asts to denote all the unconsumed tokens and newly constructed ASTs and use asts to denote all the constructed(allocater ASTs. For correctness guarantees, we give detailed type specifications for tokens, ASTs, and PreASTs as follows.
We define the Token type follows:
/// The "Token" enum represents the various types of tokens that can be
1// identified during lexical analysis phase compieer. variant
1/1 corresponds to specific category of taken that can be encountered
/// in the source code.
Duo enun Token
1// A literal value, which can be number, string, or other prinitive type. Li Literal(Literal),
1// A reserved keyword in the language, such as rif", "else", "while", etc. (eyword(K)yward)
10
1/7 An identifier, typically representing variable names, function names, !/! other user-defined symbols. IIdentI.)
11
12
13
1/1 An operator, such as "+', *H", te", "==", etc., representing nathematical logical operations. (pr()
15
beginning 1/7 A right deliniter, such ')", "Y', 'I', used to denote the end of /// black, list, or expression.
deliniter, such 'C, "C, "D' used /// block, list, expression.
17
18
19
20
(ighbelinnterr(@ghbbblliii !!1 A separator, such as or ";", used to separate elements in a list or statements in Separator (Separator),
22
21
25
}
The type has an encoding dimenion dToken (loog L), which is large enough to faithfully represent its information.
More specifically, the types Literal, Keyword Ident
Opr LeftDelimiter, RightDelimiter
Separator are local types assumed to have encoding dimension less than dTokem Keyword
Opr, LeftDelimiter, RightDelimiter, Separator are small, they can be encoded in straight-forward manner entirely using dToken- However, Literal and Ident are larger than representable by limited number of bits because potentially a Literal can be string literal of arbitrary length and Ident also be of arbitrary length. This be solved through methods like interning, which gives all literals and identifiers that actually appear in the input distinct encodings. As the context length is L, the number of different literals/ /identifiers are bounded by context length and interning needs (ddoken) = O(log L) to work. As far as our theories are concerned, it's totally reasonable to assume that all these types are assumed to have encoding dimension less than dToken O(log L).
We define AST type as follows:
/// Represents node in Abstract Syntax Tree (AST).
///
/// Each "Ast" node has reference to its parent node (if any) and holds
/// the associated syntax data (such as expressions, statenents, or other "AstData" enun).
/// constructs deflined
pub struct Ast {
The
parent
AST, it exists.
///
"Sone"Idk)"; The node has parent, and "Idx" represents its position. /// "None", The node is the reot does not have parent.
10
11
pub parent: OptioncIdxo,
associated with
node.
13
II!
field holds syntax information, which typically
41

---

Published as a conference paper at COLM 2025
defined "AstData" enun. could represent literals, expressions,
16 /// statenents, and other constructs in the source language.
pub data: AstData,
18
Note that we intentionally structure the tree by always storing the parent but not necessarily storing all children information. In our assumptions, we only control the depth of ASTs but don't control the number of children. More specifically, a function can have as many statements possible. To avoid overflowing, don't store all children information. As shall see, parent information alone is enough for transformers to perform tree operations.
The AstData is the most complicated we define in this paper, as follows:
/// Enumeration representing different types of Abstract Syntax Tree (AST) nodes
pub Astilata
/// Represents literal value (e.g., integer, string)
Literal(Literal).
/// Represents an identifier (e.g., variable nane)
(Ident).
/// Represents prefix expression (e.g., "DO, (-x))
///
10
///
Prefix
12
1// Operator in the prefixx expression (e.g., "f", TH1)
13
opr: PrefixOpr,
14
/// Operand index of the expression opd: Idx,
13
17
1// Represents binary expression (e.g., "x y', bi)
Binary
19
!// Index of the left operand lopd: Idk,
20
/// Operator in the binary expression (e.g., 14", (et)
22
opr: Binaryapr,
23
/// Index
right operand
24
ropd: Idk.
26
!// Reprosents suffix expression (e-g., "x++", Ty-+")
27
Suffix
28
/// Index of the operand
29
opd: Idx,
/// Operator in the suffix expression (e.g., 'et", (--1)
31
opr: Suffix0pr.
},
33
/// Represents delinited expression (e.g., "(x +),,, '(a, b, c)7)
34
Delinited (
!/1 Index of the left delimiter the expression left_deliniter idx: Idk,
36
/// deliniter (e.g., 'C' '('
38
left_deliniter: Leftbelimiter, !// right delimiter (e.8., ")", '}") delimieei::: RightDelimiter,
60
41
separated by SeparatedIten {
Represents
(e.g., elements in array
43
/// Index content, any
45
content: Option<Idx>,
46
/// separator (e.g., ",", ";")
47
separator: Separator,
48
Represents function call array (e.g., "f(..)", "aC...)) I//
50
things "f(...)" "a[..."" call {
52
/// Index the caller (e.g., function array)
54
caller: Ids.
55
//7 The left deliniter of the call (e.g., 'C', ((")
56
deft_delintter: LeftDeliniter. /// The right delimiter of the call (e.s., ')", '1">
57
right_delimite ter: Rightlelimiter, /// Index of the delinited arguments in the call
59
60
delimited, argunents:: Idx,
61
62
I// Represents a 'let" statement with an initialization (e-g., "let x 5;")
64
HI U stnts
42

---

Published as a conference paper at COLM 2025
LetInit
67
/// Index of the expression in the initialization expr: Idx,
68
69
/// Index of the pattern being initialized pattern: Idx,
70
71
/// Optional index of the initial value initial_value: Option<id<>,
72
73
74
I// Reprosents an "if" statement
75
76
/// Index of the condition in the "if" statement condition: Idk,
77
78
/// Index the body of the "if" statenent body: Idx,
79
81
I// Represents an "else" statement
82
Else {
83
/// Index of the associated "if" statement
94
if_stnt: Idx,
/// Index of the body of the "else" statenent
86
body: Idx,
2.
88
1// Represents function or variable definition
89
90
/// defn
91
///
Defn
93
/// The keyword in the definition (e.g., "fn", "enun")
keyword: Defnkeyword, /// Index of the identifier in the definition
95
96
ident idx: Idx,
97
/// The identifier being defined (e-g., function nane, variable name)
98
ident: Ident, /// Index
body definition
100
content: Idx,
102
enun represents intermediate /// encountered during the parsing phase, before the final AST is constructed.
are
/// Each variant corresponds to a specific type token or partial
/// node that contributes the construction the final AST.
#[derive(Clone, Copy, PartialEq, Ea)] pub PreAst
/// A reserved keyword in the language, such as "if, "else", "while", etc. Keyword((eywardd,
1// operator, such "+", "-", "*', t==", etc., representing mathenatical
10
1// or logical operations.
(pr()pr).
12
/// A lef't deliniter, such as 'C', '0, "C', used to denote the beginning of expression.
block, Lefthelimiten ter (lefteelirtt))))))))
14
13
right delimiter, such ")", ")" "I", used to denote of /// block, list, or expression.
16
17
Rightbelimiter(Rigihe (Rreiiintrr(ighhtalliiimee partially constructed AST representing II/ that will be further processed to build the final AST. Ast(AstData),
corplex
19
21
I// A separator, such as "," ";", used to separate elements in list
22
statenents in block. Separator (Separator),,
23
24
/// this beyond the of Cybertron
///
rather general function to integrate for testing
pub fn calc_asts_from frots_fron_iiie (n:::t Astr, usize) -> (Seecoption<Prosst>>, SegpOptionckstss) { takenize(ingut); let pre_asts ieee_ast_initill_seeeeeee
allocated_asts: SegslptioncAsto> tekens. token) token.into()):
tichuren_timespree.stts. allecated_asts, n)
The reduce function in Cybertron is designed to progressively refine sequences pre- abstract syntax trees (pre-ASTs) and allocated abstract syntax trees (ASTs). The function takes two input sequences: pre_asts, which is sequence of optional pre-ASTs, and
43

---

Published as a conference paper at COLM 2025
allocated asts, which is sequence of optional ASTs. It returns tuple containing the reduced sequences of pre-ASIs and allocated ASIs.
The reduction process carried out in multiple stages, each focusing on different syntactic constructs:
1. reduce by_opr This step handles reduction by dealing with operators and their precedence. It simplifies expressions involving operations to form more compact ASTs.
2. reduce by delimited This step reduces constructs that are delimited, such those involving parentheses, braces, or other grouping symbols. It ensures that delimited blocks are properly nested and combined in the AST.
3. reduce by_calll In this stage, function method calls are reduced. This involves identifying and structuring calls within the AST, ensuring correct representation of function invocations.
4. reduce by_mtmt: This reduction step addresses statements, ensuring that individual statements are correctly parsed and represented within the AST, such as assignment statements, loops, and conditionals.
5. reduce we_bbb__ddnff. Finally, reduction by definition handles the parsing of definitions, such as variable or function declarations. This step ensures that all definitions are correctly represented within the AST.
By sequentially applying these reduction steps, the reduce function progressively trans- forms the initial sequences into their most refined forms, ready for further syntactic or semantic analysis.
pub fn reduca(
pre_asts: Segs@ptionnPrekst>>
allocated_asts: asts: Sepoptionsssto9,
(Sey<@ptian<rrelstt Seg(pptionksst>))
// Reduca ASTS by handling ing operators and precedence
(pre_asts, allocated_asts) reduce_by_oprr byooboyyooppppasttt. allocated_astss;
// Reduce ASTs by handling delimited constructs like parentheses or braces
1et (pre_asts, allocated_asts)
allocated_asts);
10
// Reduce ASTS handling function method calls let (pre_asts, allocated_asts) = reduce_.y_ccallppee... allocated_asts)
12
14
// Reduce ASTs by handling statenents, ensuring proper syntax structure
15
let (pre_asts, allocated_asts) reduce_by.stmttprre.ee allocated_asts).
16
17
// Reduce ASTs by ing definitions, like variables or functions (pre_asts, allocated_asts) medice_byydrrf(prr..ttt, allocatedLasts)
19
reduced (pre_asts, allocated_asts)
pre-ASTs allocated
21
22
pub reduct_n_tines(
nut pre_asts: sendoptiinnPeesst>>, nut allocated_asts: Segs@ptioncsst22,
usize.
) -> (SerspptionPrekstto,, SegcOption<Astts) e...
let (pre_astsl, allocated_astst) reduce(pre_asts, allocated_astts)
pre_asts pre_astsl;
allocated_asts allocated_asttl;
10
(pre_asts, alloeated_asts)
12
In the above definition, actually used Rust's mutable variable semantics. However, it's straightforward to see that it translates to a computation graph that sequential composition of subgraphs with sequential length Because the AST's depth is bounded
44

---

Published as a conference paper at COLM 2025
by D, can just take to be D. Each subgraph is generated from the reduce function, then they are all constant graphs constructed by global and local functions, then by Proposi- tion 13,11 and 2 they translate to transformers with Olog + D) depth, model dimension, and number of heads, where log L. comes from the encoding of types like Token
Below we give full details of the various reduction functions.
As these are implemented as Rust functions, they have been tested against number of inputs. We don't guarantee an industry level of correctness, but the key point is well illustrated.
F.2 Operators
In this section, we lay down the definition of reduce by_opr
(super) fn reduce_
pre_asts; SeydptiionPreksss.,
allaatedd_asts: Sepdpptionckst>>,
) -> (SepsppiimmfPresttb,, SegrOption<kstss) (
pre_asts_marret__lff2 pre_asts. pre_ants.nearnst_ffrr. nearest_left2));
let wre_asts_nearest_rigg
pre_asts. nearest_right2(;
new_opr_asts new_opr www__orr_stt.oom asp.lapllyypre astssseearest_ee.oeee left2, pre_asts, pre_asta_ hesttstneretttrighhta
let jpre_estt_reduced, new_parents) reduce_pre__eee pttpppe___st___ooooo bytss_y__ppraaee wprropppppr_assee (pre_asts, new.opr_asts);
pre_asts
new_opr_asts):
10
let allocated_asts
11
blocate_asts_and_oe. (pre_asts, allocated_asts)
apwsopr_ssts, nex_porents);
13
/// Finite function pub(crate) fn new_opr_ast(
nearest_left2: Option2<(Idx, PreAst)?,
current: Option<PreAst>, nearest_right2: Option2<(Idx, PreAst)>,
>> Some(Prekst:OOp((o)r))
OotionststDats>
return None;
):
match apr
11
Prefxx())))))) >> Sone((epd, PreAst::Ast(.))) nearest_rightt.firscd
13
return None;
};
15
if let Sone ast)) nearest.riggtt..scomd
16
natch ast Keywor())
18
Trekst::Op(rright.com >> natch right_opr
Ppr::Pref(x(_) ().
20
Opr::Binar(rright..om >>
21
// every binary opr
small language associative, so instead
22
if
right_opr.preeeeeeee right_opp..reecedncnn) preceddecd)))) Pre.ceededce)) (
23
return None;
24
26
Opr:: :euusuuufrrgght_ppp >>
27
if rightt_opr.pret (tt..pppccceecce())) Precedeecee (
28
return None;
29
31
}.
PreAst:cAst())
33
// Function call or index takes higher procedence
34
Preast::LeftteelimteerCC => return None, Press:::RighDeeiiiterrCC. s> O. Separat:Se => O)
35
36
38
}: Someeasttaata: { opr, opd ))
40
41
Binaryyony()p)) let Sone((lopd, PreAst::Ast(.)) nearest_lefl2.firstt else return None;
42
45
3:
45
let (rop( Arstst::Ast(.)) nesrest_rightt. first() else
return Nane;
45

---

Published as a conference paper at COLM 2025
48
if let Sane((., ast)) bearesst_efft.seccondd match ast (eyeor:: Q.
50
51
(Leef нo natch left_
52
Ppr:: if left_opr-pret precadicce() >= prr-predeeecee) (
53
None;
55
56
57
Opr: Bineryilett s>
58
1/1 every binary opr in our small language left associative, so "Se" instrad
of 1>
99
if left_opr.preeeeeeee precedence() >= spr.precedence() ( return None;
61
62
63
SSffiXC)) O, // actually this will be syntax error ProAst::Ast()
64
66
1f opr != Binhhror::Lighhdrrow {
68
69
20
Prebst::eefUDelimiterrd => O, PreAst: RighbrD:igDDDDiiieerrr.... => return None, Separrato()
71
72
73
}
3:
75
if let Sone((.. ast)) nearest_rightz. second() match ast { :resst::Keywrdd(ee match Keyword: :ELSE => return None,
76
77
78
80
}. PreAst::0pr Crrrihhhorrr natch right_opr
82
Ppe:: s> // actually this will be syntax error Dor:BBnary(righh_ppp. => every binary
83
84
small language left associative, '<" instead
of
if right_opr. return None;
riight.orr.preeeeeeee prr.peeced))ce( precedeecee)) {
86
57
88
89
Opr:: Sur::Suffixrright.orr => if right_opr..prreeeee preredeencn))) spr.praceeeecee) return None;
91
93
}
),
95
// function call index takes higher precedence Leefst: ter => return None, PreAst: Righhtiliittttetterrrrr PreAst::Ast() => ()
96
O,
98
Sepaatt ()
100
}
}:
Some(AstData: { lopd, opr,
105
Opr:: Sufffi(opp) let Sone((opd, PreAst::Ast(_))) nearest left2. first( else Nane;
105
107
};
1f Sone ast)) nearest_left2.
match ast Keyyord))) >> O.
110
PreNst: natch right_opr
112
Prr::Prrfixrrihhtt..oo =>
right_opr. pre.precceeecc(() precedence))) {
114
return None;
117
Opr: BinnrB(rriggttt.oo => every binary opr small language left associative, "e" instead
of Tice
if right_opr. niigh_.orr.preceeee precedence)) precedence() { return None;
120
123
Opr:: Suffix()) >> O.
46

---

Published as a conference paper at COLM 2025
Prekst::Leffollmmtterr. (_) O. PreAst::ightDDelinita >> return None, PreAst: return None, Spepst:: O.
126
128
131
Some(Astiaata:: Suffix ( opr, opd ))
133
/// returns sequence of renaining PreAsts and new parent idxs
pub(erate) fi relure_pre_astee brttieeppresassbyyo___ bypop(
pre_asts: Segs@ptiondPrekstb),
nex_asts: Segsptionastbatap,
)
(SorsptiansProkstt,,, $eg(@ption(Id>>))
let mew_asts_nearett.iff new_asts, new.stt..marstt_lfff. nearessetttt
pre_asts redice_pre_ass..be www..eeaast..plllllee.
new_asts);
let (pre_asts, new_parents) reduucepre__st__ee btt.ppprrr_tt____e____e....
pre_asts)
decouple();
11
let cer.sttt_earrst_riggg... www.asts.nearest.rige
13
aappy_
seuneratedree..stt..aareee decouple()
pre_asts, new_parents)
14
15
reduce_pre. bess__by__w_asttpeee OptiondPreAst>, new_ast: Optiancastilata>) Optian<PreAst> if ies_ee)..s__some {
None
elsse
pre_ast
reduce_pro__de radluc..pr__sss_bby.pp__....
idx:
let_asttnnares__lett: Option<(Idk, Astilata)>, pre_ast: Option<PreAst>,
->
(Option<PreAst>, OptionsIdx)) le: Sone(pre_ast) pre_ast else return (None, None);
): Some((new_ast_ul) new_ast_data)) new.ast,.eareet_Leff else return (Sone(pre_ast). None);
10
11
}:
12
natch new_ast__aa _aw_ast_data_a_e AstData: :Binary { ropd: upd, .. AstData:Preffx opd, .. } if apd idx
13
(None, Sone (nne_astt__dx))
15
(Sone(pre_ast)) None),
17
18
reduce_pree catpucc__re__s__byy___ arr__ast_by.oor_right
idx: Idx,
new_ast_nearast_riig Option<(Idx, AstData)>,
pre_ast: OptionsPreAst>,
new_parent: OptionsIdx>,
->
(OptioncPreAst>, OptioncIdke) 1et Some(pre_ast) pre_ast else return (None, new_parent);
);
let Some(new_parent) new_parent return (None,
11
13
1et Some (ome@(new_ast_idee idx, new_ast_dataa) new_ast_noorest_right else { return (Sone(pre_ast), None);
14
16
match new_ast_data (
:Binary lood: opd. .. AstData::Suffic opd, (None, (one__s_sst__dd))
18
20
>> (preespre_ss),, None),
21
47

---

Published as a conference paper at COLM 2025
F33 Statements
In this section, we lay down the definition
reduce_ Satuue_by_see by_stmt
pub (super) fn reduce_by by_stet(
pre_asts: SepdpttionSrekstb,,
allocated_asts Segspptionssst>
) -> (Sersption<<rekst>>), Seg<option<ss>>)) {
pre_asts_ are_asts_nearest.ti 1eftstt pre_asts. pre.etts.neerrst.eettzzz
let wre.asts..oorestrrigh222 prt.aats..marrst.rrghh20 new_stat_ossss
new_stnt_ast... wtttt_est..pplyppee.artt met.sttseeeest..ef....
prre_asts_nearee wew.eeeet.trihhhaa.
let (pre_asts, neu_parents)
(mn_stt__asts)
allocated_asts
11
sllocat_asts__ane
imm_uudatee.arretssaaa
astss new_parents);
pre_asts update_pre_ peeeete_pr__sss______eesssssssse prre_sts_by__att
new_stat_ests))
13
(pre_asts, allocated_asts)
new_stnt__ast(
pe.st__nerrssi_eef.2 Option2<(Idx, PreAst)>,
pre_ast: Option<PreAst>,
(e__ast_nerast_rightt. (ption2<(Ióx, PreAst)>,
) -> Ootion<AstData>
pre_ast?
return None;
):
natch
10
StmtKeyword: iet Presst::Ast(<st))) wte.asttneerestt.iihh.... first() else let Sone((1dk),
12
return None;
3;
14
if let Sone((_, pre_ast)) prr.ast.mearstt_iigh...cm {
15
natch pre_ast
PreAst: Keywerd)) O,, Pre)st::Opr(.) (rekst::Leftbeliniter]] => return None, PreNst::Righteeliitee PreAst::Ast(.) so return None,
17
O.
19
PreAst::Separate (separator)
separator
21
Separator: :Conna return None,
22
Separator::Semicodle => (),
23
24
26
let (pattern, initial_value) = natch ast AstData::Binary lopd,
28
29
apr: BinaryOpr:Assiign
ropd,
31
} => (lopd, Some(ropd)).
AstData::Ident..
33
AstData: :Prefix {..
Astbata: :Binary {
35
: Delinited (
36
AstData: :Call ( .. => (idx1, None),
return
38
Some(AstData:LeiInntt
40
expr: idx1, pattern, initial_value.
41
12
43
45
StntKeyward: :IF =>
Sone (conditioo, Prodst::Ast(astt))) pre..ust_msresttrrihh....
47
return None;
68
3: let Sone(( body,
89
50
Tresst:Ast(sstttee:elllint
52
left left_delimiter: LOURL, right_delimiter: RCURL,
54
55
}). rew.ass_eerrss__ighh..cee
56
57
else {
None;
99
):
Some(Asthata::1f candition, body })
48

---

Published as a conference paper at COLM 2025
62
Statkeyward: :Else =>
Sone((ff_stet, PreAst: if ( ... }))) pr else {
64
65
return None;
67
let Some((
body,
69
PraAst::Ast(
70
AstData:DDllmiteer [
71
deftndelinite:: LCURL.
72
right_delimiter. ROURL,
73
74
73
AstData::If {
76
AstData: (..
77
).
78
wwe..st.nerrrsL.ighhh..... else {
79
None;
81
):
if Sone((.. ProM:::lewerd(eewwrrr.tL.)))))): pre_ast_nearest_rrghh2
83
return None;
84
85
Elle if_stmtt body
96
83
reduce pwt.tpreeessss___eeeeee_eeeee by_ (
pre_asts: SevrOption<Prekst>,,
new_asts: Serdpttionckttlata>,
-> "See<cption<Preesttt Seq<aption<idk>>)
nearest_eftt www.asts.nearest.uu
www_antt..nares_.right
nearest_rightt)
reduce_pre rre_aas__b_.ste
laaplyyleeeeee anunerated(neu_eee seterrrrsssttteeess_eeeeree. new_asts_.earret_riig pre_asts)
.decouple)
Fn reduce_prs satico_poooast_b_sttee
1dx: Idx,
nee__st__nerret__eff Option=(Idx, AstData)>,
mew.ast_neares__right Option<(Idxx AstData)>,
pre_ast: Option<PraAst>,
) +> (Option<PreAst>, Option<ldx>)
if Sone((idx1, ast)) nww.ast_.narrst__lff
AstData::LetIntt expr, .. } expr idx (None, Sone(idx1)). match ast
10
AstData::If
11
condition, body, if condition idk body AstData::Elss { body, 1f body =s 1dk ss (None, Sone(idx))).
(None, Sone(idx1)),
13
(pre_ast, None),
15
16
else if let Sone((idk1, AstData: :Else if_stnt. ))) wew.estt.earest_rige if_stnt idk
17
18
Some(idx1))
20
else {
(pre_ast, None)
22
F4 Generalized Call Forms
In this section, we lay down the definition reduce_by_cs
pub (super) fn reduce by_call(
pre_asts: Seyaptiionsrekktt>
allocated_asts: Seqsoptioncast>>,
) (SeysoptionsPresst> Seecoption<Ast>3)
let wtw.asts_nerrst_iig pre_asts. pre_atts.errrsstriiiie nesrest_rghtt
let
new.call_est sapllyeeuueratee((rr. srtt:rr..srtsmmmsstt_ee.... met.ssts_earess_riiggg
(pre_asts, new_parents) redice_re__atttbb_cclll neu_call_asts))
49

---

Published as a conference paper at COLM 2025
allocated_astt
11
new_call_asts, new_parents); pre_asts hww..aass..h..eee..aaee new_call_asts);
12
15
apte_asts, allocated
14
Fn new_call_ast(
idx: Idx,
ire_ast_nearest_leff Ogtion2<(Idx, PreAst)>,
pre pre_ast_neares_rriht: Options(Iax, PreAst)?,
OntiondastData>
let (caller, PreAst: (rtcsl::st(()lleerr.sss) pre_ast_.eeresttlefff first(? else None;
}:
(
10
delinited ted teiinited__rguneeee arggunensts
11
As (roatt:AAs((sttttt:::00iiim {
left_dnlimiter_idk,
13
left_delimiter,
right_delimiter.
15
)). wwe.ast.neerest.righh
16
17
else {
18
return None;
20
if 1et Sone((., snd)) = wer.sst.eerres..lfff.eeeeo
22
Key natch kw
23
Keyword: :Defn(kk) so natch kw
24
Defrkeeyerd: :Struct Defnkeyword:
=>
25
Befnkeyword: :Fn => match lnft_del del initni {
26
Delini :Paretthsss :elimiter::Box return Delimi :er:: #> O)
27
29
)
30
Keyword: (Stntt =o natch kw Statkeyword: :Ltt => O,
31
32
Statkeyword: iff => match left_delimiter. dewelliitee.eeliiiieeee deliniter() {
33
Delini Parenthhess Deliniter::Bx O.
34
Delini :Crry m> return None,
36
StatKnyword: :Els => return None,
37
}.
39
(oprst):(rr(opr) => natch opr Opr::PrefLx(.) Opr::Binary(.)
left dew.nieeeerr...mmme deliinierrd)) Deliniter: Parenthesss Deliniter::Box => (), ter: :Curly return None,
41
43
44
Opr::Suffix() => return None,
55
Lresst::Le => O. PreMat::iihhDeeiiiteer. (_)
None,
48
ArsAst::Astssndd_e =>
bstilata::ldent (.)
50
5& left_delimiter == LOURL
51
match caller_ast C
53
AstData: {
opr: BinaryOor::LighhArrr
53
57
AstData::Dellnitee left_delimiter: LPAR, right_delimiter:
58
60
} => return None,
62
63
64
} else return None;
65
67
Sopratt: ( O.
69
70
71
if wer__deeinnteerreee Is idx
72
return None;
74
Sale {
caller,
50

---

Published as a conference paper at COLM 2025
delini ted_ argunents,
77
left snft__dliiitter
right_delimiter.
79
reduce_pre__st www.uee_rre.sst.bbyoooo ays.sssyycccllc
pre_asts: $er9ptionsPrekstp,,
new_asts: SeyspptioncsstDatap>,
) (Sepssptian<Prokst>>, Seqdppionk(ldos))
let wew.asts_nearest_ief! neo_psts.neress_eett)
new_sts, nes.ttss.rrsstrrigttt))
reduce_pre
apply_enunerr
new.asts_nearest.rigg.. pre_asts)
.decouple()
10 }
reduce_pre_ece pre_ast_by_call call(
idx: Idx,
new_ost_noaret_llet:: (ption<(Idx, Asthataa?,
wew.est.nearesi_rrhhh:: Option<(Idk, AstData)>,
pre_ast: Option<PreAst>,
-> (Optien<PreAst>, Option<ldee)
if let Sone(( idx1,
AstData: :aal { delimi delimited ted_argunents,
11
}.
13
}) new nearessttttt
14
deLimited arguueetsss 1dk
15
16
(Nane, Sinx(idx)))
else if let Some((idx1, Astuata: caller, 1)) new.ast..earesttriith
18
88 caller == idx
19
20
(None, Some(idx1))
21
else
22
(pre_ast, None)
23
F5
Definitions
In this section, we lay down the definition of reduce_by_dee
(super) fn redure_by__dee by_defn(
pre_asts: Seyshttion<reesst>
allocated_ Sepspptionsss>>>
+> (Sersspt, Seqctption<Ast>>) (
pre_asts_neares, nearesttettst pre_asts. nearest.leftt();
let wre_asts_nearestrrigh2 pre.ests.merresLrrihhz))) new_defr_asts:
aaternnstt.aeplyyrr...ttt. nets__earrst__lftt) pre_asts, smm_ants_naarss_rrghhh)
let (pre_asts, new_parents)
wwwppeestss..ddeeeeerre..... new_defn_asts);
allocated_es$e
11
allorate_are asts__nd__udate_ppe pawennts(allcaated.oro new_defn_asts, new_parents);
12
pre_asts sodate_pre_asts.bb be__eensstttprreeeeee new_defn_ests);
(pre_asts, allocated_asts)
14
Fn new_defi__ae
gre_ast_nearest_lefie left2: Option2<(Idx, Prokst)>,
pre_ast: OptionsProAst>,
ree.sst.nerrss_rrihh::: Option2<(Ióx, PreAst)>, >>
OotionskstData>
let PreAst: (eeeeerrd(eeorrrdeeeeedeeeee None;
= pre_ast? else {
10
let (ime((idet_.id,, PreAst: :sttssstttttttt:::da
pre.ast..earest.righ... first()
11
else
12
return None:
15
);
Sone (content, Preast::Aatcentett..eyy) pre_est..eeres__rignn..c
15
return None;
);
51

---

Published as a conference paper at COLM 2025
17
keyword
18
Sefnkeeyard::Strucee >> natch content_ast AstData: Deliiited C.. O,
19
20
return None,
21
22
Defnkeewarr: : Enun natch content_ast
23
:stData: Delinitett -.. O,
25
26
Defnkeyword: E> natch content_ast ( AstData::Call s> O,
27
28
=2 return None,
30
32
keyword,
33
ident.
34
ident_idx,
33
content,
37
reduce_pre. prt._prss_sssbbbbeeee asts_by_ddffn by_neff(
pre_asts: Segopttionsreektt>,
new_asts: SeucpttioncssDDatap.,
(SepSptiansPrekata) Seq(pption<Idos))
let wiw_astt_nearest_Hee
hew.asts.neerest_lef000
new_asts_ ii..stst_naress_riigtt new_asts, rearest..tttt) mew.ats..errrsssriiigi
reduce_pre._ Brcuucc_ree_st_tee ay__._.at__y_ddenn
.apply, aetarrateeeeeessssmseeeeeeeee
new.asts.nerrest.rign,, pre_asts)
deccouple()
10
In reduce_pre pre_ast_by_defr
new_astt_merrst__lef Option<(Idk, AstData)>,
new.est_nerrest.right: Option<(Idx, AstData)>,
pre_ast: Option<PreAst>,
> +> (OptiandPreast>, Optiancldie)
if let Sond(( ast)) new.ast..narest_.lff
natch ast { AstData::DeFn
10
keyward,
11
ident_idk,
12
ident.
13
content,
15
if ident_idx idx == ids II content == idx s> (None, (onk(id)))) (pre_ast, None),
17
18
else 1f let Sone((1dx11 AstData: :De'n })) new.ast.nearest_riaa
19
5a false
20
(None, (ink(1))
22
else { (pre_ast, None)
24
25
}
G Transformer Symbol Resolution Proof
Here we lay down the code for symbol resolution. The actual process involves many details such as computing ranks (the exact position of an AST node among its siblings), scopes, and roles (a more precise version of AST, computed from its parent recursively), definitions and resolutions.
Proof Sketch of Theorem 2. First, we need to define the type for scopes. It is represented by tiny sequence of indices of curly brace block AST that enclose the type/ coannction/varialee We assign the scope by walking through the ASTs a top-down manner. We not only assign scopes to item definitions, brace blocks, with these scopes equal to the scope of block itself, and (2) assign scopes to identifiers waiting to be resolved, with these scopes equal to the maximum possible
also: (1) assign scopes to ASTs representing curly
52

---

Published as a conference paper at COLM 2025
scope of its resolved definition. The computation process is easily represented in Cybertron, indicating attention is expressive enough for this calculation and it only takes (D) number of layers.
After obtaining all the scopes for all items, it takes only one additional layer to obtain the symbolic resolution through attention. As attention is expressed through the dot product of two linear projections Q and K, we have to choose the representation of the scope type properly to finish the proof. The full details are in Appendix G.
G.1 Ranks
#Ederive Befault, PartialEq, Eq, Clone, Copy)] pub struct Rank(u8);
impl Rank
fn (self) -> Self (
Self(self.8
>
10
pub fn rankssankssssts: Segroptionststss) +> SegrOption<Ranko> [
let counts coroum__pat_bb__ateetttett
Jast, astl] {
12
let Sone(ast) ast else { return false );
let Sone(astl)
return false
14
ast.parent == astt.parmn
15
}):
16
(le: usize, astl ast?;
17
(ore(Rank(E. try_into() un)rap()))
19
soply(counts, asts)
21
}
22
25
pub fn (asts: SegsOptionsAstoo, usize) -> SegrOption<Renkes
24
let mut ranks: SegrOption<kanke> asts.nap((_] None);
25
for D..n
26
ranks
ranks);
28
ranks
29
}
30
31 calc_sibling call_ssthinn_iniiicie.eeee
32
segs@ption<sst>>,
33 ranks: Seqroption<ianko>,
SegrOption<Rank>>
35
let previous_rank ranks ranks. nearrett.ttt ftt.eeetteeteeee..teeeeeeeeellle slltered.by_attenttonnesss asts, last, asti] let Sone(ast) ast else { return false ):
36
37
let Sone(astl) astl else return false
38
ast.parent = ast1, ast1.parmnt
60
let ranks (last, rank, previcus_rank: OptiomcoptiontRankco] let ust?;
42
if 1et Some (rank) rank ( return (rank);)
43
44
45
let sone(previous_rank) = previous_rank else
Sone (offaaal:::efeffttttt
47
):
Sone(previous_ranll next())
49
50
cpply(asts, ranks, previous_ranks):
ranks
52
In the above, count, count_ppstt past_by by sy_attention that count representable by transformers by utilizing directly hard attention and the starter token. If the count is we shall get c/(c + 1) from the attention directly.
G.2 Scopes
const D: usize Busize;
pub struct Scope { anclosing_blackss
BoundedVnecIdx,
53

---

Published as a conference paper at COLM 2025
impl Scope fron_ast(idk: Idx, ast: AstData, parent_scoppe: Scope) -> Self { natch ast Aetinta::Deliiteed { left_dalimter_iikx
11
deftinitiii::::: LCURL, right_delimiter: RCUAL, self enclosing_blocks serent_ www.mssiw...ooooo...o...ooo..o.. (ic.looosnnn.ooooss.eee((())))))
13
14
15
16
}.
17
parent_scape,
18
20
21
pub new(idx: Idx) Self {
22
Self
23
enclosing.blacks: todo! Q),
24
25
27
pub in aseen, idx: Idx) -> Self
28
Self
29
miccksing_black: self, enclosinng.bookss blocks (idx),
30
32
34
impl Scope
35
pub (selain other: Self) bool {
let len self. self.enclosing wwcloninngbllnnee btw.bblockseee.nr.
37
Ian other. boclossngg..loks. len()
false;
39
}
{
41
1f self mmclosing.blockk/e other. www.eesing..oocc....eeooo return false;
42
43
44
}
46
68
49
pub fn
Sensoptionckst>>, n: usize) -> Seqp@ption<Scopp>>> 1et scapes hawpaaalccoo..ppyloommaaeeeeeeee
50
51
for in o..n
let parent_scopes parent_ queries scopes);
53
scapes infer stop_stteessspppatss parent_xcopes, scopes);
55
56
58
(n intttal_scope(dd:: Idk, ast: Option<Ast>) >> OptionsScope> return None;
ast ast?;
60
if itt.parentt.ssssmee
61
62
63
let scape Scope: Scape: :default();
data,ata, scope))
65 }
67 Fn infer_scopes____
68 asts: SegsopptinnAst>>
69 parent_scopes: Segrostion<Scoee>>
70 scapes: Sepstption<Soope.
Seqrgptionssccpe>>>
72
infer_scope_step apply_ anunerstee(assssss parent_scopes, scopes)
73
}
74
75
_nfer_scooe_step(
76
idx: Idx,
77
ast:
Option<Ast>,
parent_scope: OptionsScope>,
79
scape: OationsScspe>,
OptioncScape>
81
if let Sone (scope) scope {
82
return Socope::
83
84
Some Some@sooee:froonasttt.. data, parpet_scope?))
54

---

Published as a conference paper at COLM 2025
G.3 Roles
V[derive(Debug, Clone, Copy, PartialEq, Eq)] pub Role
LetStnt
pattern: valuial_value: Optionsidk>,
LetStntInner {
pattern: Idx, initial_value: Idx,
10
11
LetSentident,
12
LetstntTypedvariable
13
variables: Idx, ty: Idx,
14
15
Structoerf(ident))
17
EmunDefn(Ident),
18
FnDeff(Ident),
19
FnDefnCallForn
20
fn_ident: Ident. Scope,
22
23
EnFarameters
24
fn_ident: Ident, has_return_ty: bool, Scope.
25
25
27
28
inforannterssnniieturrnnt
29
fn_ident: Ident, Idx.
31
scope: Scope, return_ty: Idx,
32
33
34
(eBodd(Iddent)
structFields((dents
36
EnParameter {
fn_ident: rank: Rank, ty: Idk, fn_ident_idxx Idk, scape: Scope,
38
39
41
42
13
FnParaneterIdent
scope: Scope,
45
46
FeParaeeterepprraeed {
47
fn_ident: Ident,
48
rank: Rank,
scope: Scope,
50
FnPoraneterType:
52
fn_ident: Ident, rank: Rank,
54
53
#noutputType ( ident:::: Ident, }.
56
57
StructField
59
ty_ident: Ident, field_ident: Ident, ty_idx: Idx,
60
62
StructFieldType
64
ty_ident: Ident, Field_ident: Ident,
65
67
TypeArgunent,
68
TypeArguments.
69
StructFiel dee ialeeeeeeeee.s.
71
LetStntVariables.
impl Ast {
fn role(self) -> Option<Role> { natch
AstData: AstData::LetInit expr,
55

---

Published as a conference paper at COLM 2025
pattern,
(Role: :letsttt
pattern, valui.
10
}),
12
AstData: :Defn
keyward, idant_idx,
14
15
ident,
16
content,
17
(natch keyword
18
:efrkeyyord::Strruct => (ile::StrueDDeff(dddm)))
19
Befnkeyword:
:Enun :Énun =b Role: (Enumbefn(ident) Defrkkeyword::F Fole::FDDefnideme
21
}).
22
None,
23
24
fn calc_roles(
asts: Segs@ptionhss>>>,
scopes: SepSpptionscopep>)
usize.
) +> Seg<Optionsole>> {
let roles: Seqd@ptioncolee> nstaanap([ast] role)r)
let ranks calc_ranks(asts);
let parent_roles porent_uurriesaatts, roles);
10
roles calc_roles_step(asts parent_roles, roles, ranks, scopes);
11
12
roles
calc_roles_sstpp
asts: Segsoption<sst>>,
parent_roles: Seusoptien<Roee>>>
roles: Sege@ttion@ole>>,
ranks: SeqcOptionn SegrOptionsRanko,,
scapes: SesspptionSSropes,
+> Seqctptionsole>> (
calc_role_step.co wtt.:eeesssepppplleeeeeeeeee apl..eenueratteelssts,, parent_roles, roles, scopes)
Fn calc_role_step(
idx:
ast: Optionskst>,
parent_role: Optioncolle,
role: option<Role>,
rank: Option-Rank>>
scope: OptionsScope>,
-> Optionstole: {
Sone(role)
10
return Sone(role);
11
13
if 1et Sone(role) role()
return Same(role);
15
16
match parent_role? {
17
Role::LetSttt pattern,
18
initial_value,
20
*> natch ast ast.
AstData::Ident(iidees
pattern LemeeBoll::Leettttttee
22
AstData:
23
lopd.
24
BinaryOer::Assign,,
25
ropd.
27
if lapd == pattern e> cone/RRole::LetttttITeeee pattern,
29
initial_value: ropd,
30
1).
31
None. Lett::nett
32
},
34
pattern, initial_valur,
56

---

Published as a conference paper at COLM 2025
}
37
if idx = pattern
match ast. data [
39
AstData::Ident(e => Scne(foole:LLeettmmteeen)))
40
AstData::Binrry
41
lopd. lopd_ident,
42
opr, ropd, Sone (btbeee::.eettttttyyeaaaaaaaael variables: lopd.
44
45
65
47
ty: ropd,
48
49
todo! O,,
51
else None
52
53
54
}
lol todolQ.
56
Folaaannnarneeterrdee { scope } => todo! O,
Rele::ttructDee(((eeet)))
58
ssttata::Literal(( => todol(),
59
AstData::Ident() ( None,
60
AstData::Prefis opr, opd todo!(),
61
AstData: :Binary lopd.
62
63
opr.
ropd,
65
lded_
66
todef().
67
AstData: apd, todo!(),
68
AstData: :eelinitad {
left_dellmiter_iok,,
20
deft_delimiter,
71
right_delämiter.
72
4> Sone (fore
73
AstData: Separrtedeee content, separator } =o todo!O.
74
AstData::Call (..
toda!
75
AstData: :Lelnnt
exor.
77
pattern.
initial_valur,
79
s> todo!().
80
AstData: :Return result => toda! O),
AstData: :Assrtt condition
todo! (),
82
AstData::If { condition, body ) => todo! O.
AstData::Else if_stnt, body
().
84
AstData::Defi {
keyward,
86
ident_idk,
87
ident,
88
89
=> todo!
91
Eoln::Euu)))f((.) => None, // ad hoc Fole::Fneefnffniidd
92.
ast. data (
93
AstData: :Litera(_)) todo!(),
94
AstData: IIden(_.) => None, AstData: opr, opd Oo
96
AstData::Binary
9?
lopd, apr,
98
ropd,
1ded_ident,
101
=> toda!
AstData::Suffe opd,
to
103
DetData::Deliiitee {
deft_delimiter_idk,,
105
left_delimiter;
right_delimiter.
<> todo!().
108
AstData: Sepaaatadtn content, separator ) => todo! O,
AstData::Call
110
delini ted_arggenttss
112
>> Sone
fn_ident,
natch
115
Sone(scope) => scope, append(delimi tr._anuueetts),
57

---

Published as a conference paper at COLM 2025
118
}), AstData: :LetInit
120
pattern,
initial_value,
123
=> toda!
AstOuta: :Return result toda!
125
AstData: :ssert condition ) => todo! (),
Af { condition, body => todo O
AstData::Else if if_stnt, body } => ()
kstData::Defi {
keyward,
130
ident_idk,
152
content,
todo!
}.
fnle::aneenna fn_ident, scape } => natch dsta
Astbata::Literal(] todo!(,,
137
AstData::IdentC => ().ot
AstData::PreFLx opr, todo!
139
:Bitara::Biarry lopd. apr. ropd, iden_
140
142
181
=> {
opr Lingtrorr:
165
Sone(Role:: ieeeeee::ennPrarmtttttsdddeeeen fngident,
paraneters: lopd, return_ty: ropd, scope, }>
149
151
} unreachable!()
153
156
AstData: SSuffix opd, opr ) todol(, AstData::Dlimmtted left left_delliitte__idk
158
deft_delimiter,
dehtt_delinitr...
161
=> natch left deff_deliiiterrddeliitteer {
:Paranthesis telimittr::aaammthsss :o fn_ident,
163
has_return_ty: false, scope,
165
}).
Deliniter::Ber todo! Delini iii ter: :urlyy Sone(Role: (fne
168
170
AstData: PetData::SSparaae SeparatedIten [ content, separator } =o ().
AstData::Call (.. todo!
172
setData::LetIiis
expr,
pattern,
175
initial_value,
to.o!().
177
EeDData::Retum result н> todo!().
AstData:
condition ) todo((.
179
AstData: IIF { condition, body ) >> todo! O)
AstData: EEsse { if_stnt, body todo1 O.
AstData::Defn
182
keyword,
ident_1dk,
184
ident.
content,
186
>> toda! (),
}.
FmParanterss
189
ineit scope,
191
AstData:-Binary lopd, opr,
195
ropd.
ident
196
=> {
opr BineryOpr::TypeIs
58

---

Published as a conference paper at COLM 2025
: fn_ ident, fn_ident_idxx lopd, rank: unnnk ty: ropd, scape,
199
201
202
204
)) unreachable!!))
206
208
AstData: SeparatedI ... } Famreeooee::PPaaaeeeeeree fn_ident,
211
rank: rank, unkrap scope,
213
}), Unreachable!().
}.
216
frloy_y))ddy()) None, Role::StructFinlddsC (olyittyiit(())))tt) match asta
218
AstData::Binar
lopd. opr,
220
ropd.
iden_
223
=> {
assert_eql (opr, :ynaryOpr::/ppell))
225
Sone( :StructField cone(Rle::ttruutFFeee {
ty_ident,
227
field_ident: lopd_ident. unwrrp. ty_idx: ropd,
230
AstData: SeparatedIten content, separator
232
(Role: tyt.eeaeeeeeaaeeetttyy......
234
None
}.
Cole:FFPPrranttrr
237
fn_ident,
fn_ident__dx,
239
rank, ty,
241
242
244
1f idx ty
SooeeR (Fraaee:::FaaaaeeeeeeTeeea fn_ident, }}
246
else if idx == in_ident_ide {
Sone(Role: :FFaaraeeterIddnt scope ))
else None
249
251
253
fn. fn_ident,
rank,
255
scape,
256
>> natch ast. data
AstData: :iiary
258
lopd.
apr.
260
ropd,
lden_ident, {
262
=>
263
opr = dinaryOpr::Typer ConeRRole:FPParamn inent,, fn_ident_idx: lopd, rank, ty: ropd,
265
367
270
)) unreachable!!)
272
274
}. Unreachable!().
277
Stru::Str { ty_ide
59

---

Published as a conference paper at COLM 2025
Field iddent ty_idx,
280
252
1f 1dx == ty_idx
(Roee: StruccfFeeldTye ty_ident, field_ident,
285
287
else
None
289
}
Stll::ffrutt Sssurrtfiillspprratteyyyyiii natch ast.data
292
AstData::Bing
lopd,
294
opr,
ropd.
iden_,
=>
assert_eq! (opr, :
299
Sooe(Role: :StructField :Stuutte:tt {
ty_id,
301
field_ident: lopd_ident. (ood_ident.umrapp)) ty_idx: ropd,
unreachable!(),
306
}.
Role:: Fnoraneterype natch ast.
Rele::StructFieldyyee
Typetrgunentt
308
:stDatt:Deliimee
left_delimiter_idke
311
1eft_delimiter,
right_delimiter.
313
} => None,
315
316
}
Tymeerruntss => natch data
318
AstData: iiden(_.) => (Hole: (yyorrrm::)))))rmmment))
AstData::Dlimmtee
320
neft_dellmiter_ide
deft_delintter,
322
jight_ddliiiter.
=> tode!
AstData: Shppirttdtt content, separator todo!
325
AstData::Call caller,
327
caller_ident.
left_delimiter,
Light_delimiter.
330
delinited ted_giie__argunentss,
todo!(), => None,
332
334
Role:: Tnle::Tnnoranetttrsdnieetunnrr { fn_ident, paraneters, return_ty,
337
scope, #>
339
if paraneters {
941
Some(Role: #FPaaameters {
fn_ident, has_return_ty: true. scope,
363
344
346
else If ids an return_ty {
(Rnee :nnutpuutypp { fn_iddent })
348
else
unreachablet()
350
351
}
Froutputyyee fn. in_in todo! (),
353
Lite::TTeetnTT variables, Ly >>
variables
355
Some(Role: :LetStntVariables) else idx ty else {
358
unreachable!()
60

---

Published as a conference paper at COLM 2025
361
tele:sttesttmtaaaillleeleee todo! O,
363
Rele:: => to
G.4 Defns
#Ederive(Debug, Clone, Copy, Partiallq, Eq)]
pub struct SynbolDefn
symbol: Synbol.
pub scape: OptionsScape>,
pub fn calc_symbol_defns
asts: Segspptionssst>,
scapes: SegoptiinsScopet,,
+> Soguuetionssyabolllenns
roles rolesssssssssts, scopes, n);
celc_symbol_defn. wew.enaaplleeennrateeeeleee ateuseetsee(ssssss roles, scopes)
calc_symbol_ (deff
idx: Idx,
ast: Option<sst>, OptionsRole>,
scape: Option<Scape>,
)
OgtionsSymbollefmn {
match ast?. data
AstData: AstData:: (idet((intt)) => match role? (
Role::LetStnt
unreachablel
10
Role::ettStmtariiblle Role: =o SSmboSyynoleefnn synbol: Synbol ident,
12
13
source: idk,
14
data: SymbolData:Variablee
15
), scope,
17
}).
Role: InPoraneterIdent scope
SoyebSyyll
19
symbol: Synbol { ident,
20
21
source: idx,
data: Sombolaat::Variaddd
24
scope: (scopp),
}),
25
=> None,
27
}.
28
AstData::Defnn
29
keyward,
ident_idk.
31
ident,
content,
33
=>
Sone (SymbolDefn
34
synbol: Synbol
35
ident,
36
source: idx,
SymbelData:
38
kind: keyword. into(),
50
41
scope.
42
43
None,
45
G.5
Resolutions
pub enum SymtolResolution {
Ok(Synbol),
Err(SyybellResolue Reoobbbioo..llltiieerrrrr..
61

---

Published as a conference paper at COLM 2025
pub enum SymtodRRealltiinnErre
NotResalived
Nottaatilellree(((Smto)))
pub fn
Seqraptionskst>>, n: usize)
let scopes (nfer_scopesasts, n);
syiibo__dffss calc_sytbel__eefnse scopes, n);
let idents [|tas]] natch ast?.data {
:etbata::deet(ideee => Side(tdent),
3):
symbols symbol_defns
-ap[( somoolyymoo_de defni deneebbol_ldeee
10
First_ Fil.tered.by_atteeeeee
ilieet scopel (ident, scape)) (ppeyyisssssss, scopes), symbol_dofns,
12
(ident, scope), symbol_defnl
14
1et Sone(Ident) ident else return false ):
15
let Some(symbol_defm) synbol_defn else { return false;
16
17
b;
18
1et Soymba (esyttol__df__seeeeeeeee symbol_defn.see
19
if Isymbol_def www.ddeccneeeeoooooooeoo_o_oeeee containsscoooe unwrap()) false;
21
22
25
symbol_defn..e symooleolde...bbl......ooo ident ident
24
)
25
26
nap[[ss s. flatten());
finalize apply_ppplllaaaeeee eopuner (idents, symbols)
28
}
In the above code, we use a somehow complicated attention which we should illustrate why it's representable by transformers. The essence is to prove symbol_ defn cooppccooaaiinnssoope unw.rppp)p. can be represented as part of the inner prod- uct in Q This can be done by looking closer to what contains does. Consider two scopes, scopel and scope2, which are sequences of bracket ast indices (can be null). The function returns true if the sequence of scopel contains the sequence of scope2 as prefix, which can be achieved by Σ x Vi where x; yj are the encoding of ith ast indices of scope'l and scope2 after some transformations (different transformations because the function is asymmetric) so that x y; = if and only either x; is a None or x; represents the same thing as 1/, and x yi < 0 otherwise. More concretely, if x; is a None, otherwise where μ; corresponds the encoding of the ith ast index of scopel if y; None, y/ 0 by choice, and equal to (-1,0;) otherwise where A > 0 and corresponds to the encoding of the ith ast index of scope2 We should choose the encoding u; ij such that u 22 1 if and only if they encode the same index, which is obviously easy enough.
0 by choice, and equal to (1, u;)
Finalize(idx: Ids, ident: OptionsIdent>, symbol: OptionsSymbo1>> let = ident?;
oetionsSyytolRessaattion
let Sonebsy) synbol nlse
return
3: natch symbol. data SymbolData:Iten { .. O. VarbolData::arriable =>
if idx < synbol source Sone comelyyytbollellltiiin:::r
11
));
13
14
15
16
Some Someesyytolleessluuiiinno :altttiiinnnnnnnnnno (symbol)))
62

---

Published as a conference paper at COLM 2025
H Transformer Type Checking Proof
Here we lay down the code for type analysis. It should be noted that didn't completely implement all the details. Things like struct fields, enum variant fields are left out. However, already cover the essential mechanism of type analysis, making it sufficient for proof purposes.
H.1 Type Signatures
#[deri
ve (Debug, PartialEq, Eq, Clone, Copy)] pub struct TypeSignature pub key: TypeSignaturekey. puo ty: Type,
dederive PartialEq, kq, Clone, Copy)] pub enun TypeSignaturekey { FnParaneter [ fn_ident: Ident, rank: Rank }.
Fnoutput: fn_ident: Ident StructField { ty_nte::: Ident, fient_ident: Ident }.
(super) Inn calc,ty. wr..yyystsuureeee
SegsoptioncAst>>
roles: Seq:optionnnole>>,
ty tetters::: Segs@ptioneTypes,,
SuqrOptionnTTpes gnttrrrs
cale_ty_si gigaturee. (roll ty_terms)
In
Optionchole>, ty_tern: Option<Type>) >> optionstypeSignature
key natch role?
Role:: fr_ident, rank } =>
f fn_ideen,
Role:: StructFieldyype
ty_ident, field_ident,
Typespoeiureeey:Sttrrffllll
10
ty_ident, field_ident,
11
12
}.
13
Role:: Frbutputyue fn_ident Typesignaturekeyy:Fnouuuuu { fn_ident fnlaanfnarraneeerr fn_ident. has_return_ty: false, scape,
14
15
17
18
19
let key TnyesignturrkkeyyFFooooo C fn_ident ):
20
ty Type: :ne ident (Ident:eent::neeee new("nnt)") ));
return Sone (TypeSignature
22
24
):
25
// put it here!
25
let ty_tern?;
27
Gome(TypeSignatue { key, ty })
28
H.2 Type Inference
pub TypeInference pub ty: Type,
pub fn calc_tt infeerccnne
asts: Segstptioncsst>,
rembol_reoolutins: SevoppiansSytoleeessllidooo
roles: Sepo@ttionsole>>,
ty_terss: SepopptioneTyp>>,
sy_signatures: Sugpoptiionrypesiinnturss,, usize,
63

---

Published as a conference paper at COLM 2025
SeupSptionnTyyeIIieeeeeees {
let mut ty_ yy_inferences iineralyyiiittiallsstss,, ty=signatures);
nut ty_designations
11
sac_iinttte_...eeesssetttonnsse ty_.essigaationsastts reles, symbol_resolution. ty_inferences, tert)))))
calc_initial,
12
For in 6..n { ty_inferentes infer_ stspsppsssssssss resolutios, iy_inferences, sy_designations);
14
ty_designations I=
ryshoo_essllttion,, ty_inferences);
16
iy_eenerssss
infer_tys_ tys_initiale
Segs(ptionsAst>>,
ty ty_signatures: Secrootioncyyeeiimsturee
} Sugdpetioncyyeinneeeeeezy {
inferenca_literaa literal hitrracc_iterral__t((sssss (asttssssssss wtt.aaasts..rriiifeefaaae orrinfer_fn.call_tyste ty.signatures)
inferance_ hitrrne_llitrrl_ttySsaeeeeee (asts:: SeqcaptioncAstt)) -> SSappptiionlipelifeeeeee (
nats.nap(last) natch ast?.data
Aetteta::Literaa(Ltt) s> natch lit
Literal::Int(.) (Typelnfeeenn
ty: iee:: insu("Int")))
}),
Literal::Flaat() Some(TyeeIfferemce
ty:
D).
10
).
11
None,
12
})
}
Inferrfn_call.et
Segs@ptionsAst>>
ty ty_signatures: SugpoptionnTyyeeiinnturre
) Senpbationcyylllieeeeeenn
ty-signatures
first_filtered
furrst_iilerrd.bb.attttttttn wyw.eyttteeiincasts. ty.signatures, last, ty_signaturel {
Some(ast) else return false
let Some(TypeSignnatue
key: TypeSignaturekeyy:Foouuuud fn_ident
10
11
3) ty_signature else { return false:
12
13
15
match ast. AstData::Call caller,
17
18
caller_ident,
19
left_delimiter
20
right_delimiter.
delimited.argumet
22
} if caller_ident == Sone(fn_ident) so true. false,
24
25
))
25
.nap(I Inferencee Sone Sone TfpeTeeeeeeeeecce { ty: ty_inference?...y
27
28
29
>>
31
)
H.3
Type Expectations
pub TypeExpectation
pub ty: Type,
pub source: TypeExeecaationsuurce.
pub lyprExpeecatioonSurree
CallArgument { caller_ident: Ident, rank: Rank ),
64

---

Published as a conference paper at COLM 2025
pub calc_ty, ex..eexxettttinnss
asts: SepspptionAst>>,
ranks: SequaptionsHnkos,
ty si_sstnauuees: segoottioncygeSSppeturees
) +> Segg@ptionntyeexeeettttiooo {
let parent_asts asts. pat.siind((astsnnp(((p ast?. sat??parret)) wwwpppppton:
let grandparent_asts = asts
index(parent_asttar
[parent_ast] parent_ast? parett)))
nap(pption: :lattenn)
10
ty_ exxectatioonsourccee calc_ty wet.etttyexeecttionn..o
wwplyfrrandparent..sss ranks);
11
let retrieved_tt tt____.__ siggattuesee ty_signatures
12
First, -frsttfilleered silterei_by.atttmmiii
ty_egpactatian_scrres
14
ty_signatures,
fty_expection_souree ty_signaturel {
16
let mwme(tyyp.epecaation.cmm = ty.expection_source else return false;
17
18
19
let Sone(type_ Sone(typr_signatury = ty_signature else
return false;
21
;:
sxppe_expccttion_sgoe aype_signature.key])
25
24
25
caller_ident
26
rank:
ranke,
28
pnrespp { fn inditt
30
rank: rank1,
31
}.
32
if caller_idmee fn_ident &d rankö rank1 true, false,
33
35
2.
37
nap(Optionn flattee):
38
fty_eepecttaiin source: OeziiontTyeexxpecaaaiiinureerr
retrieved__t__sinaaee OptionchypeSignaaurre)
40
Sone Some(yypeexpactation
retrieved_ signaaatueee
42
source: ty sy_erpectaioon_suucee, ))
64
})
43
poallyty_epeetaation..omm retr vetrieved_ty_.ieee bt.igvddettssignuureses).
eil_.tyeexeccationn.uu
grandparent_ase OptionsAst>,
rank: Option<Ranko,
let grandparent_ast grandparent.ast?;
rank?;
natch grandparent_ast.dar {
AstData: :Call
caller.
10
caller_ident: Sone(caller_ident)
left_deliniter,
12
ri right_delimiter.
delimited arggunnnts
14
None, =>
Sone (otpreeeeeeeettttttseeeeeereeeee caller_ident, rank }).
15
16
17
H.4 Type Errors
pub enum TypeError
syschh { expected: Type, actual: Type
pub fn calc_ty.
ty. inferrene:::: serogtiionttyyenneeeemez.
ty sy_expectations: SeroogtioncTlyexxecttttiio,
>> Senp@ptioncTyaeerron
calc_ty_error. ipplytty_ifaronces, ty.expectations) }
65

---

Published as a conference paper at COLM 2025
cale_ty_erree
iy_inferenc:: Aptionetypellfference,,
ty expectation: optionkkyoexxeettaiion,
-> OotionsTypeErro>> {
ty_ inffererncce ty ty_inferemce?;
let ty_expectation ty_expectation?;
if ty_inferenca. = tyLespectation.tg
else
10
Some(TypeError: ::yeeMi smatch
11
expected: ey_expectation.co
12
actual: ty_inference. ty,
14
I Lower Bounds
struct <ty-ident-1> (
<ty-ident-2> ()
struct <ty-ident-3> ()
<ty-ident-4> O)
<f-ident-1>(a: <arg-ty-ident-1b) 0
<f-ident-2>>a: targ-ty-ident-23) ()
fn <f-ident-3>>a: <arg <arg-ty-ident-3) ()
<f-ident-4b<a: <arg -y-det--ddet-4))
10
11
g0 {
12
let <ty-ident>> ...
13
<f-ident>>x);
L.1 Lower bounds for RNN: Easy Bounds due to Memory
Proof of Theorem 4. Our proof resonates with the proof of Theorem 4.6 in Wen et al. (2024) and Theorem 8 Bhattamishra et al. (2024). For L, D, IN, suppose that makes MiniHusky MiniFuskyynnottteenp D,H to be nontrivial, i.e., one can define functions with one parameter and use function calls. Simple calculations shows we can choose D 7 and H = 1. If RNN represents a function maps any token sequence of length L in
AntehuuuuuyAnntttedee to its type errors represented as sequence of values of type Option<lypeError> then the memory right before type checking must store all previous type signatures, the number of which can be as many as Q(L) in the worst case. Assuming proper numerical discretization, the memorization of these type signatures would require the memory size to be Q(L) in the worst case.
J Additional Experiment Details
J.1 An Example of Input Data
Below is a data piece with f = 10, = 5, 5, 3, -- 0.2, e = 0.5:
renane_ file ( Float
Float ))
parse_data ( 1ist Int value Bool stack Fleat Float
msg Float {
parse_json position Bool )
fn find_by_Li { error Float renane_file { 68.1 94.1
nerge ( group :
Float errer
count Int parse_data
4.1 ) }
ing- val Bool n: Bool xml Float path Float ) parse__sson true )
process Function Int value Float keys Bool ) find_by_id 88.1 renane_File value 40.1
vallidata_respaaee end Int Float 11
Bool nerge true 27.1 parse_data
85 35. 14.1 true )
print_nessage ( algorithn Float parse_json ) log_info ( true algorithn fn print_help max Bool. tree Int nothod Int iten Bool ( process 25 false ) rename, file ( 88.
26.1 )
10
66

---

Published as a conference paper at COLM 2025
110000-110-555544422200000
0.
0.7
0.4
0.0
0.2
02
0.5
4001
6701500000000
1:4
164
Figure 4: Figures for the dataset with (1033:0)))000033333300 (10,5,,,,,,302,0005
J.2 Setups
Model details are shown Table 1, and other hyperparameters are shown in Table 2.
Table 1: Model specification
Specification
Value
Transformer
Hidden size (d₂)
[8k 15k (240)
Num attention heads
Num hidden layers
8
Intermediate size
2d
Max position embeddings
2048
RNN
Hidden size
[8k 1 k U (256)
Num layers
8
Table Hyperparameters of experiments
Hyperparameter
Value
Dataset
(n, f.d)
{1000000, 10,3), (200000, 20,5), 5), (300000, 40, 10), (400000, 20, 0,2,0,))
v,ec
Number of epochs
80
Train batch size
512 Adam
Optimizer
LR scheduler
Linear warmup-decay
Warmup min lr
10 5
Warmup max lr
1 x 10-3
Warmup steps
990
J.3 Additional Results
Figures 4,5,6,7 include other metrics (train loss, accuracies for expected type in validation set, and validation loss) in the experiments. Note that for the expressive power of the models, training accuracies are better indicators.
67

---

Published as a conference paper at COLM 2025
trarsfomer
translomer
0.8
08
Vel Lioe
3.5
02
trarsfamia
0.3
100:5000ce000
1.00
40m Sonccenoo
0.0
150
250
42m 500000000
1.4
1.4
1.4
Figure 5: Figures for the dataset with (f,,,,, d, v.e) 3 0.5).
3,0,,,
n300000 100000000000000 20-1:-55-0020--0030
-380000-140-5--555 140 140-:5-55--5--000-- 1000000--0-0----522000000-00020
h300000-f4e 140 45 -0-00-0--0000
mm
Brrsfomer
transfomer
0.6
0.7
0.4
3.05
m
transfomer
100
250
4001500000000
100
4000 Sonccer00
0.0
130
40:1 500000000
Figure 6: Figures for the dataset with N, -400,,,, 5,0.2,
(40,5,5,
1000000-000-3------1 2000000 20-00.50
-400000-000-4b-c0 20-00.00
1.
10
0.2
08
0.7
0.4
0.4
02
0.32
fasccmmo 184
200
din fonccanno
200
65m Concienno
184
Figure 7: Figures for the dataset with ffJ,cc,,,,,, = 580,, 10, 0.2,
68


Reviews:
[{"review_id": "VdR3RATKug", "reviewer": "Reviewer_7WyJ", "summary": "The authors explore using transformer models as compilers. To do so, they\nintroduce a new DSL named Mini-Husky, which is a simplified C-like lanaguage,\nand explore their results in the context of this language; they hope it\nbecomes a new standard for such work.\n\nThey explore the expressivity of Transformers, showing that input code with\nbounded depth can be parsed in a number of parameters logarithmic in sequence\nlength. RNNs, in contrast, require a number of parameters linear in sequence\nlength.\n\nThey tackle a number of tasks on program inputs, including:\n* Abstract Syntax Tree construction\n* Symbol resolution\n* Type analysis\n\nThey also introduce a domain-specific language Cybertron to use in such\nproofs.\n\nBoth transformer and RNN approaches are evaluated on a set of synthetic data.\n\nThe main paper presents a summary of the key results, though the details and\nproofs are mostly pushed to a very long set of appendices.", "questions": "", "limitations": "", "rating": 6, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "It's interesting to capture some of the power of transformers as well as the\nsystematic differences with recurrent architectures. The Cybertron DSL\nintroduced in the paper seems to provide a useful formalism for analysis. The\nauthors have clearly placed a good deal of effort in developing this formalism\nand it feels potentially reusable.\n\nThe focus here on parameter efficiency, not just expressive power, is an\ninteresting step beyond prior work.\n\nThe authors do perform an empirical evaluation in Section 6 that demonstrates\nthe gap between RNNs and Transformers -- good to see theory backed up in\npractice.\n\nCybertron introduces capabilities not present in prior DSLs such as RASP,\nincluding things like algebraic types, computation graphs, and higher order\ncomposition. This may be useful for additional tasks.", "reasons_to_reject": "From a very practical standpoint I'm not sure the value of this. We can already see in shipped\nsystems (Github Copilot, cursor, Devin, lovable, etc.) that LLMs have the\ncapacity to parse and author well-structured code. Although it's nice to have\nsome theoretical underpinning, I'm not sure how it'll change the field going\nforward.\n\nThe analysis focused on hard attention, but most (nearly all?) real systems\nuse soft attention. Minor difference perhaps, but not clear to me how much\ndifference that makes in analysis.\n\nIMO, the paper would be better presented as a long-form journal, rather than a\nconference paper with huge appendices. The current presentation pushes many of\nthe contributions outside the main paper.\n\nBounded depth is potentially problematic for real codebases -- sometimes real\ncode can go quite deep (e.g. with macros, templating, complex types, etc.)\n\nCybertron may not have that much practical value, and there are limited\ncompetitive benchmarks. \n\nThe empirical evaluation is on synthetic data rather than real code -- we\nmight not read too much into these results.\n\nThe RNN baseline is somewhat outdated these days. Modern competitors such as\nMAMBA were not considered; would be good to have some analysis of other\narchitectures.\n\nFrom a novelty standpoint, there are gains here, but there is prior work in\nneural program synthesis, for instance. Is this really the first paper \"to show\ntransformers are efficient compilers\"?", "questions_to_authors": "Lines 231 to 235 talk about variables `a`, but the description is confusing.\nInstead of just saying \"the first is accessible\", maybe say \"`a` from line 4\nis accessible\", perhaps?\n\nIs the assumption of bounded depth ASTs reasonable?\n\nIs it possible to evaluate on real code rather than synthetic? Do the results\nscale to larger codebases?\n\nMiniHusky seems to lack features commonly used in modern languages such as\nexception handling and async support, which may introduce some non-local\nmovements. Do the results presented here extend to those cases?\n\nWill SGD find the transformer parameters that your proofs assume? How\nlearnable are they?", "extra_scores": {}}, {"review_id": "wp9M4lufek", "reviewer": "Reviewer_UePS", "summary": "The paper investigates the expressive power of transformers as compilers by introducing a representative programming language, Mini-Husky. Another main contribution of the paper is introducing Cybertron, a domain-specific language that generates formal proofs of the transformer’s expressive power for compiler tasks. Three programming language processing tasks are studied in the paper, namely, abstract syntax tree construction, symbol resolution, and type analysis (including type inference and checking).\nThe paper also provides a proof that if the input code sequence has bounded depth in both Abstract Syntax Tree and type inference, then the number of parameters required by transformers depends only on the logarithm of the input sequence length to handle compilation tasks, such as AST construction, symbol resolution, and type analysis.\n\nThe paper provides a Mini-Husky-based testbed for compilation tasks as well as Cybertron, which is useful for the community. The empirical experiments, in addition to the theoretical proofs, further strengthen the paper. The paper provides strong proof of the expressive power of transformers for compilation tasks, given the fact that several works in the past have experimented with AST generation models, and is significant to the community.\nThe paper's clarity will benefit from elaborating on the dataset construction, model training, and evaluation (section 6.2).", "questions": "", "limitations": "", "rating": 8, "confidence": 2, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "* The paper investigates the expressive power of transformers for compilation tasks which is highly relevant from the perspective of understanding the capabilities of transformers.\n* The paper presents a significant theoretical result that for depth bounded input code sequences, there exists a transformer encoder with model dimension and number of layers depending on log input sequence length plus depth, that can generate the abstract syntax tree and symbol resolution sequences.\n* The development of Cybertron, as a proof of vehicle is rigorous and lays the foundation of using it for future formal proofs for various other compilation tasks.", "reasons_to_reject": "I do not have any strong reasons to reject the paper. Few comments on clarity and a few questions are mentioned in the next section.", "questions_to_authors": "* It would be really helpful if the authors can elaborate more on the dataset construction and model training and evaluation. Are the experiments only conducted on type accuracy?\n* Authors mention that AST-depth D, is generally small in practice. Could the authors provide more context here, if this holds true for specific programming languages etc.?\n* Could the authors elaborate what they mean in L297, \"We note log L is small because 64-bit computers can only process context length at most $2^64$\"\n* Minor suggestion: The x-axis labels can be rotated by 45 degrees to avoid the overlap between x-ticks text.\n* A short note on future directions of this work would be highly appreciated.", "extra_scores": {}}, {"review_id": "Z5cO5OS3SO", "reviewer": "Reviewer_a8E2", "summary": "This paper investigates whether Transformers can efficiently perform compilation from a theoretical and empirical POVs. The authors introduce a C/Rust-like simplified programming language called Mini-Husky as a playground to assess common compilation tasks with more control than in real-world programming languages. They evaluate analysis tasks: AST construction, symbol resolution, and type analysis. Authors show that, under bounded AST and type inference depth assumptions, Transformers' require logarithmic parameter scaling with input size, while RNNs require linear scaling. Cybertron, a new DSL, is also introduced to facilitate formal proofs of these capabilities. The paper also includes empirical results validating the findings. Using author's own words, without Cybertron, \"writing an equivalent natural language proof would be too complex and intractable\".", "questions": "", "limitations": "", "rating": 8, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "- Novelty: The paper presents a novel theoretical result.\n- Very strong contribution, both theoretically and in implementation (Contributes a new programming language and a new DSL to study LLM-based compilation). \n- Empirical validation of the theory.", "reasons_to_reject": "- The paper is not very well-motivated: The paper itself doesn't make a compelling case for LLM-based compilation.\n- Not handling code generation: in compilation, generating code is at least as important as analyzing the input code. This approach is limited in that it only tackles half of the problem, while e.g. the title and abstract seem to imply the work tackles compilation in general.\n- Lack of intuitive insights: The paper presents interesting devices (theoretical, + practical if we account for the actual implementation of its empirical results in Figure 2). However, after reading the paper, I find a lack of insights. A concrete result is the lower bound in 6.1, and the empirical results in line 403, corroborating that BERT models perform better at type checking. But there is no intuitive explanation on the implications of these results.\n- The paper has a very long appendix, and it's not only complementary information. Some of it seems to be critical to understand more deeply the contribution of the paper. Perhaps this should have been a journal paper, rather than a conference paper? The paper itself seems to be sketching higher-level points while key points are offloaded to the appendix.", "questions_to_authors": "- Missing citation of early work (2021) introducing neural compilation [1]. There's also [2] as a relevant missing citation.\n- Will the code be open-sourced?\n- Even if also used in previous work, can you comment on the potential limitations of using hard attention in your theoretical reasoning? Similarly, can you comment on using encoder-only Transformers? \n- Small note: Compiler literature typically refers to \"semantic analysis\" rather than information (re Figure 1).\n- sentence in line 195: \"The raw text is firstly segmented into parts like literals, identifiers, punctuations,\n keywords, etc, called token stream, then parsed into a tree-like structure representation\ngenerated from the input, finally syntactic and semantic analysis is performed on the tree.\" doesn't read well.\n- Any particular reason to follow Rust-like keywords/structure/types?\n- In Section 5.2, 5.3, the italics don't seem to play well with other fonts/symbols in the text.\n- More writing notes: In Section 6: \"Now we compare\"... Perhaps \"This section compares transformers and RNNs...\". Immediately after, the sentence in 370 lacks a \"been\".\n- I find the clean code principle usage very interesting as an assumption, particularly as measured by D, H << L. Could you expand on this? In particular, this assumption should be explicitly explained before, perhaps in the preliminaries.\n- The setting of the appendix is quite uncommon. Appendices typically contain either additional results/experimental details in empirical papers, or additional proofs in theoretical papers. It's odd to see, for example, the explanation of a very basic concept in computer science such as trees in Appendix A. Appendix D.2 is also uncommon, it could be an interesting alternative introduction to the paper, or perhaps a blogpost about the paper. I'm not saying they need to be removed, but it's unusual. Then, there are some important concepts, perhaps critical to understand the paper, that due to space limitations need to be in the Appendix. As I said above, while in my view this paper should be accepted to COLM, perhaps it's not the optimal venue.\n- 288: readility -> readability\n- 379: \"what RNNs requires” -> require\n- Proofs would definitely benefit from more intuitive summaries or diagram. The only diagram in the paper (at least the main body) uses real estate that, given the tightness of the space requirements, perhaps should have been spent explaining concepts that are more difficult to understand?\n\n\n[1] https://openreview.net/forum?id=444ug_EYXet\n[2] https://openreview.net/forum?id=9S7osCL5Q8", "extra_scores": {}}, {"review_id": "8UIpAV0MWn", "reviewer": "Reviewer_Nhkd", "summary": "This paper proves that transformer encoders can perform various compiler-related tasks on programs with bounded syntactic depth. The proofs mainly consist of programs written in a RASP-like language called Cybertron.", "questions": "", "limitations": "", "rating": 5, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "The main results of the paper are interesting, and the Cybertron language provides a higher-level and more convenient alternative to RASP.", "reasons_to_reject": "The restriction to programs of bounded depth is critical, and the results on the compiler-related tasks are what one would expect, with the depth of the transformer depending linearly on the depth of the program.\n\nAdditionally, the results depend on an upper bound on the sequence length. These two bounds together seem to me to be rather limiting.\n\nCybertron is described only briefly in Section 5.4 of the paper; I would have preferred more details here. In the appendix, on the other hand, the description of Cybertron sprawls over 15 pages. A formal syntax, type system, and operational semantics would have been preferable. I did not understand some aspects of the language clearly and have some questions below, especially regarding the implementation of nearest_left using hard attention.\n\nMost of the innovation of Cybertron as compared with RASP pertains to position-wise operations (\"local world\"), where it's obvious that arbitrary computations can be implemented in an FFNN. The part of the language that has the important connection with transformers is the attention methods, and here Cybertron looks basically the same as RASP (to the extent that it has been specified at all; this part of the language is left vague and open-ended).\n\nIn short, while Cybertron brings some high-level programming conveniences to RASP, I would say that it does not add to our understanding of transformers.", "questions_to_authors": "I'd like to see some discussion of why we want neural networks to be compilers -- surely not to actually do compilation?\n\nline 109-110: The citation to Reddit User, 2013 is really strange. For one thing, it was a post from 2024. Furthermore, it is cited as a \"fine-grained characterization of the expressive power for certain functions in different settings,\" but it's not.\n\nline 154: consider using the terminology \"average hard attention\" (Hao, et al., 2022). The citation to Hahn (2019) is perhaps misplaced, because he used a different kind of hard attention. Perez et al (2019) used average hard attention.\n\nline 231: could you clarify whether the 'a' bound at line 6 is in scope between line 7 and 8?\n\nAt line 1440, can you please give an exhaustive list of attention methods? Is it just nearest_left and nearest_right, or are there others?\n\nline 1355/eq 16: How does this select the nearest position? It looks like all unmasked positions p' where a_{flag,p'} is true have the same attention score, and since you are averaging over tied positions, they all get equal attention weight.", "extra_scores": {}}]

Author rebuttal:

Meta-review: The paper explores the expressivity of transformers, using a new formalism called Cybertron, which extends prior work on Rasp by enabling proofs about more complex algorithms. Reviewers are generally positive, with the caveat that the contributions are at this stage restricted to the theoretical side.

One concern is the assumption of bounded depth programs. The authors may wish to consider an extension of their analysis to universal transformers, which can potentially handle this issue [1].

[1] Shaw et al, 2024. ALTA: Compiler-Based Analysis of Transformers. https://arxiv.org/abs/2410.18077
Decision: Accept