![[2602.16473] Synthesis and Verification of Transformer Programs](https://arxiv.org/static/browse/0.3.4/images/arxiv-logo-fb.png){kind=logo}
[2602.16473] Synthesis and Verification of Transformer Programs
Summary
This paper presents C-RASP, a programming language for transformers, and introduces new algorithms for its synthesis and verification, enhancing transformer program optimization and constrained learning.
Why It Matters
The development of C-RASP and its verification techniques is significant for advancing the reliability and efficiency of transformer models in machine learning. As transformers become increasingly integral to AI applications, ensuring their correctness through formal verification can lead to more robust AI systems.
Key Takeaways
- C-RASP captures concepts expressible by transformers, facilitating their synthesis and verification.
- New algorithms developed improve the automatic verification of C-RASP programs.
- The connection to synchronous dataflow programs allows the use of advanced model checkers.
- The paper presents a local search algorithm for learning C-RASP programs from examples.
- Applications include transformer program optimization and constrained learning based on partial specifications.
Computer Science > Machine Learning arXiv:2602.16473 (cs) [Submitted on 18 Feb 2026] Title:Synthesis and Verification of Transformer Programs Authors:Hongjian Jiang, Matthew Hague, Philipp Rümmer, Anthony Widjaja Lin View a PDF of the paper titled Synthesis and Verification of Transformer Programs, by Hongjian Jiang and 3 other authors View PDF HTML (experimental) Abstract:C-RASP is a simple programming language that was recently shown to capture concepts expressible by transformers. In this paper, we develop new algorithmic techniques for automatically verifying C-RASPs. To this end, we establish a connection to the verification of synchronous dataflow programs in Lustre, which enables us to exploit state-of-the-art model checkers utilizing highly optimized SMT-solvers. Our second contribution addresses learning a C-RASP program in the first place. To this end, we provide a new algorithm for learning a C-RASP from examples using local search. We demonstrate efficacy of our implementation for benchmarks of C-RASPs in the literature, in particular in connection to the following applications: (1) transformer program optimization, and (2) constrained learning of transformer programs (based on a partial specification). Subjects: Machine Learning (cs.LG); Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO) Cite as: arXiv:2602.16473 [cs.LG] (or arXiv:2602.16473v1 [cs.LG] for this version) https://doi.org/10.48550/arXiv.2602.16473 Focus to learn mo...
