对话DeepSeek研发团队前成员辛华剑：如何用大模型把数学家从细节中解放出来｜甲子光年

大语言模型时代的形式化数学。

原标题：对话DeepSeek研发团队前成员辛华剑：如何用大模型把数学家从细节中解放出来｜甲子光年
文章来源：甲子光年
内容字数：18388字

大语言模型时代的形式化数学：辛华剑演讲要点

本文总结了辛华剑在UKTI.HUB发表的演讲《大语言模型时代的形式化数学》的核心内容，探讨了形式化数学的历史、挑战、以及大语言模型(LLM)在该领域的应用和未来展望。

1. 形式化数学的历史与当代挑战

   形式化数学旨在用精确的符号语言表达数学陈述和证明，其历史可追溯至莱布尼茨的“普遍语法”和希尔伯特的计划。然而，当代数学面临着工程化挑战：证明篇幅过长、知识管理困难、验证成本高昂等。例如，开普勒猜想的证明长达300页，验证耗时12年。陶哲轩认为，形式化数学结合AI，可使数学研究更高效、协作和规模化，未来甚至可一次性证明数百或数千条定理。

2. 形式化数学作为解决方案

   形式化数学提供了一种解决方案，通过使用Coq、Lean、Isabelle和Mizar等形式化系统，将数学问题转化为计算机可验证的形式。借助证明助手软件(如Isabelle和HOL Light)，可以保证证明的正确性，并有效管理庞大的数学理论体系，例如陶哲轩的Lean blueprints项目。

3. 大语言模型在形式化数学中的应用

   近年来，LLM在解决科学问题和算法竞赛上的能力显著提升，例如OpenAI的模型和DeepMind的AlphaProof。DeepSeek-Prover系列模型，尤其V1.5版本，在形式化定理证明基准上表现突出，并展示了模型“先思考再作答”的能力。其训练方法包括大规模自动形式化方法来合成证明数据，进行迭代训练。 未来，LLM有望在提出数学猜想、发现数学抽象、构建完整的数学知识库等方面取得突破。

4. LLM在形式化数学中的挑战与局限

   当前LLM在形式化数学应用中仍面临挑战，例如数据稀缺、自然语言与形式语言的翻译难题、形式系统的复杂性等。 需要进一步提升模型的Agent能力，使其能够在大规模代码库上有效工作。

5. LLM对数学研究及其他领域的影响

   LLM的应用将对数学研究、工业规模验证、数学教育以及一般应用产生深远影响。它有望帮助数学家快速验证猜想，加速形式化验证的普及，保存和传承数学知识，并促进数学工具在更广泛领域的应用。

6. 问答环节要点

   问答环节涵盖了DeepSeek的创新之处、算力利用率的提升、MCTS在模型训练中的作用、LLM的幻觉问题、AI对科研工作的潜在影响等方面，辛华剑提供了深入的见解和分析。

总而言之，辛华剑的演讲强调了形式化数学的重要性及其与LLM结合的巨大潜力。虽然挑战依然存在，但随着技术的进步，LLM有望推动数学研究和相关领域的性发展。

联系作者

文章来源：甲子光年
作者微信：
作者简介：甲子光年是一家科技智库，包含智库、社群、企业服务版块，立足中国科技创新前沿阵地，动态跟踪头部科技企业发展和传统产业技术升级案例，推动人工智能、大数据、物联网、云计算、新能源、新材料、信息安全、大健康等科技创新在产业中的应用与落地。