近日，在法国巴黎举办的第29届国际自动定理证明器竞赛 (The CADE ATP System Competition, CASC-J12)中，西南交通大学数学学院系统可信性自动验证国家地方联合工程实验室徐扬教授团队提交的一阶逻辑自动定理证明器获得ICU（I Challenge yoU）组亚军和FOF（First Order Formula）组季军的好成绩。该团队是自2018年中国团队首次参赛以来，唯一持续参加这个竞赛并每年都取得良好成绩的团队。
自动定理证明是人工智能领域既经典又前沿的研究方向之一，涉及数学、逻辑学、计算机科学等领域，广泛应用于自然科学、技术科学、社会科学等领域，特别是数学定理的证明与发现。自动定理证明器属基础性工具，具有重要的科学与应用价值。自动定理证明同时也是一个非常困难的问题，需要让计算机从浩如烟海的条件中找到成功的证明路径，经常被比喻为“大海捞针”。
国际自动定理证明竞赛是国际上自动演绎推理领域的最顶级赛事，自1996年以来每年举办一次，至今已举办了29届。本次赛事设有THF、TFA、TFN、FOF、UEQ、SLH和ICU组。其中西南交通大学参加的ICU组是本届竞赛新增的组别，其中的定理都是较难证明的定理，非常具有挑战性。学校参赛的证明器CSI_E在该组别中获得亚军，说明徐扬教授团队研发的证明器在证明困难定理方面具有独到的优势。而学校参加的另外一个FOF组有11个证明器参赛，是竞争最激烈的一组。参赛单位包括英国曼彻斯特大学、德国斯图加特DHBW大学、中国西南交通大学、美国爱荷华州大学、英国剑桥大学、德国格赖夫斯瓦尔德大学、爱沙尼亚塔林理工大学等。
徐扬教授团队在基于逻辑的自动演绎推理相关领域研究多年，原创地提出了基于矛盾体分离的多元、协同、动态自动演绎推理理论与方法，从本质上突破了现有的一阶逻辑自动定理证明器普遍采用的二元、静态推理方法，是自动演绎推理领域的一个重大突破。基于该理论、方法已经研发了一系列一阶逻辑自动定理证明器（这次参赛的自动定理证明器是其中之一）。用这些自动定理证明器已证明26万多个来自于国际标准问题库 TPTP 及 Mizar 的一阶逻辑表示的定理。这些定理涉及数学分析、代数学、拓扑学、范畴论、组合数学、几何学、数论、逻辑学、规划、计算理论、管理科学、程序验证、集成电路验证、协议验证等方面。学校参加2024年CASC-J12竞赛的团队主要成员包括徐扬、曾国艳、吴贯锋、Jun Liu (英国Ulster大学)、Stephan Schulz(德国斯图加特DHBW大学)、陈树伟、刘沛瑶、曹锋、何星星、徐鹏、李志辉等系统可信性自动验证国家地方联合工程实验室的多名教师和研究生。
下图为竞赛结果，其中CSI_E、CSE_E等为我校参赛的证明器。
