摘要
规范对确保程序正确性至关重要，但手动编写耗时且困难。现有基于大语言模型（LLM）的单次提示方法往往生成结果不准确。本文提出 SpecMind 框架，将 LLM 视为交互式探索推理者而非一次性生成器。该框架采用反馈驱动的多轮提示策略，使模型能结合隐式和显式正确性反馈迭代优化候选后置条件，并自主决定停止时机。此过程促进了对代码的深度理解，显著提升了生成后置条件的准确性和完整性，优于最先进方法。
AI 推荐理由
论文核心在于利用多轮交互和反馈驱动机制，提升 LLM 在代码后置条件推断中的深度推理能力。
研究机构
德克萨斯大学达拉斯分校
FPT软件AI中心
VinUniversity
南洋理工大学
论文信息