让大模型像人一样反复推敲，自动生成更准确的程序后置条件。
SpecMind: Cognitively Inspired, Interactive Multi-Turn Framework for Postcondition Inference
- 用多轮互动反馈机制，让大模型逐步修正生成的断言。
- 在多个数据集上准确率提升12%以上，且完整度显著更高。
- 适合需要高可靠性的软件验证与自动化测试场景。
规范对保证程序正确性至关重要，但手动编写规范仍具挑战且耗时。近年来基于大语言模型（LLM）的方法在生成规范（如后置条件）方面取得进展，但现有单次提示方法常产生不准确结果。本文提出SpecMind，一种新型后置条件生成框架，将大模型视为交互式、探索性推理者而非一次性生成器。SpecMind采用反馈驱动的多轮提示策略，使模型通过隐式和显式正确性反馈迭代优化候选后置条件，并自主决定停止时机。该过程促进更深层次的代码理解，提升生成结果与真实程序行为的一致性。实证评估表明，SpecMind在生成后置条件的准确性和完整性方面显著优于现有最先进方法。
原文摘要 · Abstract (English)
Specifications are vital for ensuring program correctness, yet writing them manually remains challenging and time-intensive. Recent large language model (LLM)-based methods have shown successes in generating specifications such as postconditions, but existing single-pass prompting often yields inaccurate results. In this paper, we present SpecMind, a novel framework for postcondition generation that treats LLMs as interactive and exploratory reasoners rather than one-shot generators. SpecMind employs feedback-driven multi-turn prompting approaches, enabling the model to iteratively refine candidate postconditions by incorporating implicit and explicit correctness feedback, while autonomously deciding when to stop. This process fosters deeper code comprehension and improves alignment with true program behavior via exploratory attempts. Our empirical evaluation shows that SpecMind significantly outperforms state-of-the-art approaches in both accuracy and completeness of generated postconditions.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。