Document Open Access Logo

Feedback & Synthesis in LLM-Assisted Termination Proofs

Authors Zeke Medley, Panagiotis Manolios

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.22.pdf
  • Filesize: 1.39 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
  • Theory of computation → Program reasoning
  • Computing methodologies → Artificial intelligence
Keywords
  • termination analysis
  • theorem proving
  • large language models
  • ACL2

Metrics

Abstract

Termination - proving there are no inputs on which a function runs forever - is one of the most fundamental problems in software verification, and competitions comparing termination analysis tools have run for over twenty years. We integrate two state-of-the-art, open-weight LLMs with a theorem prover’s built-in automation to generate termination proofs, solving 39% more problems than the best LLM alone and more than tripling the number solved by the built-in analysis on our benchmark. This is the first, to our knowledge, integration of an LLM with a termination-analysis algorithm, and is generalizable to any theorem prover based on a functional language. Our design is informed by nine ablations considering what theorem-prover feedback helps the LLM and four experiments on how the model decomposes problems.

Cite As Get BibTex

Zeke Medley and Panagiotis Manolios. Feedback & Synthesis in LLM-Assisted Termination Proofs. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.22

Author Details

Zeke Medley
  • Khoury College of Computer Sciences, Northeastern University, Boston, MA, USA
Panagiotis Manolios
  • Khoury College of Computer Sciences, Northeastern University, Boston, MA, USA

Supplementary Materials

References

  1. Tudor Achim, Alex Best, Kevin Der, Mathïs Fédérico, Sergei Gukov, Daniel Halpern-Leister, Kirsten Henningsgard, Yury Kudryashov, Alexander Meiburg, Martin Michelsen, Riley Patterson, Eric Rodriguez, Laura Scharff, Vikram Shanker, Vladmir Sicca, Hari Sowrirajan, Aidan Swope, Matyas Tamas, Vlad Tenev, Jonathan Thomm, Harold Williams, and Lawrence Wu. Aristotle: IMO-level Automated Theorem Proving, 2025. URL: https://doi.org/10.48550/arXiv.2510.01346.
  2. Agda Team. Sized Types. https://agda.readthedocs.io/en/latest/language/sized-types.html, 2025.
  3. Anthropic. Claude sonnet 4.5, 2025. Large language model. URL: https://www.anthropic.com/news/claude-sonnet-4-5.
  4. AxiomMathAI. Putnam, the world’s hardest college-level math test, ended yesterday … AxiomProver solved 9/12 problems in Lean autonomously, scoring at top of 4000 participants. Tweet, 2025. Posted on X (formerly Twitter), Dec 7, 2025. URL: https://x.com/axiommathai/status/1997767850279440715.
  5. Dirk Beyer. Competition on software verification (sv-comp). In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, pages 504-524. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28756-5_38.
  6. Robert S. Boyer and J Strother Moore. A Computational Logic. Academic Press, New York, 1979. Describes the NQTHM (Boyer-Moore) theorem prover. Google Scholar
  7. Sergiu Bursuc, Theodore Ehrenborg, Shaowei Lin, Lacramioara Astefanoaei, Ionel Emilian Chiosa, Jure Kukovec, Alok Singh, Oliver Butterley, Adem Bizid, Quinn Dougherty, Miranda Zhao, Max Tan, and Max Tegmark. A Benchmark for Vericoding: Formally Verified Program Synthesis, 2025. URL: https://doi.org/10.48550/arXiv.2509.22908.
  8. Harsh Raju Chamarthi, Peter C. Dillinger, Matt Kaufmann, and Panagiotis Manolios. Integrating Testing and Interactive Theorem Proving. In David S. Hardin and Julien Schmaltz, editors, Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, volume 70 of EPTCS, pages 4-19, 2011. URL: https://doi.org/10.4204/EPTCS.70.1.
  9. Harsh Raju Chamarthi and Panagiotis Manolios. Automated Specification Analysis Using an Interactive Theorem Prover. In W. A. Hunt Jr. and S. D. Johnson, editors, Proceedings of the 11th International Conference on Formal Methods in Computer‐Aided Design (FMCAD 2011), pages 92-99, Austin, TX, USA, 2011. Google Scholar
  10. Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, Cheng Ren, Jiawei Shen, Wenlei Shi, Tong Sun, He Sun, Jiahui Wang, Siran Wang, Zhihong Wang, Chenrui Wei, Shufa Wei, Yonghui Wu, Yuchen Wu, Yihang Xia, Huajian Xin, Fan Yang, Huaiyuan Ying, Hongyi Yuan, Zheng Yuan, Tianyang Zhan, Chi Zhang, Yue Zhang, Ge Zhang, Tianyun Zhao, Jianqiu Zhao, Yichi Zhou, and Thomas Hanwen Zhu. Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving, 2025. URL: https://doi.org/10.48550/arXiv.2507.23726.
  11. Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Terminator: Beyond Safety. In Computer Aided Verification (CAV 2006), volume 4144 of Lecture Notes in Computer Science, pages 415-418. Springer, 2006. URL: https://doi.org/10.1007/11817963_37.
  12. Thierry Coquand and Gérard Huet. The Calculus of Constructions. Information and Computation, 76(2-3):95-120, 1988. URL: https://doi.org/10.1016/0890-5401(88)90005-3.
  13. Marcos Cramer and Lucian McIntyre. Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK, 2025. URL: https://doi.org/10.48550/arXiv.2502.07728.
  14. Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language. In Automated Deduction - CADE 28, volume 12699 of Lecture Notes in Computer Science, pages 625-635. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  15. Peter C. Dillinger, Panagiotis Manolios, Daron Vroon, and J Strother Moore. ACL2s: "The ACL2 Sedan". In 29th International Conference on Software Engineering (ICSE 2007), Minneapolis, MN, USA, May 20-26, 2007, Companion Volume, pages 59-60. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/ICSECOMPANION.2007.14.
  16. Kefan Dong and Tengyu Ma. STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving. CoRR, abs/2502.00212, 2025. URL: https://doi.org/10.48550/arXiv.2502.00212.
  17. Jürgen Giesl, Carsten Aschermann, Marc Brockschmidt, Fabian Emmes, Falko Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephan Swiderski, and René Thiemann. Analyzing Program Termination and Complexity Automatically with AProVE. Journal of Automated Reasoning, 58(1):3-31, 2017. URL: https://doi.org/10.1007/s10817-016-9388-y.
  18. Anthony Hall. Seven myths of formal methods. IEEE Software, 7(5):11-19, 1990. URL: https://doi.org/10.1109/52.57819.
  19. Horace He and Thinking Machines Lab. Defeating Nondeterminism in LLM Inference. Thinking Machines Lab: Connectionism, 2025. URL: https://doi.org/10.64434/tml.20250910.
  20. Lei Huang, Weijiang Yu, Weitao Ma, Weihong Zhong, Zhangyin Feng, Haotian Wang, Qianglong Chen, Weihua Peng, Xiaocheng Feng, Bing Qin, and Ting Liu. A Survey on Hallucination in Large Language Models: Principles, Taxonomy, Challenges, and Open Questions. ACM Trans. Inf. Syst., 43(2):42:1-42:55, 2025. URL: https://doi.org/10.1145/3703155.
  21. Adharsh Kamath, Nausheen Mohammed, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K. Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, and Rahul Sharma. Leveraging llms for program verification. In Nina Narodytska and Philipp Rümmer, editors, Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024, pages 107-118. TU Wien Academic Press, 2024. URL: https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_16.
  22. Matt Kaufmann, Panagiotis Manolios, and J Strother Moore, editors. Computer-Aided Reasoning: ACL2 Case Studies. Springer, 2000. URL: https://doi.org/10.1007/978-1-4757-3188-0.
  23. Angelo Kyrilov and David C. Noelle. Using Automated Theorem Provers to Teach Knowledge Representation in First-Order Logic. CoRR, abs/1507.03670, 2015. URL: https://arxiv.org/abs/1507.03670.
  24. Lean Prover Community. Recursive Definitions (Lean 4 Reference Manual). https://lean-lang.org/doc/reference/4.19.0/Definitions/Recursive-Definitions/, 2025.
  25. Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving. CoRR, abs/2502.07640, 2025. URL: https://doi.org/10.48550/arXiv.2502.07640.
  26. Nils Lommen, Fabian Meyer, and Jürgen Giesl. Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops. In Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, editors, Automated Reasoning (IJCAR 2022), volume 13385 of Lecture Notes in Computer Science, pages 734-754. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-10769-6_43.
  27. Panagiotis Manolios. Reasoning About Programs. Course notes, Computer-Aided Reasoning, Northeastern University, 2026. URL: https://www.ccs.neu.edu/home/pete/courses/Computer-Aided-Reasoning/2026-Spring/ReasoningAboutPrograms.pdf.
  28. Panagiotis Manolios and Daron Vroon. Termination Analysis with Calling Context Graphs. In Thomas Ball and Robert B. Jones, editors, Computer Aided Verification (CAV 2006), volume 4144 of Lecture Notes in Computer Science, pages 401-414. Springer, 2006. URL: https://doi.org/10.1007/11817963_36.
  29. Panagiotis Manolios and Daron Vroon. Interactive Termination Proofs Using Termination Cores. In Matt Kaufmann and Lawrence C. Paulson, editors, Interactive Theorem Proving (ITP), volume 6172 of Lecture Notes in Computer Science, pages 355-370. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14052-5_25.
  30. Claude Marché and Hans Zantema. The Termination Competition. In Franz Baader, editor, Term Rewriting and Applications (RTA 2007), volume 4533 of Lecture Notes in Computer Science, pages 303-313. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73449-9_23.
  31. Zeke Medley and Panagiotis Manolios. 0xekez/fslatp. Software, (visited on 2026-07-14). URL: https://github.com/0xekez/fslatp
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.27134
  32. Iman Mirzadeh, Keivan Alizadeh, Hooman Shahrokhi, Oncel Tuzel, Samy Bengio, and Mehrdad Farajtabar. GSM-Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Models. Apple Machine Learning Research (paper page), 2024. URL: https://machinelearning.apple.com/research/gsm-symbolic.
  33. Iman Mirzadeh, Keivan Alizadeh, Hooman Shahrokhi, Oncel Tuzel, Samy Bengio, and Mehrdad Farajtabar. GSM-Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Models. arXiv preprint, 2024. URL: https://doi.org/10.48550/arXiv.2410.05229.
  34. OpenAI. Gpt-5, 2025. Large language model. URL: https://openai.com/gpt-5.
  35. OpenAI. gpt-oss-120b & gpt-oss-20b Model Card, 2025. URL: https://doi.org/10.48550/arXiv.2508.10925.
  36. Christine Paulin-Mohring. Inductive Definitions in the System Coq: Rules and Properties. In Typed Lambda Calculi and Applications (TLCA 1993), volume 664 of Lecture Notes in Computer Science, pages 328-345. Springer, 1993. URL: https://doi.org/10.1007/BFb0037116.
  37. Stanislas Polu and Ilya Sutskever. Generative Language Modeling for Automated Theorem Proving. CoRR, abs/2009.03393, 2020. URL: https://arxiv.org/abs/2009.03393.
  38. Jianxing Qin, Alexander Du, Danfeng Zhang, Matthew Lentz, and Danyang Zhuo. Can Large Language Models Verify System Software? A Case Study Using FSCQ as a Benchmark. In Proceedings of the Workshop on Hot Topics in Operating Systems (HotOS '25), pages 34-41, New York, NY, USA, 2025. ACM. URL: https://doi.org/10.1145/3713082.3730382.
  39. Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition. CoRR, abs/2504.21801, 2025. URL: https://doi.org/10.48550/arXiv.2504.21801.
  40. The Rocq Development Team. The Rocq Prover Reference Manual, 2024. URL: https://rocq-prover.org/refman.
  41. Aleksandr Shefer, Igor Engel, Stanislav Alekseev, Daniil Berezun, Ekaterina Verbitskaia, and Anton Podkopaev. Can LLMs Enable Verification in Mainstream Programming?, 2025. URL: https://doi.org/10.48550/arXiv.2503.14183.
  42. Oren Sultan, Jordi Armengol-Estapé, Pascal Kesseli, Julien Vanegue, Dafna Shahaf, Yossi Adi, and Peter O'Hearn. Llms versus the halting problem: Revisiting program termination prediction. arXiv preprint v3, 2026. URL: https://doi.org/10.48550/arXiv.2601.18987.
  43. FAIR CodeGen Team, Jade Copet, Quentin Carbonneaux, Gal Cohen, Jonas Gehring, Jacob Kahn, Jannik Kossen, Felix Kreuk, Emily McMilin, Michel Meyer, Yuxiang Wei, David Zhang, Kunhao Zheng, Jordi Armengol-Estapé, Pedram Bashiri, Maximilian Beck, Pierre Chambon, Abhishek Charnalia, Chris Cummins, Juliette Decugis, Zacharias V. Fisches, François Fleuret, Fabian Gloeckle, Alex Gu, Michael Hassid, Daniel Haziza, Badr Youbi Idrissi, Christian Keller, Rahul Kindi, Hugh Leather, Gallil Maimon, Aram Markosyan, Francisco Massa, Pierre-Emmanuel Mazaré, Vegard Mella, Naila Murray, Keyur Muzumdar, Peter O'Hearn, Matteo Pagliardini, Dmitrii Pedchenko, Tal Remez, Volker Seeker, Marco Selvi, Oren Sultan, Sida Wang, Luca Wehrstedt, Ori Yoran, Lingming Zhang, Taco Cohen, Yossi Adi, and Gabriel Synnaeve. Cwm: An open-weights llm for research on code generation with world models. arXiv preprint, 2025. URL: https://doi.org/10.48550/arXiv.2510.02387.
  44. Termination Competition. Termination competition 2025: Trs standard. https://termcomp.github.io/Y2025/TRS_Standard.html, 2025. Accessed: 2026-05-21.
  45. Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. An In-Context Learning Agent for Formal Theorem-Proving, 2023. URL: https://doi.org/10.48550/arXiv.2310.04353.
  46. Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Longhui Yu, Léo Dreyfus-Schmidt, Lewis Tunstall, Luigi Pagani, Moreira Machado, Pauline Bourigault, Ran Wang, Stanislas Polu, Thibaut Barroyer, Wen-Ding Li, Yazhe Niu, Yann Fleureau, Yangyang Hu, Zhouliang Yu, Zihan Wang, Zhilin Yang, Zhengying Liu, and Jia Li. Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning, 2025. URL: https://doi.org/10.48550/arXiv.2504.11354.
  47. Wolfgang Windsteiger. Automated Theorem Proving in the Classroom. In Predrag Janicic and Zoltán Kovács, editors, Proceedings of the 13th International Conference on Automated Deduction in Geometry, ADG 2021, Hagenberg, Austria/virtual, September 15-17, 2021, volume 352 of EPTCS, pages 54-63, 2021. URL: https://doi.org/10.4204/EPTCS.352.6.
  48. Huajian Xin, Daya Guo, Zhihong Shao, Z. Z. Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data, 2024. URL: https://doi.org/10.48550/arXiv.2405.14333.
  49. Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Haowei Zhang, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, and Chong Ruan. DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search. In The Thirteenth International Conference on Learning Representations, ICLR 2025, Singapore, April 24-28, 2025. OpenReview.net, 2025. URL: https://openreview.net/forum?id=I4YAIwrsXa.
  50. A. Yang et al. Qwen3: Large Language Models with Hybrid Thinking and Non-Thinking Modes. arXiv preprint, 2025. URL: https://arxiv.org/abs/2505.09388.
  51. Zhe Ye, Zhengxu Yan, Jingxuan He, Timothe Kasriel, Kaiyu Yang, and Dawn Song. VERINA: Benchmarking Verifiable Code Generation. arXiv preprint, 2025. https://arxiv.org/abs/2505.23135, URL: https://doi.org/10.48550/arXiv.2505.23135.
  52. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics. arXiv preprint, 2021. URL: https://arxiv.org/abs/2109.00110.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact