近日，由国际机器学习领域顶级会议ICML联合多家企业和高校举办的ICML 2024自动化数学推理竞赛圆满落幕，认知智能全国重点实验室队伍cogbase在赛道1-1（自动形式化，Auto-formalization）和赛道1-2（自动非形式化，Auto-informalization）获得两项冠军；在赛道3（代码自动求解优化问题，Automated Optimization Problem-Solving with Code）获得亚军。指导教师为实验室黄振亚副教授、刘淇教授、王士进副主任、陈恩红副主任。

自动化数学推理竞赛：聚焦数学问题形式化、新定理生成及问题求解

ICML（International Conference on Machine Learning）是全球机器学习、人工智能领域最重要的学术会议之一，被中国计算机学会（CCF）推荐为A类会议。ICML 2024自动化数学推理竞赛，集结了谷歌、华为、牛津大学、剑桥大学、卡耐基梅隆大学、北京大学及加州大学洛杉矶分校等众多顶尖企业与高等学府联合举办，吸引了全球184支队伍参与，旨在探索并推动人工智能技术在多种数学推理任务上的应用。本次竞赛设有三个主要赛道：

• 赛道1-1（自动形式化，Auto-formalization）和赛道1-2（自动非形式化，Auto-informalization）
• 赛道2（自动化定理生成与证明，Automated Theorem Generation & Proving）
• 赛道3（代码自动求解优化问题，Automated Optimization Problem-Solving with Code）

其中，赛道1-1和1-2集中于自动形式化及其逆向过程，即如何将自然语言描述的数学证明转化为形式化语言LEAN3，并进行逆向操作，赛道3则着重于优化问题的自动化建模与解决。

以上赛道不仅涉及将自然语言中的数学问题与严格的形式语言相互转化，还包括探索基于公理集的新定理生成，以及理解并求解优化问题。

大模型与经验、工具库相结合 破解数学推理自动化难题

• 赛道1-1：

在本赛道中，实验室团队提出了一套自动形式化方案，利用GPT4大语言模型和多层次的经验总结与检索机制，实现了数学问题从自然语言到形式化语言的高效转换。

具体来说，团队首先构建了一个经验代理（Experience Agent），通过运行大语言模型（LLM），比较生成内容与标准答案，总结出任务的通用方法、成功经验、常见错误等。这些经验能够为模型提供显式的的任务先验知识和方向并减少重复的错误。其次，团队使用检索模型BGE-M3，从训练集中筛选出与测试问题最相似的问题，作为示例提供给模型进行上下文学习。通过动态调整示例，模型能够根据具体问题进行类比推理，生成更准确的形式化代码。然后，团队将经验列表、检索到的示例和预设的提示模板组合起来，输入到LLM中，生成多种形式化证明代码。通过多次采样和后处理，获得一组LEAN3代码。为了评估生成代码的质量，团队构建了一个批判代理（Critic Agent），从代码和语义两个角度对其进行检查。批判代理不仅验证代码的语法正确性，还确保代码逻辑上解决了原问题。通过多角度评估，团队能够选出最佳的形式化代码。

这种多层次的策略不仅提升了生成LEAN3代码的准确性和稳定性，还展示了大语言模型在复杂数学问题自动形式化上的巨大潜力。自动形式化及其逆向过程是开发有效形式数学推理系统的核心构建模块，对自动定理证明和数学推理验证具有重要作用。通过自动实现正式语言和非正式语言之间的转换，可以显著提高数学问题处理的效率和准确性，助力验证复杂数学推理的正确性。

• 赛道1-2：

本赛道的任务是自动非形式化。与赛道1-1不同，赛道1-2需要将形式化的数学陈述和证明转换为自然语言的陈述和证明。为了实现这一目标，实验室团队沿用了赛道1-1的框架，但在生成模型的输入上做了调整。对于每个输入，团队首先进行知识解析，提取出其中的关键信息，包括难度等级、涉及的知识点、以及问题的主题场景（例如人名、地名等）。基于这些元素，生成自然语言问题和解决方案，这是弥合形式与非形式之间差距的关键步骤。

其他步骤与赛道1-1类似：团队将经验列表、检索到的示例、解析出的知识和预设的提示模板组合起来，输入到LLM中，生成多种自然语言的陈述和证明。批判代理随后从数学证明和语义角度对生成内容进行检查，确保其准确性和一致性。最终，团队通过多角度评估，选出最佳的自然语言陈述和证明。

• 赛道3：

在本赛道中，本团队主要通过程序推理（Program of Thought, PoT）的策略，利用GPT4大语言模型首先生成能正确求解优化问题的Python代码，然后借助多种数学工具库进行自动求解。在使用大模型生成代码的过程中，实验室团队设计了下图所示的一种动态prompt构造方法，通过聚类的方式筛选出训练集中的相似题，作为prompt中的示例，为模型的正确推理提供了可靠的启发；随后，本团队还引入了一种大模型自我修正策略，通过将代码求解的结果代入原问题，验证答案的正确性，对验证不正确的结果重新求解；此外，本团队对大模型多次采样的结果进行自一致性投票，从而提高答案求解的准确率和稳定性。

针对赛事多条赛道，实验室团队提出的解决方案探索了大模型在各类数学推理任务上的潜力，为未来在形式化语言理解与生成、定理证明、复杂问题求解等研究领域提供了新思路。

本次比赛实验室团队所采用的技术可以与教育实践深度结合。一方面，理解和生成复杂的数学定理公式、求解数学问题的自动化，不仅能在具体的教学场景中帮助提高学生的学习效率，而且能深化学生对数学概念、数学推理过程的理解和应用能力；另一方面，本次比赛的方法具有很高的可解释性，例如通过生成易懂的自然语言描述来表示形式化语言、生成具体的定理证明路径、以及生成求解优化问题的代码，这些求解方式的引入为实现自适应和个性化教学提供可能。

大语言模型革新未来教育教学

当前，随着大语言模型技术的不断深化发展，智能教育正处于可能引发长期乃至革命性变革的关键时刻，大语言模型与教育相结合的应用是这一变革的前沿阵地之一。

在“大模型+教育”的新赛道上，讯飞星火正全速进发，当前中英作文批改准确率已经超过一般老师的水平，口语教学已支持CET、雅思、托福等多类口语学习和模考，科普教学、答疑辅学助力学生科普问题解答率及学习完成率分别超过95%和90%。

展望未来，我们期待上述研究成果与星火大模型深度融合，并能在更广阔的教育场景中得到应用。这不仅将在数学教学与学习中发挥关键作用，还能跨学科支持语言学习、科学探索和技能训练等多个方面，助力打造更为高效、个性化、智能化的学习环境，给予教育教学更加蓬勃的生命力，进一步推动教育行业新质生产力的革新与发展。