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

翻译：C-RASP是一种简单编程语言，近期被证明能够捕获Transformer可表达的概念。本文开发了用于自动验证C-RASP程序的新型算法技术。为此，我们建立了C-RASP与Lustre语言中同步数据流程序验证之间的关联，从而能够利用采用高度优化的SMT求解器的最先进模型检测工具。我们的第二项贡献则聚焦于C-RASP程序的初始学习问题：我们提出了一种基于局部搜索的从示例中学习C-RASP的新算法。我们通过文献中C-RASP基准测试验证了所实现算法的有效性，特别在以下两类应用中：（1）Transformer程序优化，以及（2）基于部分规范的Transformer程序约束学习。