Synthesis and Verification of Transformer Programs (Technical Report)

TL;DR

This paper introduces new algorithms for verifying and learning C-RASP programs, a language capturing transformer concepts, leveraging model checkers and local search, with applications in transformer optimization and constrained learning.

Contribution

It develops verification techniques connecting C-RASP to Lustre dataflow programs and introduces a local search algorithm for learning C-RASP from examples.

Findings

Effective verification of C-RASP using SMT-solvers.

Successful learning of C-RASP programs from examples.

Application to transformer optimization and constrained learning.

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