至顶科技

2025-06-16 10:09:10

当我们在解数学题时，通常是先读懂题目，然后一步步推理证明。但对于人工智能来说，这个看似简单的过程却充满挑战。想象一下，如果你只会看懂正式的数学符号，却完全不理解人类的自然语言，那么当老师用中文或英文出一道几何题时，你就完全束手无策了。这正是目前大多数AI数学证明系统面临的困境——它们虽然能在严格的数学符号世界里游刃有余，却无法直接处理我们日常使用的自然语言数学问题。

这个问题困扰了研究人员很久，直到华为诺亚方舟实验室、华为Celia团队和香港中文大学的联合研究团队带来了突破性进展。他们在2025年6月8日发表的这项研究名为"Mathesis: Towards Formal Theorem Proving from Natural Languages"（Mathesis：走向从自然语言出发的形式化定理证明），完整论文可通过arXiv:2506.07047v1获取。研究团队包括华为Celia团队的俞学军、翟鹏义等人，华为诺亚方舟实验室的钟建元、冯子锦、刘浩雄等研究者，以及香港中文大学的徐强教授，由李振国和沈鑫担任通讯作者。

这项研究首次实现了从自然语言数学问题到严格数学证明的端到端自动化处理。就像为AI配备了一位既精通人类语言又擅长数学推理的翻译兼数学家。研究团队不仅开发了名为Mathesis的完整解决方案，还创建了一个包含488道中国高考数学题的标准测试集，为这个领域建立了重要的评估基准。

更令人兴奋的是，这套系统已经被实际应用到华为Celia智能助手中，帮助解决真实的高考数学问题。当面对复杂的数学推理时，系统能够将非正式的推理与严格的形式化证明相结合，准确率从原来的65.3%提升到了84.2%。这意味着AI不仅能理解我们的数学问题，还能给出既严谨又可验证的证明过程。

一、从语言理解到数学翻译：Mathesis-Autoformalizer的突破

想象你是一位精通中英文的数学老师，学生用中文向你提出一个几何问题，你需要将这个问题精确地翻译成严格的数学符号语言，不能丢失任何条件，也不能添加多余的假设。这正是Mathesis-Autoformalizer所要完成的任务——将自然语言表达的数学问题准确转换为计算机能够处理的形式化数学语言。

传统的自动形式化方法就像一个只会按照固定模板工作的翻译软件，遇到复杂或新颖的表达方式就容易出错。而Mathesis-Autoformalizer采用了一种全新的强化学习方法，就像培养一个真正的数学翻译专家，让它在实践中不断学习和改进。

这个系统的核心创新在于建立了一套双重检验机制。首先是语法检验，确保翻译出的数学表达式在形式上是正确的，就像检查一个句子是否符合语法规则。然后是语义检验，确保翻译后的内容与原问题的数学含义完全一致，就像确认翻译是否准确传达了原文的意思。

研究团队设计了一个巧妙的奖励系统来训练这个翻译专家。当系统成功将一个自然语言问题转换为语法正确且语义准确的形式化表达时，就会获得正面反馈。反之，如果翻译出现错误或偏差，系统就会收到负面信号并调整策略。这种方法让AI能够从每次翻译尝试中学习，逐渐提高准确性。

为了进一步优化性能，研究团队还引入了层次化偏好优化技术。这就像为翻译专家配备了一位资深导师，不仅关注单次翻译的质量，还考虑翻译结果是否有利于后续的数学证明过程。通过这种方式，系统学会了生成既准确又实用的形式化表达。

在数据准备方面，研究团队采用了智能的主题建模技术来筛选训练材料。他们使用BERTopic算法将大量数学问题按照主题进行分类，然后有针对性地选择那些能够提