Transformers are Efficient Compilers, Provably

Major Theoretical Weaknesses:

• Limited Illustration of Cybertron's Proof Mechanism: The main body of the paper doesn't explain how Cybertron could serve for proving these subtasks that represent transformers clearly. The examples in the appendix are not intuitive for understanding, as they are too implementation-specific. The paper needs revisions on its writing to explain their ideas on how Cybertron is used for proving the capabilities of transformer models. For example, we need at least some detailed minimal end-to-end examples in Mini-Husky for basic statement-level and block-level constructs. I think at least a basic statement-level example, like "a = b + c * d" and a block-level example, like "if(){}" will be needed.
• Language Design and Classification Issues: Mini-Husky is more accurately characterized as a Rust-like language rather than C-like. The choice of Rust-like features may be beneficial for type analysis but should be explicitly justified. The language classification needs to be more precise and well-justified.
• Limited Semantic Generalizability: From a traditional compiler development view, the semantics cannot be fully presented through BNF grammars, as many language-specific features are configurable and implementation-dependent. For example, the authors limit their Mini-Husky language to avoid any type conversion for their type system's convenience; however, this limit also limits the language's generality. For Mini-Husky-2, which allows type conversion, the proof generated by Cybertron is not valid since we need Cybertron-2 to validate it. I think the authors should clarify this key challenge: semantics is different from syntax/grammar, which is why we need language manuals besides BNF grammars to define a programming language. The current presentation seems to overclaim their capability in semantic handling, as the type system in Cybertron is implementation-dependent on Mini-Husky, therefore not generalizable. Current Cybertron is therefore more like a partial compiler (not generating assembly or IR output currently) with type checking tailored to Mini-Husky rather than an extensible DSL, which makes me confused about its effectiveness on other programming languages with different semantics. Authors are encouraged to clarify what the common parts in PLs are that MiniHusky+Cybertron can prove transformers-capable and what are not and need extra development to prove.

Empirical and Evaluation Weaknesses:

• Limited Experimental Validation: Empirical validation focuses only on type checking comparison with RNNs. Missing evaluation results for AST construction, symbol resolution, and comprehensive type analysis. The lack of practical validation weakens Mini-Husky's contributions.

Technical Writing Issues

• Non-standard ICLR template usage: The template it used is not the newest ICLR-template as it differs significantly with other papers.
• Various writing errors: Redundant sentences(line 079-081), Incorrect indentation( line 049: "Taelin (2023b)demonstrates", line 277-280), Incomplete words(line 053: "such as (missing JavaScript)(Flanagan, 2011) and Rust (Klabnik & Nichols, 2023)", line 094: "(T)o our knowledge").
• Too long appendix: Too many code snippets in the appendix, many of them are direct copies of code, which is inappropriate for a premier conference like ICLR. Simplifications and abstractions are needed. Current length in the appendix is too much for any readers to read, including reviewers.

While the paper is overall coherent, I did find some bits to be unintuitive (due to the order in which concepts are introduced) and even obtuse (due to poor prose). For instance, I would suggest modifying/reordering Section 5.4 to first motivate the use of key abstractions (e.g., computation graphs), and then go over what constitutes types in Cybertron, followed by how such types constrain the use of abstractions and ensure the soundness of propositions (e.g., that there exists a transformer encoder capable of symbol resolution). I was unable to form a fully cohesive mental picture connecting these details until after reading this section a few times and referring to the appendices. I understand that the authors are constrained by the page limit, but I would appreciate it if they could smooth out such readability speedbumps. I would personally cut a significant portion of the first paragraph of Section 5.4, as it largely parrots what has been said in the abstract and introduction.

Related to the above point, it would have been better if the authors provided more intuition for the key abstractions (e.g., computation graphs and function compositions) ahead of time in the main text, leading up to the overview and exposition on the type system. I was only able to adequately grasp their roles after going through much of the appendices.

Other than the aforementioned structural issue, I would have to say that the prose of the paper can be dramatically improved. An inexhaustive list of typos I found is included at the end of the Questions section. While most of them do not impede understanding, there are a few more serious ones that do (e.g., line 405, incorrect examples in Appendix E.1). I would appreciate it if the authors could correct them and do one more pass to double check.

For the most part, I appreciate and enjoy the formal approach. But on the topic of soundness, I would have liked to see a precise specification of Cybertron’s type system and its correctness (via properties like progress and preservation), in addition to the properties stating whether specific constructs expressible in Cybertron can be represented using MLPs/transformers. In my opinion, this is a missing ingredient that is important for an approach akin to interactive theorem proving. For instance, such a specification would clarify which of the two type errors on line 9 of the code snippet in Section 4 would actually occur, blocking the other from occurring (or not, depending on the specification). Presently, I have no way of knowing such behaviors from the paper alone. On the same point, the authors could have further formally specified Cybertron’s semantics operationally/denotationally/etc. to be the most precise, and proved it correct, which is important for such a formal reasoning approach. Same applies to Mini-Husky.

The paper does not convince the reader that its main claims are supported by proof or empirical evidence. Alternatively, the claims are moot since they only apply to a language whose semantic properties can be checked with bounded complexity (MiniHusky).

The exposition of this paper is too intricate, and most of the body of the paper is spent introducing background definitions and not the actual substance of the claims.

• Theorem 1 is "proven" essentially by repeating the theorem statement. Thms 2 and 3 do not have a recognizable proof. Neither of these are proofs in any useful sense, which is problematic as the paper puts "provably" in its title.
• What is "Cybertron"? We don't see a compact definition of this proof language, which is unfortunate because this is the main technical device of the paper. Only in the middle of Section 5.4 (line 409) do we get a hint of what is this Cybertron, whereas this should be moved up to where it's first mentioned. Appendix E starts with what are supposed to be examples but are exactly the same code snippet repeated 4 times.
• I do not find support for the claim of exponential separation between RNNs and transformer models wrt model size parameter in the type inference task (claim 3 in the Contributions section). From figure 2 it seems that both model classes saturate in accuracy at comparable sizes.
• Section 3 the Preliminaries material could be easily moved to the appendices, as it's not used in the body of the paper.
• It should be stated more clearly that the claims are only relative to the object language introduced by the authors (MiniHusky). This language apparently is designed to have "shallow" ASTs and a bounded complexity of type inference, but neither claim is proven in the body of the paper.
• The "clean code" heuristic suggested as a justification for MiniHusky is only cited but never formalized. On the other hand, this was a set of folklore programming practices and not grounded in theory since their inception.
• There is a lot of ad-hoc technical material in the appendices (which by the way does not cite any preexisting literature), but it is very hard to connect it to the main body of the paper. Much of the "proof" content is apparently limited to its Rust implementation, which is unfortunate for those who cannot easily compile and run it in their heads.
• Figure 2 is hard to read and does not make a clear claim, esp re. the "first 8 points" remark. Similarly, the other figures with experimental results at the end of the appendices are given almost without comment.

Minor comment: it's unclear why the authors choose to repeatedly call out AgdaJS in the beginning.

(1) The paper is fundamentally incomplete: while the authors claim to introduce Mini-Husky as a pared-down programming language, they do not do this at all in the main text of the paper, and even in the extensive appendix, they do not actually provide a full definitions of syntax or semantics.

As example, note that the BNF is Appendix D does not in any way correspond to the example given 5 lines under it, which uses keywords such as mut and assignment operators such as +=, . and assert statements; none of which appear in the BNF. Similarly, no semantics of the language are provided, so it is impossible to verify any proof about its properties. The BNF also does not cover the syntax for type annotations, which is crucial given the paper's focus on typing tasks.

(2) The paper is overclaiming: no attempt is made at showing the suitability of Transformers as "compiler", as two core phases (code generation and optimization) are not even discussed. Text and helpers such as Fig. 2 seem to be written as if compilers only analyze code, but do nothing else. The term "efficient" is used repeatedly without a definition, and it remains unclear what is viewed as efficient (is it meant as running in polynomial time, or in the less formal, but better understood way of being acceptably fast?)

(3) The paper is not well-written, often referring to concepts, identifiers or ideas not introduced. Examples:

• "the computation process is easily represented in Cybertron" (line 358), when Cybertron is only introduced in the following section
• $L$ in line 318 (its meant to be the sequence length I assume, but the last use of $L$ was in l196 and refers to the number of layers)
• "As types are mathematically interpreted in this paper a discrete subset of a vector space" is the only mention of a representation of types in the main text.

(4) The citing of related work is often incorrect. For example, Sect 3 starts with "The major innovation in the transformer architecture is self-attention", which is surprising given that the Transformers paper ("Attention is all you need") has a related work discussing prior uses of self-attention. On the other hand, the contrast to the most related work to the submitted paper (RASP, Weiss et al. 2021) is not discussed beyond a "Cybertron has a powerful algebraic type system that helps to prove complicated operations beyond simple algorithms" (though that type system is not actually introduced in the paper).

Let me be clear that none of the criticism above is about the actual research, but only about the presentation - I don't feel it's possible to fully grasp the proposed ideas given the paper. To some degree, this is a consequence of the ICLR page limit, and so I would make the following two suggestions to the authors:

(i) Submit to a venue with a longer page limit (e.g., TLMR, or POPL/PLDI/OOPSLA as conferences on the PL side that were open to such contributions in the past - in particular POPL seems appropriate). This will allow for a longer exposition and inclusion of more of the crucial details in the main text.

(ii) Think about the core ideas that make things work, and try to focus the exposition on that. For example, RASP already showed how to express primitive programming constructs as parts of a Transformer, so what is new here? What changes are required to make the proofs work? Think back on early steps of the work: what challenges did you need to overcome? These are the things most interesting for other researchers.