---
title: "Synthesis and Verification of Transformer Programs"
authors:
  - "Hongjian Jiang"
  - "Matthew Hague"
  - "Philipp Rümmer"
  - "Anthony W. Lin"
doi: "10.24963/ijcai.2026/434"
url: "https://ijcai.org/proceedings/2026/434"
pdf: "https://ijcai.org/proceedings/2026/0434.pdf"
venue: "Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence"
year: 2026
pages: "3899-3907"
track: "Main Track"
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"
---

# Synthesis and Verification of Transformer Programs

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

*Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence*, pages 3899-3907. DOI: [10.24963/ijcai.2026/434](https://doi.org/10.24963/ijcai.2026/434)

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