提出自动验证与学习Transformer程序的新方法，提升可解释性与可靠性。
Synthesis and Verification of Transformer Programs (Technical Report)
- 通过关联Lustre数据流程序验证，利用SMT求解器实现高效自动验证。
- 在已有基准上成功验证多个C-RASP程序，验证效率显著提升。
- 适合关注AI可解释性、形式化验证的开发者与研究人员。
C-RASP是一种简洁的编程语言，已被证明能表达Transformer模型中的概念。本文提出新的算法技术，用于自动验证C-RASP程序。为此，我们建立了其与Lustre中同步数据流程序验证的联系，从而可利用最先进的模型检测器及高度优化的SMT求解器。第二项贡献是关于如何从示例中学习C-RASP程序。我们提出一种基于局部搜索的新算法来实现这一目标。我们在文献中的多个C-RASP基准上展示了实现的有效性，尤其在以下两个应用中表现突出：(1) Transformer程序优化，(2) 基于部分规范的约束式Transformer程序学习。
原文摘要 · Abstract (English)
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).
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。