Search papers, labs, and topics across Lattice.
This paper introduces techniques for verifying and synthesizing C-RASP programs, a simplified language capturing transformer expressivity. They establish a connection between C-RASP verification and synchronous dataflow program verification in Lustre, enabling the use of SMT-based model checkers. Furthermore, they present a local search algorithm for learning C-RASP programs from examples, demonstrating its effectiveness in transformer program optimization and constrained learning.
Unlock formal verification for transformer-level programs by translating them into synchronous dataflow languages, enabling rigorous analysis and optimization.
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).
