AI4Math · Invited Talk 01 · Junqi Liu

来源： Invited Talk 01 · Junqi Liu 播客： ICML 2026 · AI4Math 分类： AI 研究 原文发表： 2026-07-11 纪要生成： 2026-07-13

基本信息

• Workshop：3rd AI for Math Workshop — Toward Self-Evolving Scientific Agents
• 类型：Invited Talk（本届首场 invited talk）
• 题目：Numina Agent: From Single Model to Agent（从单一模型到 agent）
• 讲者：Junqi Liu（中科院数学与系统科学研究院 AMSS 博士生；领导 Numina 形式化团队；Kimina-Prover 系列核心贡献者）
• 真实时段：约 08:41–09:00（KST，7/11）

一句话概括

介绍 Numina Agent——首个构建在通用 coding agent 之上的形式化定理证明 agent：不再设计固定流水线，而是给通用编码 agent 配上 Lean 工具（Lindex、Info Prover、Discussion Partner），让它自主决定何时调用哪个工具，实现全自主形式化。Putnam 2025 上 12 题全解，是首个能对齐闭源 SOTA 的开源系统，并进一步做成对数学家友好的 Numina Fields 多 agent 工作台。

背景与动机

LLM 的演进与数学的角色

过去几年 LLM 从纯文本模型快速演进为具备强推理与 agentic 能力的系统：早期主要做文本补全、翻译等纯文本任务；随着能力增强，研究者开始问"它们能否真正推理、理解复杂概念"。数学是这些能力的关键试金石——解数学题不仅要理解语言，还要多步推理、保持逻辑一致。更近期，LLM 具备了 agentic 能力：不再只生成答案，而能用工具、写并调试代码、与外部环境交互以完成长程任务。整体上 LLM 从"文本生成器"变成"更强推理、理解、执行"的系统，而数学能力在此过程中至关重要。

非形式（informal）数学的进展与硬伤

聚焦自然语言数学推理：自 GPT-3.5 起进展迅速，起初只能做 GSM8K、MATH 等应用题，两年内在数学竞赛上大幅提升、接近 IMO 金牌水平；此后 OpenAI 宣称其模型解决了一个开放 80 年的猜想（被 Fields 奖得主团队高度评价）。但 informal 数学有一个关键硬伤：常只用最终答案评判——例如正确答案是 −10、模型也输出 −10 就算对。这方便且易扩展，但最终答案不能保证推理过程正确：生成的解常有缺步、逻辑错误，有时是"用错误推理蒙对答案"。对数学证明来说这很严重，因为每一步都必须正确。

形式系统的优势与代价

好的解法是用形式系统：给模型一个形式陈述、让它生成形式证明，Lean 等系统可自动检查每步是否正确。相较 informal，形式数学有两大优势：(1) 严格、自动的检查；(2) 系统能展示当前证明状态、告诉你还剩什么。代价：形式证明常远长于自然语言证明（每小步都要写清）；形式库仍缺很多高层定义，有些问题甚至难以在 Lean 中陈述。简言之，形式数学带来正确性，但把"证明"变成了更长更复杂的"编码任务"。

主要内容

已有两类范式及其局限

• Whole-proof generation（整证生成）：给模型一个形式定理，让它一次生成完整 Lean 证明再交 Lean 检查。问题有三：(1) 极受限——哪怕只有小错，Lean 也会拒绝整个证明；(2) 复杂证明常需许多中间引理和长推理链，模型难一次生成全部；(3) 未充分利用证明助手的交互特性——Lean 能在每步后给出当前目标和局部反馈，而整证生成只把 Lean 当最终检查器。
• Step prover（分步证明）：每次只产一个证明步/一个 tactic，可配 MCTS 等搜索探索不同证明路径，潜力很大——2024 年 Google DeepMind 用它达到 IMO 银牌水平。局限：(1) 通常只擅长证定理，而人类解难题时会试特例、探不同思路、引入有用引理，这些单步 prover 难做到；(2) 一道难题往往需极大搜索、与 Lean 大量交互，耗算力多；(3) 能力常局限于固定的 tactic 空间，难泛化到通用模型。也有系统用固定 workflow（先检索相关定理→拆问题→生成证明→修复证明）。领域脉络：GPT-f → DeepSeek-Prover → 后续 Kimina-Prover / Hilbert / Seed-Prover 等。

Numina Agent 的三点动机

1. 想从"专用模型"转向利用现有基座模型；
2. 现代 coding agent 已支持完整工作循环——能管理上下文、运行命令、持续修代码；
3. 这是通向大规模自动形式化的可扩展路径：基座模型进步，整个系统无需训练即变强；用基座模型还能大幅降低大规模形式化项目的成本。

Numina Agent 的设计

基于上述动机，推出 Numina Agent——首个建在 coding agent 之上的形式化定理证明 agent，有效复用编码 agent 自身强大的上下文管理与文件管理能力。做法：修改现有的 Lean LSP-MCP 项目，集成三个新工具——Lindex、Info Prover、Discussion Partner。有了 coding agent，就不再需要设计固定流水线：把所有认为有用的工具都提供给系统，让系统自主决定何时调用哪个工具，实现全自主形式化。

典型工作流示例：收到一个形式陈述后，agent 先用工具取得 goal → 检索与该 goal 潜在相关的定理 → 基于理解把数学问题发给 informal prover 得到非形式解 → 再形式化。Discussion Partner 工具在极难问题上尤其有用（如 Putnam 2025 的 A5、B6 题）。

结果与消融

• Putnam 2025 全解：用 Cloud Code（以 Claude Ops 4.5 为基座）测试，成功解出全部 12 题，是首个能与闭源 SOTA（如 X-Prover）对齐的开源系统。部分题的处理时间短于 Aristotle 与 Seed-Prover 1.5、以及 Axiom；在证明长度上，除了 Aristotle 这类天然有短证明优势的 prover 外，Numina Agent 在多数题上也优于 Seed 和 Axiom。
• 核心结论：通用 coding agent + 合适的形式化工具，已能处理相当复杂的数学证明任务。
• 消融研究：(1) 检索工具通常只影响证明生成的速度，不影响性能；(2) coding agent 的基座不仅需强数学与 Lean 技能，还需良好的 token 效率与指令遵循能力；(3) 在难题上，informal prover 与 Discussion Partner 更有用——帮主 agent 跳出局部编码错误、在更高层重新思考证明。
• 成本：若每步都用最强模型，大规模形式化难以落地。同一 harness 下，实验显示 DeepSeek 系达到接近 Claude Ops 4.7 的效果、成本仅约 1/8。这说明 agent 框架与基座模型可以分离。

人机协作与 Numina Fields

• 人机交互形式化案例：设计了人机交互模式来形式化一篇 2025 年 11 月发表的文章；与一位数学家和 Lean 专家协作，两周内完成该文形式化，生成 2.8 万+ 行 Lean 代码、引入 70+ 个新定义与引理。数学家与专家主要提供方向性指导。
• Numina Fields：为让这种人机协作真正好用而开发的工作台。背景：Meta 等团队已在用 agent 形式化数百页研究生教材或论文，但直接用命令行 + 多 agent 对数学家不友好，Fields 提供更友好的工作空间。两种主要模式：(1) 交互模式——用户与 agent 实时对话、看它在证什么、控制关键步；(2) 自动模式——系统把大任务拆给多个子 agent、长时间自动运行。Fields 还含：LaTeX blueprint、追踪进度的依赖图、原生 Lean Info view、供自然语言交互的 agent 聊天窗。多个 agent 可与人协作起草引理、写 Lean 代码、逐步改进证明直到编译通过；多 agent 也能并行处理形式化的不同部分。blueprint 以依赖图呈现，用户可实时看每个节点是否已形式化、已证明。为处理不同任务，Fields 用多专家 agent 团队：Blueprint drafter → Formalizer → Prover → Golfer（化简完成的证明，也可减少编译时间）。更详细的例子里，用户可在单一界面内完成几乎整个工作流：与 agent 交互、编辑 blueprint、查看依赖图、改 Lean 文件、检查 Lean 消息与证明状态，甚至直接推送到 GitHub。讲者认为 Fields 可成为大规模自动形式化专家的重要助手。演讲末尾提供了扫码获取代码资源。

关键结论 / Takeaways

• 通用 coding agent + Lean 工具 = 无需专用模型即可做复杂形式化证明，且随基座升级而自动增强。
• agent 框架与基座可解耦：换更便宜基座（如 DeepSeek）可拿到接近 SOTA 的性价比（约 1/8 成本达到接近 Claude Ops 效果）。
• Putnam 2025 12/12 全解，首个对齐闭源 SOTA 的开源系统；检索影响速度而非性能，难题靠 informal prover / Discussion Partner。
• Numina Fields 把大规模自动形式化包装成对数学家友好的多 agent 工作台（drafter/formalizer/prover/golfer）。

Q&A / 讨论亮点

转写中该场结束后主持人直接衔接下一场（Leonardo de Moura），未见独立提问环节。

名词 / 引用

• Lean LSP-MCP：被改造以集成新工具的底座项目。
• Lindex / Info Prover / Discussion Partner：Numina Agent 集成的三个 Lean 工具。
• Putnam 2025：评测集，Numina Agent 报告 12/12 全解。
• X-Prover / Aristotle / Seed-Prover 1.5 / Axiom：对比的闭源 SOTA 与其他 prover。
• Numina Fields：面向数学家的多 agent 形式化工作台（blueprint、依赖图、Lean Info view；drafter/formalizer/prover/golfer）。
• Cloud Code + Claude Ops 4.5 / DeepSeek：基座与成本对比（约 1/8 成本达接近效果）。

原文发表：2026-07-11  ·  纪要生成：2026-07-13