AutoReSpec: A Framework for Generating Specification using Large Language Models

arXiv:2604.03758v1 Announce Type: cross 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. Techniq