Synthesis and Verification of Transformer Programs

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

IJCAI 20260 citations

Synthesis and Verification of Transformer Programs

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

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

Knowledge Representation and Reasoning: Automated reasoning and theorem provingKnowledge Representation and Reasoning: Knowledge representation languagesKnowledge Representation and Reasoning: Learning and reasoningMachine Learning: Attention models

BibTeX

@inproceedings{ijcai2026_synthesisandveri,
  title = {Synthesis and Verification of Transformer Programs},
  author = {Hongjian Jiang and Matthew Hague and Philipp Rümmer and Anthony W. Lin},
  booktitle = {IJCAI 2026},
  year = {2026}
}