[2604.03758] AutoReSpec: A Framework for Generating Specification using Large Language Models

Computer Science > Software Engineering arXiv:2604.03758 (cs) [Submitted on 4 Apr 2026] Title:AutoReSpec: A Framework for Generating Specification using Large Language Models Authors:Ragib Shahariar Ayon, Shibbir Ahmed View a PDF of the paper titled AutoReSpec: A Framework for Generating Specification using Large Language Models, by Ragib Shahariar Ayon and 1 other authors View PDF HTML (experimental) Abstract:Formal specification generation has recently drawn attention in software engineering as a way to improve program correctness without requiring manual annotations. Large Language Models (LLMs) have shown promise in this area, but early results reveal several limitations. Generated specifications often fail verification due to syntax errors, logical inaccuracies, or incomplete reasoning, especially in programs with loops or branching logic. Techniques like SpecGen and FormalBench attempt to address this through prompting and benchmarking, but they typically rely on static prompts and do not offer mechanisms for recovering from failure or adapting to different program structures. In this paper, we present AutoReSpec, a collaborative framework that combines open and closed-source LLMs for verifiable specification generation. AutoReSpec dynamically chooses an LLM pair and prompt configuration based on the structure of the input program. If the primary LLM fails to produce a valid output, a collaborative model is invoked, using validator feedback to refine and correct the ...