Synthesis and Verification of Transformer Programs (Technical Report)
Authors: Hongjian Jiang, Matthew Hague, Philipp Rümmer, Anthony Widjaja Lin
Organizations: University of Kaiserslautern-Landau, Germany · Royal Holloway, University of London, England · Uppsala University, Sweden · University of Regensburg, Germany · MPI-SWS, Germany
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).
Figures & tables
SL Synthesis
Program Minimization
Constraint Learning
Language
TA (%)
EA (%)
Time (s)
R
Synth (s)
Verif (s)
R
Synth (s)
Verif (s)
Dyck-1
99.75
99.5
3.92
21
27.7
41.7
12
–
–
AStarBStar
100
100
24.62
11
7.7
46.8
1
10.2
8.9
AnBnCn
100
100
80.05
22
88.7
42.4
2
–
–
AAStar
100
100
1.57
4
1.0
10.0
1
15.5
8.3
ContainsAB
100
100
17.35
6
2.2
12.5
1
145.0
10.42
Table 1: C-RASP synthesis results across benchmark languages (timeout: 300s). SL synthesis reports train accuracy (TA), evaluation accuracy (EA), and runtime; program minimization and constraint learning report refinement rounds (R), synthesis time (Synth), and verification time (Verif). “–” indicates that no 100%-accurate program was found within the timeout.
SL Synthesis
Program Minimization
Constraint Learning
Language
TA (%)
EA (%)
Time (s)
R
Synth (s)
Verif (s)
R
Synth (s)
Verif (s)
Parity
83.12
82.50
185.63
-
-
-
-
-
-
Tomita 3
79.25
78.00
228.94
-
-
-
-
-
-
Tomita 5
79.44
71.70
112.23
-
-
-
-
-
-
Tomita 6
75.75
71.48
183.61
-
-
-
-
-
-
Table 2: C-RASP synthesis results for languages beyond C-RASP’s expressive power
Task
Val0
Val1
Val2
Time (min)
012Star_0_2Star
82.2
58.2
42.8
20.88
AAAAStar
74.7
73.3
63.4
48.93
AAStar
69.4
54.6
53.2
17.74
AAStarBBStarCCStarDDStarEEStar
97.4
71.5
53.6
24.82
ABABStar
75.1
75.0
75.0
48.34
ABStar_D_BCStar
94.8
62.0
42.5
16.19
Table 3: Transformer training validation accuracy (%) at lengths ≤50 (Val 0 , training), [51,100] (Val 1 ), and [101,150] (Val 2 , generalization), and training time (min) for all tasks.