Synthesis and Verification of Transformer Programs (Technical Report)
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866911690070687744 |
|---|---|
| author | Jiang, Hongjian Hague, Matthew Rümmer, Philipp Lin, Anthony Widjaja |
| author_facet | Jiang, Hongjian Hague, Matthew Rümmer, Philipp Lin, Anthony Widjaja |
| contents | 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). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_16473 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Synthesis and Verification of Transformer Programs (Technical Report) Jiang, Hongjian Hague, Matthew Rümmer, Philipp Lin, Anthony Widjaja Machine Learning Formal Languages and Automata Theory Logic in Computer Science 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). |
| title | Synthesis and Verification of Transformer Programs (Technical Report) |
| topic | Machine Learning Formal Languages and Automata Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2602.16473 |