本站讯（通讯员 赵洪科）6月13日，由国际机器学习领域顶级会议ICML联合多家企业和高校举办的ICML2024自动化数学推理竞赛（ICML 2024 Challenges on Automated Math Reasoning）圆满落幕。由经管学部赵洪科副教授指导的2021级信息管理与信息系统本科生王慜懋作为第一队员获得自动化定理生成与证明赛道全球亚军，该成果由天津大学经管学部与认知智能全国重点实验室师生共同完成。

ICML（International Conference on Machine Learning）是全球机器学习、人工智能领域最享有盛誉、公认排名第一的学术会议，被中国计算机学会（CCF）推荐为A类会议。本次ICML2024自动化数学推理竞赛，旨在探索并推动人工智能技术在多种数学推理任务上的应用。本次竞赛集结了谷歌、华为、牛津大学、剑桥大学、卡耐基梅隆大学、北京大学及加州大学洛杉矶分校等众多顶尖企业与高等学府联合举办，共同探讨AI技术在各类数学推理和问题求解任务中的前景与挑战。

数学推理是人类智能中最具挑战性和最具深度的部分。人类在数学推理的发展进程中总结出了各种形式化语言，得以严格地描述数学问题和证明过程。而近年来的机器学习算法和大规模语言模型正在逐步接近甚至超越人类在一些数学推理的表现。那么，下一步本团队该如何发展AI数学推理，使之成为人类突破未知数学领域的最强辅助？本次挑战的任务即为通过给定一组公理及符号，模型需要正确生成新的定理，以简化证明路径。

在这个挑战中，本团队使用了自动定理生成（ATG）数据集，该数据集基于开源定理证明库“set.mm”开发，包含约38000个以Metamath形式语言编写的人类定理。该数据集主要关注多达2000个命题定理，通过给定一组公理和符号，需要推理出新的可证明定理。在评估过程中，本团队使用“set.mm”中的随机问题样本来衡量生成定理的实用性。

方案设计

图1 总体流程图

图2 Prompt 模板图

在本次挑战中，本团队使用了GPT-3.5作为推理模型。由于该任务没有明确的标签，因此无法在本地直接测试模型效果。为此，团队首先仔细设计Prompt，比较不同模版的Prompt，在云端运行后，得到效果最好的Prompt。在Prompt中输入随机抽取的15个定理(经灵敏度分析检验)作为推理定理集合，以尽可能提高模型输出的规范性。接下来，本团队在云端多次运行模型，根据云端结果，得到一些效果优异的新定理，将其加入新定理集合中。随后，在本地构建一个定理推导图，每一个节点表示一个定理，并计算每个节点的度中心性并进行排序，将度最高的几个定理加入到高重复性定理集合中。之后，本团队在云端再次运行模型，将这些高重复性的定理输入Prompt，以增强推理效果。通过并行处理的方法，在短时间内生成大量定理，并设置定理验证模块，以提高模型生成定理的通过率。

本次大赛吸引了来自全球顶尖高校和科技公司的184支队伍参与，显示了全球研究社区对于AI在数学领域应用的高度关注和积极参与。该成绩是天津大学管理与经济学部作为第一参赛单位在AI领域顶级学术会议赛事上取得的最好成绩。近年来，天津大学管理与经济学部大力支持人工智能方向科学研究和人才培养。该成绩的取得得益于学部在AI领域人才培养等方面打造的坚实基础。

参赛队伍介绍

选手介绍

王慜懋，2021级信息管理与信息系统专业在读本科生，天津大学三好学生，曾获全球校园人工智能算法精英大赛一等奖、清华IE亮剑全国工业工程应用案例大赛一等奖、美国大学生数学建模大赛M奖等。研究兴趣为图神经网络和大语言模型（LLMs），一篇关于图神经网络和大语言模型的研究论文已被CCF-BigData会议录用。

指导教师介绍

赵洪科，经管学部信息管理与管理科学系副教授；研究方向为机器学习、算法管理，在计算机、信息管理等领域的高水平学术期刊（如JOC, TKDE, TEVC, TOIS, TKDD, TWEB, TIST, TSMC, TETCI, TBD, Omega, IMM, PR, JMSE, 软件学报, 管理科学学报，管理工程学报）和顶级国际学术会议（如SIGKDD, AAAI, IJCAI, WWW, SIGIR, ACL, CIKM, WSDM, ICDM）上发表论文90余篇。

（编辑 赵晖 安桐瑶）