CCF 中国软件大会 2026（ChinaSoft 2026）于 11 月 6 日至 8 日在天津举行，由中国计算机学会（CCF）主办。 定理证明竞赛是大会竞赛活动之一，为定理证明与程序验证领域的学生、从业者和爱好者提供交流与实践的机会。
2026 年 11 月 8 日 9:00—12:00，第二届定理证明竞赛人与 AI 协作赛道（LLM/AI 辅助证明赛道）线下决赛在天津社会山国际会议中心酒店举行，设置了 8 道 C 程序验证题目。
本届竞赛设置人工证明与 LLM/AI 辅助证明两个赛道。其中，今年新增的 AI 辅助赛道采用线上初赛与线下决赛相结合的形式，两场初赛分别于 9 月 20 日、10 月 10 日举行，旨在通过比赛促进定理证明的学习、教学与研究，探索人与大模型协作完成程序验证。
本场比赛采用个人参赛形式，允许选手使用 AI 辅助解题，通过 QCP 或 CStar 提交验证结果，并要求如实说明 AI 的使用情况。选手可以先阅读全部题面，但同时最多打开两道题，下载相应的程序代码、形式化定义和相关材料；成功解答或永久放弃其中一道题后，才能打开新的题目。
决赛首先按通过题目数量排名；通过题数相同时，再比较最后一次成功提交距开赛的分钟数，加上初赛排名的一半。初赛排名取两次初赛中较好的一次，未参加初赛或排名低于第 30 名的，按第 30 名折算。
决赛成绩与获奖名单
本场决赛共有 19 名选手取得有效成绩，其中 8 名选手通过全部 8 道题目。
沈皓（tsuki）以 50 分钟的决赛用时率先完成全部题目。计入初赛折算时间后，其最终计时为 52 分钟，位列榜首。陶四能（taosn12）以 79 分钟完成全部题目，最终计时为 85.5 分钟。两位选手均使用 QCP，获得本次比赛一等奖。
程章（mongo）、王瑞涵（pinecone）、蒋欣桐（pineapple）、赵毅龙（firepunch）、陆华毅（green）和曹一川（caoyichuan）也完成了全部题目。其中，赵毅龙使用 CStar，其余五位选手使用 QCP。
综合最终成绩，本次比赛评出 一等奖 2 名、二等奖 4 名、三等奖 7 名。
| 奖项 | 姓名 | 选手 ID | 通过题数 | 使用工具 |
|---|---|---|---|---|
| 一等奖 | 沈皓 | tsuki | 8 | QCP |
| 一等奖 | 陶四能 | taosn12 | 8 | QCP |
| 二等奖 | 程章 | mongo | 8 | QCP |
| 二等奖 | 王瑞涵 | pinecone | 8 | QCP |
| 二等奖 | 蒋欣桐 | pineapple | 8 | QCP |
| 二等奖 | 赵毅龙 | firepunch | 8 | CStar |
| 三等奖 | 陆华毅 | green | 8 | QCP |
| 三等奖 | 曹一川 | caoyichuan | 8 | QCP |
| 三等奖 | 张书豪 | studyingfather | 7 | CStar |
| 三等奖 | 叶永舜 | shreckye | 6 | QCP |
| 三等奖 | 郭思远 | gsy | 6 | CStar |
| 三等奖 | 郭达凯 | guodk | 6 | QCP |
| 三等奖 | 江忻然 | jiangxinran | 6 | QCP |
祝贺各位获奖选手！
决赛题目与验证任务
决赛题目涵盖了多种算法与数据结构。本场决赛的 8 道题包括最长合法括号子序列、汉堡的最大制作数量、批量区间操作后的数组、合法花序的区间计数、给定位数和数位和的最小与最大数，以及 RSA 编解码、哈希表实现的最长连续序列和 Two-Way 字符串匹配。前五道题涉及贪心、二分查找、差分数组、动态规划与前缀和等方法，要求选手证明给定程序确实满足题目规定的结果。
RSA 题基于 mini-gmp 的大整数接口实现密钥生成与编解码，题目允许模数最多为 4096 位。程序根据两个不同的奇素数生成公钥和私钥，编码与解码中的模幂运算均采用蒙哥马利模乘。选手需要证明：在规定的输入条件下，消息经过编码和解码后能够恢复原值，同时保持输入对象不变。这一要求也包括消息为零或为素数因子倍数的情形。
题目提供 mini-gmp 基础操作与分配函数的外部规约；选手需要为密钥生成、编解码和蒙哥马利辅助函数补充内部规约，并完成循环不变式、数学引理与证明标注，将数论性质与大整数对象的内存操作联系起来。
最长连续序列题采用哈希表记录数组中出现过的整数，去除重复值，再从每段连续序列的起点逐一查找后继，计算最长段的长度。本题只提供最外层的最终规格，哈希表专用谓词和内部函数规约需要选手自行补充，考察从数据结构实现到整体算法性质的验证能力。
Two-Way 字符串匹配取材于 musl libc 的内部 twoway_strstr 函数。比赛提供的适配版核心函数有 141 行非空 C 代码（不计注释和规格），包含最大后缀计算、周期判断、位移表和增量探测文本末端等处理。算法将模式串分为两部分，先比较右半段，再比较左半段，并利用周期信息和末字节筛选跳过不可能匹配的位置。
选手需要证明这些跳转不会遗漏最早的匹配：函数返回模式串在文本中第一次完整出现的位置，或者在不存在匹配时返回空指针，并保持输入字符串不变。验证还涉及数组访问、指针与整数运算的安全性；题目提供 memcmp 和 memchr 的外部规约，验证范围为内部匹配函数。
这些题目要求选手理解程序与待证性质，补充能够由验证工具检查的证明。AI 可以参与生成标注和证明，选手则需要判断生成内容是否符合题目要求，并根据验证反馈继续修改。
QCP 与 CStar 工具简介
QCP（Qualified C Programming）是一款面向 C 程序的形式化验证工具。用户为程序添加函数前后置条件、循环不变式等规约与标注，QCP 通过符号执行和分离逻辑推理生成验证条件，并支持在 Rocq 或 Lean 中完成相应证明，用于检查程序的安全性与功能正确性。
CStar（C*）是一种面向 C 程序验证、融合开发与证明的系统编程语言。它允许用户在同一份源码中编写程序、规约和证明，并以 C 风格的语法组织证明步骤，将程序实现与正确性证明结合起来。
两个工具均提供在线评测平台，供选手提交并检查验证结果。读者可以通过 QCP 决赛赛事页面和 CStar 决赛赛事页面了解比赛内容，也欢迎使用两个平台学习和实践程序验证。
本届人与 AI 协作赛道的两场线上初赛与线下决赛至此结束。感谢所有参赛选手的参与，感谢竞赛主办单位浙江望安科技有限公司，以及承办单位 TPChina 定理证明开放社区、浙江大学、上海交通大学的组织与支持，也感谢赛事组织与评审委员会、命题人员和平台维护人员的工作。