DROPS

Artifact

Software

0xekez/fslatp

Authors: Zeke Medley and Panagiotis Manolios

Abstract

Cite as

Zeke Medley, Panagiotis Manolios. 0xekez/fslatp (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-27134,
   title = {{0xekez/fslatp}}, 
   author = {Medley, Zeke and Manolios, Panagiotis},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:26cbefe528532dda47d04b7198cca383281e5a72;origin=https://github.com/0xekez/fslatp;visit=swh:1:snp:c0586566dcf43c2bf58ba92e5b738480c1db6b0b;anchor=swh:1:rev:98d85b5d1e46d2428b51d5e3799812e2a07387e6}{\texttt{swh:1:dir:26cbefe528532dda47d04b7198cca383281e5a72}} (visited on 2026-07-16)},
   url = {https://github.com/0xekez/fslatp},
   doi = {10.4230/artifacts.27134},
}

Document

DOI: 10.4230/LIPIcs.ITP.2026.22

Feedback & Synthesis in LLM-Assisted Termination Proofs

Authors: Zeke Medley and Panagiotis Manolios

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{medley_et_al:LIPIcs.ITP.2026.22,
  author =	{Medley, Zeke and Manolios, Panagiotis},
  title =	{{Feedback \& Synthesis in LLM-Assisted Termination Proofs}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{22:1--22:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.22},
  URN =		{urn:nbn:de:0030-drops-269965},
  doi =		{10.4230/LIPIcs.ITP.2026.22},
  annote =	{Keywords: termination analysis, theorem proving, large language models, ACL2}
}

Search Results

Documents authored by Manolios, Panagiotis

0xekez/fslatp

Abstract

Cite as

Feedback & Synthesis in LLM-Assisted Termination Proofs

Abstract

Cite as

Thanks for your feedback!

Could not send message