TY - GEN
T1 - Automated Postcondition Generation System
T2 - 22nd International Conference on Intelligent Computing, ICIC 2026
AU - Li, Luofeng
AU - Huang, Yanhong
AU - Shi, Jianqi
AU - Yang, Yang
N1 - Publisher Copyright:
© The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2027.
PY - 2027
Y1 - 2027
N2 - 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.
AB - 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.
KW - Formal Verification
KW - Large Language Models
KW - Model Fine-tuning
KW - Postcondition Generation
KW - Software Reliability
UR - https://www.scopus.com/pages/publications/105046924262
U2 - 10.1007/978-981-92-3435-6_41
DO - 10.1007/978-981-92-3435-6_41
M3 - 会议稿件
AN - SCOPUS:105046924262
SN - 9789819234349
T3 - Lecture Notes in Computer Science
SP - 489
EP - 501
BT - Advanced Intelligent Computing Technology and Applications - 22nd International Conference on Intelligent Computing, ICIC 2026, Proceedings
A2 - Huang, De-Shuang
A2 - Zhang, Chuanlei
A2 - Chen, Wei
A2 - Pan, Yijie
A2 - Premaratne, Prashan
PB - Springer Science and Business Media Deutschland GmbH
Y2 - 22 July 2026 through 26 July 2026
ER -