Automated Postcondition Generation System: A Linguistic-Logical Hybrid Retrieval and Refinement Approach with Fine-Tuned LLMs

Mapping natural language (NL) docstrings to formal program specifications is essential for software reliability, yet general-purpose LLMs often suffer from logical hallucinations. This paper proposes a methodological framework for automated postcondition generation centering on domain-specific fine-tuning of open-source LLMs. By fine-tuning Qwen2.5-7B-Instruct on a high-quality dataset of 17,007 Python docstring-postcondition pairs, our approach enables models to capture intricate linguistic-logical mappings. We enhance accuracy through a hybrid similarity retrieval mechanism, combining semantic and structural context, and a dual-path feedback loop integrating static symbolic analysis (Z3) with dynamic execution. Experimental results on EvalPlus show that our fine-tuned model achieves a 38.01% Bug-Complete (BC) rate, which further improves to 45.16% under the full framework, surpassing GPT-4. The methodology’s generalizability is validated on Java (HumanEval-X) and real-world bugs (Defects4J). Our work demonstrates that methodologically reinforced open-source models provide a technically viable, privacy-preserving paradigm for automated formal specification generation.