Synthesis and Verification of Transformer Programs

Jiang, Hongjian; Hague, Matthew; Rümmer, Philipp; Lin, Anthony W.

doi:10.24963/ijcai.2026/434

Synthesis and Verification of Transformer Programs

Hongjian Jiang, Matthew Hague, Philipp Rümmer, Anthony W. Lin

Download BibTeX Cite

Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence. Main Track. Pages 3899-3907.

https://doi.org/10.24963/ijcai.2026/434

Keywords

Knowledge Representation and Reasoning: Knowledge representation languages
Knowledge Representation and Reasoning: Learning and reasoning
Knowledge Representation and Reasoning: Automated reasoning and theorem proving
Machine Learning: Attention models

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).

Hongjian Jiang, Matthew Hague, Philipp Rümmer, and Anthony W. Lin. 2026. Synthesis and Verification of Transformer Programs. In Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-26. IJCAI, 3899–3907. https://doi.org/10.24963/ijcai.2026/434

@inproceedings{ijcai2026p434,
  title     = {Synthesis and Verification of Transformer Programs},
  author    = {Jiang, Hongjian and Hague, Matthew and Rümmer, Philipp and Lin, Anthony W.},
  booktitle = {Proceedings of the Thirty-Fifth International Joint Conference on
               Artificial Intelligence, {IJCAI-26}},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},
  editor    = {Diego Calvanese},
  pages     = {3899--3907},
  year      = {2026},
  month     = {8},
  note      = {Main Track},
  doi       = {10.24963/ijcai.2026/434},
  url       = {https://doi.org/10.24963/ijcai.2026/434},
}

TY  - CPAPER
TI  - Synthesis and Verification of Transformer Programs
AU  - Jiang, Hongjian
AU  - Hague, Matthew
AU  - Rümmer, Philipp
AU  - Lin, Anthony W.
T2  - Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-26
PB  - International Joint Conferences on Artificial Intelligence Organization
PY  - 2026
SP  - 3899
EP  - 3907
DO  - 10.24963/ijcai.2026/434
UR  - https://doi.org/10.24963/ijcai.2026/434
ER  -