近日，ICSE'26组委会公布了在该会议上获得ACM SIGSOFT杰出论文奖的名单，Sergey Mechtaev团队发表在ICSE'26的论文《HoarePrompt: Structural Reasoning About Program Correctness in Natural Language》获ACM SIGSOFT杰出论文奖。ACM SIGSOFT杰出论文奖是由ACM SIGSOFT设立的论文奖项，用于奖励软件工程顶级会议上不超过10%的最优秀论文。

论文的第一作者为北京大学 2025 级博士生 Dimitris Bouras（导师：Sergey Mechtaev），通讯作者为北京大学Sergey Mechtaev助理教授。

论文研究大型语言模型是否能够判断一个程序是否符合自然语言规范。作者发现，直接让 LLM 判断程序正确性通常效果较差，因为模型难以准确推理程序语义。HoarePrompt 通过对推理过程进行结构化来解决这一问题：它在程序执行过程中传播对可达程序状态的自然语言描述，从而构建类似 Hoare 逻辑的非形式化推理轨迹，用以总结程序行为。随后，将这些带有状态注释的程序输入给 LLM，以判断实现是否满足规范。实验表明，这种结构化推理方式显著提升了程序正确性分类的能力，并表明基于自然语言的状态推理可以成为连接非形式化规范与程序分析之间的一种有效桥梁。