# AutoReSpec: A Framework for Generating Specification using Large Language Models

arXiv: https://arxiv.org/abs/2604.03758 · HTML: https://mlsanity.com/paper/2604.03758/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 10 of its 36 references that are in the map.
- First posted on arXiv 4 Apr 2026.

## Builds on (most cited first, 10 of 10)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Training language models to follow instructions with human feedback](https://mlsanity.com/paper/2203.02155/) (2022)
- [Large Language Models for Software Engineering: A Systematic Literature Review](https://mlsanity.com/paper/2308.10620/) (2023)
- [Few-shot training LLMs for project-specific code-summarization](https://mlsanity.com/paper/2207.04237/) (2022)
- [Keep the Conversation Going: Fixing 162 out of 337 bugs for 0.42 each using ChatGPT](https://mlsanity.com/paper/2304.00385/) (2023)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [Ranking LLM-Generated Loop Invariants for Program Verification](https://mlsanity.com/paper/2310.09342/) (2023)
- [Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference](https://mlsanity.com/paper/2503.04779/) (2025)
- [EvoSpex: An Evolutionary Algorithm for Learning Postconditions](https://mlsanity.com/paper/2102.13569/) (2021)
- [What's Decidable About Program Verification Modulo Axioms?](https://mlsanity.com/paper/1910.10889/) (2019)

## Built on by (most cited first, 3 of 3)

- [Reversa: A Reverse Documentation Engineering Framework for Converting Legacy Software into Operational Specifications for AI Agents](https://mlsanity.com/paper/2605.18684/) (2026)
- [Faithful Autoformalization of Natural Language Assertions](https://mlsanity.com/paper/2607.13303/) (2026)
- [From Helpful to Trustworthy: LLM Agents for Pair Programming](https://mlsanity.com/paper/2604.10300/) (2026)

## Abstract (arXiv)

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 specification. This two-stage design enables both speed and robustness. We evaluate AutoReSpec on a new benchmark of 72 real-world and synthetic Java programs. Our results show that it achieves 67 passes out of 72, outperforming SpecGen and FormalBench in both Success Probability and Completeness. Our experimental evaluation achieves a 58.2% success probability and a 69.2% completeness score, while cutting evaluation time by 26.89% on average compared to prior methods. Together, these results demonstrate that AutoReSpec offers a scalable, efficient, and reliable approach to LLM-based formal specification generation.