Transformers for Program Termination
Yoav Alon, Cristina David

TL;DR
This paper explores the use of transformer ensembles to recognize program termination patterns directly from source code, achieving superior performance and providing syntax-aware explanations.
Contribution
It introduces an ensemble framework of transformer encoders trained with imbalance-aware techniques, outperforming existing methods in termination prediction.
Findings
Ensemble models outperform single transformers and existing methods.
The framework effectively handles data imbalance with specialized loss functions.
The attribution pipeline offers syntax-aware explanations for termination decisions.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
