用Transformer识别代码是否终止，提升程序分析可靠性。
Transformers for Program Termination
- 设计小型Transformer集成框架，应对非终止样本稀缺问题。
- 集成模型性能超越单个Transformer及主流大模型和图方法。
- 提供语法感知的解释，帮助理解判断依据，适合安全验证场景。
判断程序是否终止是程序分析中的核心挑战，直接影响正确性、验证与安全性。本文研究Transformer架构能否直接从源码中识别终止模式，并通过集成方式增强其能力。为应对非终止样本极度稀缺的问题，设计了由紧凑Transformer编码器组成的集成框架，采用多种抗不平衡损失函数和类别感知采样技术进行系统训练。通过组合不同损失函数训练的模型，集成方法显著优于单一Transformer，性能超过多种现成的大语言模型和基于图的方法。最后，提出一种归因流程，生成语法感知的终止判断解释。
原文摘要 · Abstract (English)
Determining whether a program terminates is a core challenge in program analysis with direct implications for correctness, verification, and security. We investigate whether transformer architectures can recognise termination patterns directly from source code and how their strengths can be amplified through ensembles. To overcome the extreme scarcity of non-terminating examples, we design an ensemble framework of compact transformer encoders, systematically trained with a suite of imbalance-aware loss functions and class-aware sampling techniques. By combining models trained with distinct loss functions, our ensembles achieve substantially stronger performance than any single transformer, outperforming both powerful off-the-shelf LLMs and graph-based methods. Finally, we introduce an attribution pipeline that produces syntax-aware explanations for the termination estimation.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。