Synthesis and Verification of Transformer Programs
This work addresses the verification and synthesis of transformer programs, which is incremental as it builds on existing C-RASP language and benchmarks.
The paper tackles the problem of automatically verifying and learning C-RASP programs, which capture concepts expressible by transformers, by developing algorithmic techniques that connect to synchronous dataflow verification and use local search, demonstrating efficacy on benchmarks for transformer program optimization and constrained learning.
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).