SpecMind: Cognitively Inspired, Interactive Multi-Turn Framework for Postcondition Inference

📄 arXiv: 2602.20610v1 📥 PDF

作者: Cuong Chi Le, Minh V. T Pham, Tung Vu Duy, Cuong Duc Van, Huy N. Phan, Hoang N. Phan, Tien N. Nguyen

分类: cs.SE, cs.CL

发布日期: 2026-02-24

💡 一句话要点

SpecMind：认知驱动的交互式多轮后置条件推断框架

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 后置条件推断 大型语言模型 交互式学习 程序规范 反馈驱动

📋 核心要点

  1. 现有基于LLM的后置条件生成方法依赖单次提示，准确性不足，难以充分理解代码行为。
  2. SpecMind采用反馈驱动的多轮交互式提示，迭代优化候选后置条件，提升代码理解和对齐。
  3. 实验结果表明，SpecMind在后置条件的准确性和完整性上显著优于现有技术水平。

📝 摘要（中文）

程序规范对于确保程序正确性至关重要，但手动编写规范仍然具有挑战性且耗时。最近基于大型语言模型（LLM）的方法在生成后置条件等规范方面取得了成功，但现有的单次提示方法通常会产生不准确的结果。本文提出了SpecMind，一种新颖的后置条件生成框架，它将LLM视为交互式和探索性的推理器，而不是一次性生成器。SpecMind采用反馈驱动的多轮提示方法，使模型能够通过结合隐式和显式的正确性反馈来迭代地改进候选后置条件，同时自主决定何时停止。这个过程通过探索性尝试，促进了对代码的更深入理解，并提高了与真实程序行为的对齐。我们的实证评估表明，SpecMind在生成的后置条件的准确性和完整性方面都显著优于最先进的方法。

🔬 方法详解

问题定义：论文旨在解决程序后置条件自动推断的问题。现有方法，特别是基于大型语言模型的单次生成方法，往往无法准确捕捉程序行为，导致生成的后置条件不准确或不完整。手动编写后置条件耗时且容易出错。

核心思路：SpecMind的核心思路是将大型语言模型从一次性生成器转变为交互式推理器。通过多轮对话和反馈机制，让模型能够逐步探索和完善后置条件，模拟人类专家逐步理解和验证程序行为的过程。这种交互式探索能够帮助模型更深入地理解代码，并生成更准确的后置条件。

技术框架：SpecMind框架包含以下主要阶段：1) 初始后置条件生成：使用LLM生成初始候选后置条件。2) 正确性反馈：通过隐式或显式的方式提供关于候选后置条件的正确性反馈。隐式反馈可能来自执行测试用例，显式反馈可能来自人工或自动验证。3) 后置条件改进：根据反馈，LLM迭代改进候选后置条件。4) 停止决策：模型自主决定何时停止迭代，并输出最终的后置条件。这个过程循环进行，直到满足停止条件。

关键创新：SpecMind的关键创新在于其反馈驱动的多轮交互式框架。与传统的单次生成方法相比，SpecMind能够利用反馈信息逐步完善后置条件，从而提高准确性和完整性。此外，模型自主决定停止迭代，避免了不必要的计算开销。

关键设计：SpecMind的具体实现细节包括：1) 使用特定的提示工程技术来引导LLM生成和改进后置条件。2) 设计有效的反馈机制，例如使用测试用例执行结果作为隐式反馈，或使用形式化验证工具作为显式反馈。3) 训练或微调LLM，使其能够更好地理解代码和生成后置条件。4) 设计停止迭代的标准，例如当后置条件在一定数量的迭代后没有显著改进时停止。

📊 实验亮点

SpecMind在实验中显著优于现有方法。具体而言，SpecMind在后置条件的准确性和完整性方面都取得了显著提升。相较于最先进的方法，SpecMind在准确率上提升了X%，在完整性上提升了Y%（具体数据未知）。实验结果表明，SpecMind的交互式框架能够有效地提高后置条件生成的质量。

🎯 应用场景

SpecMind可应用于软件开发、测试和验证等领域。它可以帮助开发人员自动生成程序规范，提高代码质量和可靠性。在测试阶段，SpecMind生成的后置条件可以用于自动生成测试用例，提高测试覆盖率。在形式化验证中，SpecMind可以辅助生成验证所需的规范，降低验证成本。未来，该技术可扩展到更复杂的程序和规范生成任务。

📄 摘要（原文）

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.