近日，我院系统可信性自动验证国家地方联合工程实验室徐扬教授团队在一阶逻辑自动定理证明器领域取得突破性进展。所研发的一阶逻辑自动定理证明器CSI_V，采用该团队原创的逆向并行逻辑演绎的科学方案，融合此前国际领先的证明器Vampire，针对该领域最顶级赛事——国际自动定理证明竞赛（International Conference on Automated Deduction —— Automated Theorem Proving System Competition）近五年共2500个竞赛问题，在标准实验条件下进行了对比实验，共证明出2446个定理，超过此前国际领先的证明器Vampire 180个定理（详见下表。事实上，每多证明1个定理都是极其困难的！），遥遥领先于此前国际领先的证明器Vampire，居国际领先！国际自动定理证明器竞赛的主席、美国迈阿密大学Geoff Sutcliffe教授对徐扬教授团队最新研发的证明器给予了极高的评价。
基于逻辑的自动定理证明器是人工智能领域最基础、最核心、最科学的研究方向之一，涉及数学、逻辑学、计算机科学与技术等领域。基于逻辑的自动定理证明器属基础性工具，具有十分重要的科学与应用价值，广泛应用于自然科学、技术科学、社会科学等领域，特别是数学定理的证明与发现。基于逻辑的自动定理证明器研发同时也是一个极其困难的问题，需要让计算机从浩如烟海的条件中找到成功的证明路径，经常被比喻为“大海捞针”。
徐扬教授团队在基于逻辑的自动定理证明相关领域研究40多年，原创地提出了基于矛盾体分离的多元、协同、动态自动演绎推理理论与系列方法，从本质上突破了现有的一阶逻辑自动定理证明器普遍采用的二元、静态推理方法，不仅是基于逻辑自动定理证明器领域的一个重大突破，还从本质上发展了所有以分离规则（Modus Ponens）为演绎推理的逻辑系统。基于该理论、方法已经研发了一系列一阶逻辑自动定理证明器，用这些自动定理证明器已证明26万多个来自于国际标准问题库 TPTP 及 Mizar 的一阶逻辑表示的定理。这些定理涉及数学分析、代数学、拓扑学、范畴论、组合数学、几何学、数论、逻辑学、规划、计算理论、管理科学、程序验证、集成电路验证、协议验证等方面。该一阶逻辑自动定理证明器主要研发成员包括徐扬、曾国艳、吴贯锋、Jun Liu (英国Ulster大学)、陈树伟、刘沛瑶、曹锋、徐鹏、李志辉、何星星等系统可信性自动验证国家地方联合工程实验室的多名教师和研究生。
实验结果对比表：
自动定理证明器 | 2020年 (500) | 2021年 (500) | 2022年 (500) | 2023年 (500) | 2024年 (500) | 五年合计 (2500) |
Vampire 4.9 | 457 | 455 | 453 | 450 | 451 | 2266 |
CSI_V 1.1 | 487 | 485 | 492 | 491 | 491 | 2446 |
