11月8日，2026 CCF中国软件大会第二届定理证明竞赛人与AI协作赛道决赛在天津举行。中国科学院数学与系统科学研究院数学机械化实验室三名成员取得佳绩：沈皓（博士三年级，导师支丽红）使用团队开发的程序验证智能体MechPV：Mechanized Program Verification ，以50分钟率先完成全部8道题目，位列赛道第一，获得一等奖；曹一川（博士四年级，导师高小山）、郭达凯（博士后）获得三等奖。

    本届决赛限时三小时，题目涵盖数组算法、哈希表、RSA编解码和字符串匹配等，要求参赛者提交能够通过形式化工具检查的程序证明。

    郭达凯负责开发的程序验证智能体MechPV将大语言模型与QCP程序验证工具、Coq/Rocq证明助手结合，通过多智能体分层协作，完成算法分析、循环不变式设计、辅助引理证明及程序验证。系统协调各模块的定义与接口，根据编译和验证反馈持续修正标注与证明，最终通过完整机器核验，确保各项推理共同支持程序的正确性要求。

    在验证难度较高的字符串匹配题中，沈皓借助MechPV，约19分钟完成源于musl C标准库的Two-Way字符串匹配函数验证，通过全部171项验证义务，覆盖算法正确性、指针运算和内存安全等要求。

    此次成绩展示了MechMath团队在人工智能辅助证明与程序验证方面的研究能力，也为多智能体协作解决复杂软件验证问题、提升软件可信性提供了实践案例。

相关链接

• 赛事官方报道：https://www.qua.codes/news/ai-verification-final.html

• QCP 官方网站：https://www.qua.codes/