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程序约束学习。