直播预告 | DeepSeek 开发者辛华剑分享活动

注意：本文部分文案由DeepSeek生成

国产大模型领域“顶流” DeepSeek -Prover 系列模型的核心开发者 辛华剑 空降 UCL创新创业中心 ！

主题分享：大语言模型时代的形式化数学革命

DeepSeek研讨会活动预览

国产技术标杆 DeepSeek 近期热度飙升，你是否也对国产大模型的神秘力量充满好奇？作为大模型领域的“顶流”，本次活动我们共同探讨DeepSeek Prover 系列模型的开发 。 未来人类数学家、推理型语言模型和形式化证明助手之间的跨界协作可能会对数学研究方式产生革命性影响。在本次分享中， 辛华剑 将结合自己在开发 DeepSeek Prover 过程中的实践经验，详细探讨这一前沿图景的最新进展、未来趋势以及依然面临的挑战。

经过半个多世纪的发展，计算机已经在现代数学中扮演重要的角色。尽管传统上其主要功能集中在数值计算和仿真模拟等辅助任务上，但近来的研究期望其在数学研究中扮演更为核心、通用的角色。大语言模型已经在处理较高层次的数学问题中展现出不俗的能力，一部分数学家已开始认可它们在日常科研中提供灵感和评判猜想的价值；但同时也有批评指出，语言模型偶尔出现的“幻觉”现象可能使其难以承担严谨、可信的数学证明工作。

与之相对， Lean prover 等计算机证明助手，则代表了一种符号主义的传统：通过以软件工程的严密方法形式化地编码数学体系，能够对人类数学知识进行系统检查和分析。形式化数学愿景强调使用证明助手形式化地表示人类数学知识、验证复杂定理证明，被认为是数学可持续发展的必要手段。

去年， DeepSeek Prover 和 AlphaProof 等项目利用神经网络生成可以被证明助手验证的代码，在数学竞赛中取得了显著进展，这进一步表明证明助手提供的精确监督信号对于训练人工智能模型以完成复杂数学推理任务具有重要作用。

这些多方面的进展预示着，未来人类数学家、推理型语言模型和形式化证明助手之间的跨界协作可能会对数学研究方式产生革命性影响。 在本次分享中 ， 辛华剑 将结合自己在开发 DeepSeek Prover 过程中的实践经验，详细探讨这一前沿图景的最新进展、未来趋势以及依然面临的挑战。

01

辛华剑

爱丁堡大学人工智能博士，中山大学逻辑学，DeepSeek研发成员，主导开发DeepSeek-Prover系列模型，专注于大语言模型在数学定理证明中的创新应用。

02

UCL Digital Sociology讲师

研究重点是AI and Digital Intimacy和AI and Creativity，分析人工智能与数字技术如何重塑创造性表达。目前在SSCI&AHCI Q1&Q2等核心期刊发表超过15+篇研究成果，同时有两部专著签约密歇根大学出版社和阿姆斯特大学出版社