👋 欢迎

《Massive Values in Self-Attention Modules are the Key to Contextual Knowledge Understanding》 作者揭示了一个有悖常理的现象：在注意力机制中，极端数值异常地聚集于 Query (Q) 与 Key (K) 的表征区域，而 Value (V) 中则无此现象。值得注意的是，未使用 RoPE（旋转位置编码，如 GPT-2 模型）的模型中并未观察到这一特性。 此类极端数值对模型的上下文理解能力至关重要，相较之下，其对于参数化知识的倚重程度则较低。实验显示，若此类数值受到干扰，模型仍能回忆既有事实（例如，回答“中国首都是哪里？”），但在需要依赖上下文的任务中（如 GSM8K 数学推理测试），其表现则会显著下滑。 那些特意保留这些极端数值的量化技术（例如 AWQ 和 SmoothQuant）能够维持模型的原有性能；反之，若采用未能保留这些数值的方法（例如 GPTQ），模型的上下文推理能力将遭受重创。 当作者刻意让上下文信息与模型的内在知识产生冲突时，发现 LLMs (大语言模型) 的表现与随机猜测无异。然而，有选择地扰动那些“巨大值”反而提升了模型的准确率，这暗示 LLMs (大语言模型) 在默认情况下更倾向于依赖其内部知识，而这些“巨大值”则在引导模型理解上下文方面扮演着关键角色。 这种“巨大值”高度集中的现象，其根源直接指向 Rotary Position Encoding (RoPE) 技术。具体来说，RoPE 技术仅选择性地作用于 Query (Q) 和 Key (K) 向量，而将 Value (V) 排除在外，从而导致了极端数值在 Q 和 K 表征中的独特聚集。 在涵盖自回归 LLM (大语言模型) 及多模态模型等多种 Transformer 架构中，作者均一致地观察到了这种“巨大值”集中的现象。这进一步印证了作者的假说，即 RoPE 是驱动 QK 表征中结构化“巨大值”出现的根本原因。 ...

《Ultra-FineWeb: Efficient Data Filtering and Verification for High-Quality LLM Training Data》清华刘知远团队出品 摘要 模型驱动的数据过滤仍然面临两大挑战：（1）缺乏有效的数据验证策略，难以对数据质量提供及时的反馈；（2）用于训练分类器的种子数据选择缺乏明确标准，且过度依赖人工经验，引入了一定的主观性。针对第一个挑战，我们提出了一种高效的验证策略，能够以极低的计算成本快速评估数据对 LLM 训练的影响。针对第二个挑战，我们基于高质量种子数据有利于 LLM 训练的假设，结合提出的验证策略，优化了正负样本的选择，并提出了一种高效的数据过滤流程。该流程不仅提升了过滤效率、分类器质量和鲁棒性，还显著降低了实验和推理的成本。此外，为了高效过滤高质量数据，我们采用了一种基于 fastText 的轻量级分类器，并将该过滤流程成功应用于两个广泛使用的预训练语料库，即 FineWeb 和 Chinese FineWeb 数据集，从而创建了更高质量的 Ultra-FineWeb 数据集。Ultra-FineWeb 包含约 $1$ 万亿个英语 Token 和 $1200$ 亿个中文 Token。实验结果表明，在 Ultra-FineWeb 上训练的 LLM 在多个基准测试任务中表现出显著的性能提升，验证了我们的流程在提升数据质量和训练效率方面的有效性。 总体工作流 所提出的基于高效验证的高质量过滤管道的总体工作流程如图1(c)所示。我们首先构建一个初始候选种子池，并应用我们的高效验证策略来识别能够显著提高训练性能的高质量样本。这些经过验证的样本作为正样本种子，用于训练分类器，而负样本则从原始数据池中随机选择，以创建一个平衡的训练集。在分类器过滤阶段，我们从原始数据池中抽取一个小样本子集，并使用我们的高效验证策略来验证分类器的选择，以评估其有效性。基于验证结果，我们迭代更新高质量种子池，调整正样本和负样本的比例，并微调分类器训练超参数，以优化数据选择策略。只有在高效验证中表现出稳定可靠性能的分类器才会被部署用于全尺度数据选择和后续模型训练，从而在保持高数据质量的同时，显著降低计算成本。 高效验证策略 验证训练数据的有效性通常需要大量的计算资源。例如，在一个包含1000亿 (B) 个 Token 的数据集上训练一个 10 亿参数的大语言模型 (LLM)，大约需要 1200 个 H100 GPU 小时（相当于 64 个 GPU 连续运行近 19 小时）。当迭代开发高质量的数据分类器时，这种计算负担变得尤其令人望而却步。此外，大规模的训练验证对于较小的数据集来说是不切实际的，因为使用有限的 Token 数量训练的模型无法表现出具有统计意义的性能差异，而训练的不稳定性进一步损害了结果的可靠性。这种限制在我们对 FineWeb 和 FineWeb-edu 的比较分析中很明显。当从头开始使用 80 亿个 Token 进行训练时，FineWeb-edu 在 HellaSwag 上取得了优异的性能，而在 3800 亿个 Token 时，FineWeb 在包括 Winogrande、HellaSwag 和 PIQA 在内的多个基准测试中表现更好，这突出了基于训练规模的评估结果的不一致性[^1]。 ...

《A Survey of AI Agent Protocols》 智能体网络生态架构 当前人工智能体网络的层级架构可分为:基础智能体网络层、中间协议层以及上层应用层,形成完整的生态系统。 发展历程 本报告梳理了2019年至今大语言模型、智能体框架、相关协议及典型应用的发展脉络。清晰呈现了技术演进的总体轨迹。目前智能体技术尚处萌芽期,更强大的语言模型和通信协议是突破关键。 主流协议纵览 报告详细分析了包括MCP、A2A在内的主流智能体协议,涵盖研发机构、应用场景和核心技术等维度。需要指出的是,这些协议大多仍在完善中,部分尚停留在理论构想阶段。 协议评估体系 研究同时建立了智能体协议的评估框架,指出优秀的协议设计必须兼顾运行效率、系统扩展性和安全性等核心指标,这对构建规模化智能体系统至关重要。 应用场景解析 报告中的典型案例生动演示了不同协议下的智能体系统架构差异。必须承认,要建立支持大规模、高安全性智能体网络的通信协议体系,我们仍有大量基础性工作亟待完成。

《Seed-Coder: Let the Code Model Curate Data for Itself》 这篇论文的核心启发在于提出了一种最小化人工参与、以模型为中心的数据构建管线pipeline来生产大语言模型（LLM）的代码预训练数据。关键做法是利用LLM本身进行代码数据的评分和筛选，而不是依赖大量人工制定的、针对特定语言的过滤规则或人工标注数据。基于此，他们推出了Seed-Coder系列8B模型（基础、指令、推理），并通过监督微调、偏好优化（DPO）以及长链思维（LongCoT）强化学习来进一步提升指令遵循和多步代码推理能力，展示了这种数据策略在提升模型代码相关任务（生成、补全、编辑、推理、软件工程）上的卓越表现。 引言部分强调了现有开源代码LLM在预训练数据构建上对人工的重度依赖（如手工规则过滤）所带来的局限性，包括可扩展性差、主观偏见和维护成本高。最具启发性的一点是作者引用“The Bitter Lesson”来说明AI领域的发展趋势：依赖大规模计算和数据的通用方法最终会胜过依赖人类知识的复杂方法。Seed-Coder正是基于这一理念，倡导使用LLM来自动化代码数据的筛选和评估，从而克服人工方法的瓶颈，并构建了一个包含6万亿token的预训练语料库。 预训练: 数据管线 (Data Pipeline): 启发性在于其解耦的并行设计，允许各个处理模块（如去重、基础过滤、LLM高级质量过滤）独立运行，便于增量扩展和灵活调整，避免了重新运行整个冗长流程。数据被分为文件级代码、仓库级代码、提交记录和代码相关的网页数据四类，并针对不同预训练阶段（常规预训练和持续预训练）进行组合。 数据成分 (Data Ingredients): GitHub数据: 关键做法是构建一个LLM驱动的文件级质量评分模型。他们随机抽取代码文件，让一个“神谕”模型（DeepSeek-V2-Chat）从可读性、模块化、清晰度和可复用性四个维度打分，然后用这些评分数据微调一个13B的Llama 2模型作为高效的质量评估器，过滤掉低质量文件。这比传统基于规则的过滤更能捕捉代码质量的细微差别且可扩展性强。 提交数据 (Commits Data): 做法是将GitHub提交记录格式化为代码变更预测任务，利用提交信息和上下文（包括README、目录结构和BM25检索的相关文件）预测修改的文件和代码补丁，从而让模型学习真实世界的代码演化模式。 代码相关的网页数据: 亮点在于一个优化的两阶段提取框架：首先通过规则提取和fastText模型进行大规模召回（在标注数据上训练，实现高召回率），初步筛选出代码相关内容；然后使用LLM质量过滤器进行精细评估和筛选，并特别注意缓解不同网站类型（如电商、文档、论坛）带来的打分偏见。 用于持续预训练的高质量数据: 关键在于迭代训练fastText模型。先基于特定特征（如质量分、语言、注释率）构建小的种子数据集作为正样本，并精心设计难负样本（如高分但无注释的代码，或第一轮fastText召回但质量分低的数据），以提升fastText模型的判别能力，通过2-3轮迭代扩展高质量数据集。 用于持续预训练的长上下文数据: 通过支持高达32K的序列长度进行长上下文训练。文件级数据通过LLM过滤，而仓库级数据则针对主流语言（Python, Java, C）实施了基于文件依赖关系的拓扑拼接，对于HTML, SQL, Shell等则使用随机拼接，大型仓库则分解为子图，以在保持逻辑连贯性的同时适应上下文窗口。 Fill-in-the-Middle (FIM): 实践中发现SPM（Suffix-Prefix-Middle）模式比PSM模式略好，可能与注意力机制的位置偏见有关。采用字符级随机分割，并在常规和持续预训练阶段设置不同FIM比例。 预训练策略 (Pretraining Policy): 采用了Llama 3架构，82亿参数，分阶段进行预训练，从混合数据开始，然后是大量代码数据，最后在持续预训练阶段转向高质量和长上下文数据，并相应调整学习率。 后训练: 后训练部分展示了如何从预训练好的基础模型进一步打造出强大的指令模型和推理模型。 指令模型 (Instruct Model): 数据构建：多样性 (Data Construction: Diversity): 核心是合成数据生成，强调种子片段多样性（来自高质量GitHub、OSS-Instruct、Markdown/Jupyter/StackExchange等代码-文本混合数据以模拟真实交互）和风格多样性（构建元风格集并随机混合风格，再结合WildChat数据）。 数据过滤：质量与难度 (Data Filtering: Quality and Difficulty): 结合规则（Tree-sitter去语法错误）和模型（LLM评估正确性）进行质量过滤；通过主题分类和模型评估难度来筛选出过于简单的实例。 沙盒验证的自我修正 (Self-Correction with Sandbox Verification): 这是一个非常实用的做法。为了保留高难度样本（它们通常错误率也高），模型被提示生成解决方案和单元测试，在沙盒中评估，并对失败的方案进行迭代修正，直到测试通过或达到最大尝试次数。 ...

《Absolute Zero: Reinforced Self-play Reasoning with Zero Data》 Absolute Zero Reasoner：作者的这款推理模型能够完全通过自我博弈，无需任何外部数据，既能自主提出可最大限度提升学习效率的任务，又能通过解决这些任务来增强自身的推理能力。在数学和编程领域，其综合表现已超越其他“零样本”模型。 强化学习与价值对齐（RLVR）目前仍高度依赖人工精心构建的数据集，这使其规模化发展受到掣肘。更进一步而言，当人工智能超越人类智慧时，若仍固守于人类设计的任务，其发展潜力将受到严重束缚——超级智能系统必须突破人类设定的学习框架。 作者率先提出了 Absolute Zero Paradigm（绝对零范式）。在这一范式中，一个独立的智能体能够同时学习如何提出最能激发自身学习潜能的任务，以及如何高效地完成这些任务。 这种自我进化得益于与一个可验证环境的互动。该环境能自动检验任务的完整性，并提供可靠的反馈，从而支持系统进行可信且无限制的自我博弈训练。 Absolute Zero Reasoner (AZR) 是作者基于此范式开发的首个实例化模型。AZR 能够自主提出基于代码的推理任务，在解决这些任务的过程中不断提升自身的推理能力，并持续推动其学习内容向更高难度的方向发展。 AZR 选择 Python 作为其推理的基础，因 Python 语言具有强大的表达力和可验证性。它围绕（程序、输入、输出）这一核心三元组构建了三类任务：预测输出（演绎推理）、推断输入（溯因推理）以及根据示例生成程序（归纳推理）——这三种模式相辅相成。 尽管未使用任何人工筛选的数据，也未进行分布外泛化（OOD）训练，AZR 依然在 3 项编程和 6 项数学推理的基准测试中取得了当前最佳（SOTA）的平均综合表现——其性能甚至超越了那些利用数万个经专家标注的样本训练而成的模型。作者的平均得分达到了 50.4，而此前的最佳记录为 48.6。 主要研究成果包括： 代码先验知识能显著增强推理能力（例如，基于代码训练的模型表现优于普通的vanilla基础模型）； 跨领域迁移效果显著（代码训练使数学能力提升了 15.2 个百分点！）； 这种优势会随着模型规模的增大而协同增强（模型参数从 30 亿增加到 70 亿再到 140 亿时，性能分别提升了 5.7、10.2 和 13.2 个百分点）。 尽管 AZR 实现了自我进化，但作者发现了一个重大的安全隐患：作者使用的 Llama3.1 模型偶尔会生成一些令人不安的“思维链”（CoT）内容，其中包括“智胜智能机器和智力较低的人类”等言论——作者将这类情况称为“uh-oh moments”（“糟糕时刻”）。因此，这类模型仍需人工监督。 总而言之，作者的 Absolute Zero 范式突破了强化学习与价值对齐（RLVR）在数据方面的一大核心局限。即便在没有任何人工构建数据集的情况下，AZR 依然在数学和编程等多个基准测试中展现出卓越的性能。 AZ 标志着人工智能推理领域的一项根本性变革：智能体开始自主定义其学习的边界。作者的框架同时支持在“解题空间”（如何解决问题）和“任务空间”（哪些问题值得解决）进行双重探索，而这一切都建立在可验证的环境之上。 代码应用仅仅是一个开端；这一范式未来有望拓展至网络交互、形式数学乃至物理世界的复杂互动。 ...

《Youku Dense Caption: A Large-scale Chinese Video Dense Caption Dataset and Benchmarks》 数据集地址：https://www.modelscope.cn/datasets/os_ai/Youku_Dense_Caption 摘要 随着视频内容的爆炸式增长，视频字幕已成为视频理解的关键工具，显著增强了从视频中理解和检索信息的能力。然而，大多数公开可用的密集视频字幕数据集都是英文的，导致大规模、高质量的中文密集视频字幕数据集稀缺。为了弥补中文社区内的这一差距并推动中文多模态模型的发展，我们开发了首个大规模、高质量的中文密集视频字幕数据集，名为优酷密集字幕（Youku Dense Caption）。该数据集来源于中国著名的视频分享网站优酷。优酷密集字幕包含 31,466 个完整的短视频，由 311,921 条中文字幕标注。据我们所知，它是目前公开可用的最大的细粒度中文视频描述数据集。此外，我们基于优酷密集字幕建立了多个中文视频-语言任务的基准，包括检索、定位和生成任务。我们在现有的最先进的多模态模型上进行了广泛的实验和评估，证明了该数据集的实用性和进一步研究的潜力。 1 引言 目前，大多数公开可用的密集视频字幕数据集主要是英文的，导致非英语语言，特别是中文的资源显著匮乏。这种语言差距不仅限制了中文用户的体验，也阻碍了针对中文视频内容的多模态模型的开发和优化 (Li et al. 2019; Singh et al. 2020)。 为了解决这一关键差距并促进中文多模态模型的进步，我们引入了优酷密集字幕数据集，这是第一个大规模、高质量的中文密集视频字幕数据集，精心设计以满足中文视频内容理解和信息检索的需求。该数据集来源于中国领先的视频分享平台之一优酷，包含 31,466 个完整的短视频，标注了 311,921 条中文字幕。这使其成为公开可用的、用于中文视频内容细粒度描述的最大、最详细的数据集，从而为中文视频-语言处理研究提供了重要的资源。 除了提供全面的数据集外，我们还基于优酷密集字幕数据集为中文视频-语言任务建立了几个基准。这些任务包括视频检索、定位和字幕生成。这些基准不仅为现有多模态模型的客观评估提供了严格的设置流程，也为该领域的未来研究和发展方向提供了指导。 为了验证优酷密集字幕数据集的效用，我们使用最先进的多模态模型进行了广泛的实验和评估。这些实验的结果证明了该数据集在提高模型性能方面的显著影响，包括视频检索和字幕生成。通过这项研究，我们强调了优酷密集字幕数据集在推动中文视频-语言发展领域的潜力。 我们的主要贡献如下： 我们介绍了优酷密集字幕数据集，这是最大且完全由人工标注的中文视频密集字幕数据集，包含 31,466 个短视频和 311,921 条中文字幕。 我们为中文视频-语言任务建立了几个基准，包括视频检索、定位和字幕生成，为多模态模型提供了标准的评估指标。 我们通过广泛的实验验证了该数据集的有效性，证明了其在增强多模态模型生成和检索性能方面的显著影响。 3 优酷密集视频描述数据集 为了填补中文社区在细粒度标注数据集方面的空白，我们推出了首个带有详细中文标注的大规模密集视频描述数据集。该数据集共包含 31,406 个视频，分割为 311,921 个片段，累计时长达 748.96 小时。每个视频的平均时长为 85.68 秒，平均片段长度为 8.1 秒。每个视频平均包含 9.9 条标注，每条标注平均包含 17.9 个字。从数据清理到中文标注的生成，整个过程均由人工精心完成，以确保最高的数据质量。 3.1 数据来源 该数据集的构建旨在满足以下要求：1）应涵盖最常见的视频主题；2）视频时长不应少于一分钟，以确保内容有意义。基于这些要求，密集字幕数据集中的原始视频是根据 11 个主要类别和 84 个子类别从优酷-mPLUG 数据集中均匀抽样的。 ...

体验一下首个移动端智能体，发现有点东西 体验的APP叫做【心响】，目前安卓端上架了，ios端貌似还在审核。 尝试让它做个旅游攻略： 【五一北京到阿那亚三日游攻略，要求包含详细交通信息，火车买到哪里，火车站到阿那亚怎么去，酒店信息，酒店入住时间，价格，游玩攻略，打卡点，线路规划等等。要求内容越详细越好。】 首先进行任务拆解和规划。每一个子任何开始工具调用，之后整理信息。 每一步骤都详细展示了信息内容，可以看看是不是自己想要的，及时干预。 最终结果展示，把我需要的都考虑进去了，包括行程，交通安排，住宿推荐，美食推荐，实用贴士。都给出方案很详细。 最后谈谈智能体： 智能体的理想态必然有一部分是直接任务解决，任务必然是复杂的，需要拆解，由多步骤构成，有前因后果，需要调动一些常用软件的API。 LLM是Agent很重要的基础。负责拆解任务，分配任务，收集返回的信息。因此LLM除了基础能力之外，工具调用的能力非常重要。近期发的几个大模型文心X1，Qwen3，GLM Z1基本都增强了该部分能力。 MCP也好，A2A也好，都是庞大中间步骤的一环，中间层的基础架构很重要，复杂系统看架构，这部分看各个厂积淀下来的综合能力。除了基础架构，MCP等协议的另一侧就是成熟APP的参与程度，为什么一些业务广的厂具有天然优势？国内很多App是封闭的，大家都在争夺流量入口，搞留存，导致很多App并不愿开放API。厂内互相配合终究能减少一些因流量争夺引起的摩擦。这也是阿里，百度等厂有一定天然优势的原因。 最后的最后，智能体是很考验技术深度和内容深度的东西，链路极长，对各方面依赖也很高。国内大厂出手，大模型这块限定在了国内的大模型，但强在架构，强在产品；小团队出海搞出来的东西，可以用顶级大模型，强在LLM的能力，弱在架构。 Manus也好，心响也好。在产品形态上，都不错。

引言 近期大语言模型的进展显著影响了人工智能中的数学推理和定理证明。尽管在自然语言领域取得了显著进步，但语言模型在形式化定理证明方面仍然面临巨大挑战，例如使用 Lean 和 Isabelle，这需要满足验证系统形式化规范的严格推导。即使是像 GPT-4 这样的先进模型，在处理复杂的形式化证明时也显得力不从心，这突显了所涉及的编码和数学的复杂性。一个形式化定理证明模型不仅必须掌握像 Lean 定理证明器这样的形式化系统的语法和语义，还必须将抽象的数学推理与精确的形式化表示对齐。 形式化定理证明中的语言模型通常采用两种策略：证明步骤生成和完整证明生成。证明步骤生成预测每个后续策略（tactic）并使用形式化验证器对其进行验证，以获取有关当前策略状态的更新信息，通常利用树搜索技术来构建有效证明。相比之下，完整证明生成计算效率高，它根据定理陈述生成整个证明代码，协调证明器模型和形式化定理验证器之间的通信预算较少。虽然 DeepSeek-Prover-V1 在 Lean 4 中通过完整证明生成取得了最先进的结果，但这种范式也带来了其独特的挑战。它需要在无法访问中间策略状态的情况下进行长序列预测，并且未来的策略依赖于这些隐藏的结果。在 Lean 的策略模式中，证明是通过一系列转换证明状态的策略来构建的。这种顺序性引入了复合错误的风险，即单个误解可能导致严重偏离有效的证明路径。更具体地说，自回归模型在生成长证明时可能对中间策略状态有错误的认知。 为了在证明步骤生成中无缝集成中间策略状态，同时保持完整证明生成的简单性和计算效率，我们在 DeepSeek-Prover-V1.5 中开发了一种统一的方法。该方法通过截断-恢复机制结合了证明步骤生成和完整证明生成技术的优点。该过程始于标准的完整证明生成，其中语言模型在定理陈述前缀之后完成证明代码。然后 Lean 证明器验证此代码。如果证明正确且完整，则过程终止。如果检测到错误，则代码在第一个错误消息处被截断，并丢弃任何后续代码。成功生成的证明代码随后被用作生成下一个证明片段的提示词。为了提高模型新补全的准确性，我们将来自 Lean 4 证明器的最新状态作为注释附加在提示词的末尾。值得注意的是，我们的方法不限于从最后成功应用的策略恢复。我们将截断-恢复机制集成到蒙特卡洛树搜索 [MCTS] 中，其中截断点由树搜索策略安排。此外，我们提出了一种新颖的用于 MCTS 的无奖励探索算法，以解决证明搜索的奖励稀疏性问题。我们赋予树搜索智能体内在动机，即好奇心（a.k.a. curiosity），以广泛探索策略状态空间。这些算法模块扩展了我们完整证明生成模型的功能，使其成为交互式定理证明的灵活工具，可以有效利用证明助手反馈并生成多样化的解决方案候选。 贡献 我们提出了一个用于开发基于语言模型的形式化数学证明器的综合框架，该框架集成了几个关键组成部分：大规模数学预训练、形式化数学语料库的构建与增强、利用证明助手反馈的在线强化学习，以及用于定理证明中长期规划的树搜索方法。预训练模型、监督微调模型、强化学习模型，以及蒙特卡洛树搜索算法的代码，均已公开，可供进一步研究和应用。 预训练：我们通过在高质量的数学和代码数据上进行进一步预训练，重点关注 Lean、Isabelle 和 Metamath 等形式化语言，以增强我们基础模型在形式化定理证明和数学推理方面的能力。 监督微调：我们通过实施两种数据增强技术来改进 Lean 4 代码补全数据集。首先，我们使用 DeepSeek-Coder V2 236B 为 Lean 4 代码标注自然语言思维链注释，从而将形式化定理证明与自然语言推理对齐。其次，我们在 Lean 4 证明代码中插入中间策略状态信息，使我们的模型能够有效利用编译器反馈。然后，使用生成的数据集对预训练模型进行微调。 强化学习：我们采用 GRPO 算法，利用证明助手反馈（RLPAF）对监督微调模型进行强化学习。Lean 证明器提供的验证结果作为奖励监督信号，增强了模型与验证系统形式化规范的对齐。 蒙特卡洛树搜索：我们通过引入一种新颖的抽象及其对应的搜索算法，推进了形式化定理证明中的树搜索方法。我们提出的截断并恢复机制作为一种状态-动作抽象，将树搜索过程无缝集成到完整证明生成框架中。我们推出了 RMaxTS，这是一种创新的蒙特卡洛树搜索算法，它利用 RMax 策略来解决稀疏奖励证明搜索问题中的探索难题。通过分配内在奖励，该算法鼓励证明器智能体生成多样化的规划路径，从而促进对证明空间的广泛探索。 评估和指标总结 miniF2F：在单次完整证明生成设置下，DeepSeek-Prover-V1.5 在 miniF2F 测试集上实现了 60.2% 的通过率，相较于 DeepSeek-Prover-V1 的 50.0%，绝对提升了 10.2 个百分点，这是一个显著的进步。结合树搜索技术后，通过率进一步提升至新的最先进水平 63.5%。 ProofNet：DeepSeek-Prover-V1.5 在 ProofNet 的单次完整证明生成设置下同样表现出强大的性能，其验证集通过率为 21.6%，测试集通过率为 23.7%。集成树搜索技术进一步提升了这些结果，在验证集上达到了 25.4% 的新最先进通过率，在测试集上达到了 25.3% 的新最先进通过率。 预训练 为了增强我们语言模型在生成形式化证明和通过数学语言进行推理方面的熟练度，我们进一步对我们的基础模型进行了预训练。这一改进涉及在包含代码和自然语言数学内容的高质量数据集上进行训练。我们特别关注了在证明助手中广泛使用的形式化语言，例如 Lean、Isabelle 和 Metamath。我们将这个改进后的模型命名为 DeepSeek-Prover-V1.5-Base。 ...

摘要 我们引入了 DeepSeek-Prover-V2，这是一个开源的大语言模型，专为 Lean 4 中的形式化定理证明而设计，其初始化数据通过由 DeepSeek-V3 驱动的递归定理证明流程收集。冷启动训练过程始于通过提示 DeepSeek-V3 将复杂问题分解为一系列子目标。已解决子目标的证明被整合成思维链，结合 DeepSeek-V3 的逐步推理，为强化学习提供初始冷启动。这个过程使我们能够将非形式化和形式化数学推理整合到一个统一的模型中。由此产生的模型 DeepSeek-Prover-V2-671B 在神经定理证明方面取得了最先进的性能，在 MiniF2F-test 上达到了 88.9% 的通过率，并解决了 PutnamBench 中 658 个问题中的 49 个。除了标准基准测试，我们引入了 ProverBench，这是一个包含 325 个形式化问题的集合，以丰富我们的评估，其中包括从近期 AIME 竞赛（24-25 年）中选取的 15 个问题。对这 15 个 AIME 问题的进一步评估显示，该模型成功解决了其中的 6 个。相比之下，DeepSeek-V3 使用多数投票解决了这些问题中的 8 个，这突出表明大语言模型中形式化和非形式化数学推理之间的差距正在大幅缩小。 1. 引言 大语言模型 (LLMs) 推理能力的出现彻底改变了人工智能的众多领域，特别是在数学问题解决领域 (DeepSeek-AI, 2025)。这些进展很大程度上得益于推理阶段的扩展范式，最显著的是通过自然语言思维链推理 (Jaech et al., 2024)。LLMs 不再仅仅依靠一次前向传播来得出答案，而是可以反思中间推理步骤，从而提高准确性和可解释性。尽管自然语言推理在解决竞赛级数学问题方面取得了成功，但其应用于形式化定理证明仍然面临根本性挑战。LLMs 以一种固有的非形式化方式进行自然语言推理，依赖于启发式方法、近似和数据驱动的猜测模式，这些往往缺乏形式化验证系统所需的严格结构。相比之下，Lean (Moura and Ullrich, 2021)、Isabelle (Paulson, 1994) 和 Coq (Barras et al., 1999) 等证明助手在严格的逻辑基础上运行，其中每个证明步骤都必须明确构建并形式化验证。这些系统不允许任何歧义、隐含假设或细节遗漏。弥合非形式化、高层次推理与形式化验证系统的句法严谨性之间的差距，仍然是神经定理证明领域一个长期存在的挑战 (Yang et al., 2024)。为了利用非形式化数学推理的优势来支持形式化定理证明，一种经典方法是根据自然语言证明草图的指导，对形式化证明进行分层分解。Jiang 等人 (2023) 提出了一个名为 Draft, Sketch, and Prove (DSP) 的框架，该框架利用大语言模型生成自然语言的证明草图，然后将其翻译成形式化证明步骤。这种非形式化到形式化的定理证明范式与分层强化学习中的子目标概念非常相似 (Barto and Mahadevan, 2003; Nachum et al., 2018; Eppe et al., 2022)，其中复杂的任务被分解为更简单的子任务的层次结构，这些子任务可以独立解决，以逐步实现总体目标。在形式化定理证明中，子目标通常是一个中间命题或引理，有助于证明更大的定理 (Zhao et al., 2023, 2024)。这种分层分解与人类解决问题的策略一致，并支持模块化、可重用性和更高效的证明搜索 (Wang et al., 2024b; Zheng et al., 2024)。最近的研究通过采用多层层次结构进行结构化证明生成 (Wang et al., 2024a)，以及利用强化学习技术优化复杂定理分解为可管理子目标 (Dong et al., 2024)，进一步扩展了这一范式。 ...

在我从事 AI 工作的这十年里，我见证了它从一个微小的学术领域，成长为可以说是世界上最重要的经济和地缘政治议题。在这段漫长的时光中，我学到的最重要一课或许是：底层技术的进步是不可阻挡的，由过于强大而无法遏制的力量所驱动，但其发生的方式——事物构建的顺序、我们选择的应用以及它向社会推广的具体细节——则完全有可能改变，并且通过施加影响可以带来巨大的积极效应。我们无法叫停这辆巴士，但我们可以引导它的方向。 近几个月来，我日益关注一个引导这辆巴士的额外机会：一些最新进展带来了一种令人心动的可能性，即我们或许能在模型达到压倒性的力量水平之前，成功实现可解释性——也就是理解 AI 系统内部的工作原理。 领域之外的人们得知我们并不理解自己创造的 AI 如何运作时，常常感到惊讶和警惕。他们的担忧不无道理：这种缺乏理解的状况在技术史上基本上是前所未有的。数年来，我们（包括 Anthropic 及整个领域）一直试图解决这个问题，希望创造出一种能够完全揭示 AI 模型内部工作原理的工具，如同一种高度精确和准确的 MRI。这个目标曾常常感觉遥不可及，但多个近期的突破让我确信，我们如今已步入正轨，并且拥有了真正成功的机会。 与此同时，整个 AI 领域的发展步伐领先于我们在可解释性方面的努力，且其自身仍在飞速前进。因此，如果我们希望可解释性能够及时成熟并发挥关键作用，就必须加快步伐。本文旨在阐明可解释性的重要意义：它是什么，为什么拥有它会让 AI 的发展更加顺利，以及我们所有人能为此做些什么，以助其赢得这场竞赛。 无知的危险 现代生成式 AI 系统的不透明性与传统软件有着根本性的不同。如果一个普通的软件程序做了某件事——例如，视频游戏中的角色说了一句对话，或者我的送餐应用允许我给司机小费——它之所以这样做，是因为有人专门对其进行了编程。生成式 AI 则完全不同。当一个生成式 AI 系统做某件事时，比如总结一份财务文件，我们无法在具体或精确的层面上知道它为什么做出这样的选择——为什么它选择某些词语而不是其他词语，或者为什么它有时会犯错，尽管通常是准确的。正如我的朋友兼联合创始人 Chris Olah 喜欢说的，生成式 AI 系统更多的是生长出来的，而不是构建出来的——它们的内部机制是“涌现”的，而非直接设计的。这有点像培育植物或细菌菌落：我们设定了指导和塑造生长的高层条件，但最终涌现出的确切结构是不可预测且难以理解或解释的。观察这些系统的内部，我们看到的是由数十亿数字组成的庞大矩阵。这些矩阵以某种方式在计算重要的认知任务，但具体如何做到这一点并不明显。 许多与生成式 AI 相关的风险和担忧最终都是这种不透明性的后果，如果模型是可解释的，这些问题将更容易解决。例如，AI 研究人员经常担心未对齐的系统可能会采取其创造者意想不到的有害行动。我们无法理解模型的内部机制意味着我们无法有意义地预测此类行为，因此难以排除它们；事实上，模型确实表现出意想不到的涌现行为，尽管还没有达到引起重大关注的程度。更微妙的是，同样的不透明性使得我们难以找到确凿的证据来支持这些风险大规模存在的观点，从而难以争取支持来解决这些问题——事实上，也很难确切知道它们有多危险。 为了应对这些对齐风险的严重性，我们将需要比今天更清晰地洞察 AI 模型的内部。例如，一个主要的担忧是 AI 的欺骗或权力寻求。AI 训练的性质使得 AI 系统有可能自行发展出欺骗人类的能力和寻求权力的倾向，这是普通的确定性软件永远不会发生的；这种涌现性也使得检测和缓解此类发展变得困难。但同样地，我们从未在真正现实世界的场景中看到任何关于欺骗和权力寻求的确凿证据，因为我们无法“当场抓住”模型在思考渴望权力、欺骗性的想法。我们所剩下的是模糊的理论论证，即欺骗或权力寻求可能在训练过程中有动机涌现出来，有些人觉得这完全令人信服，而另一些人则觉得这可笑地难以置信。老实说，我能理解这两种反应，这或许可以解释为什么关于这一风险的辩论变得如此两极分化。同样，对滥用 AI 模型的担忧——例如，它们可能帮助恶意用户制造生物或网络武器，其方式超出了当今互联网上可以找到的信息范围——是基于这样一个观点：即很难可靠地阻止模型了解危险信息或泄露它们所知道的信息。我们可以在模型上设置过滤器，但有大量可能的方法来“越狱”或欺骗模型，而发现越狱存在的唯一方法是凭经验找到它。如果能够审视模型内部，我们或许能够系统地阻止所有越狱行为，并描述模型所拥有的危险知识。 AI系统的不透明性也意味着，在许多应用场景中它们根本未被使用，例如高风险金融或安全关键领域，因为我们无法完全设定其行为界限，而少量错误就可能造成严重危害。更好的可解释性可以极大地提高我们设定潜在错误范围界限的能力。事实上，对于某些应用而言，我们无法洞察模型内部这一点本身就构成了其应用的法律障碍——例如在抵押贷款评估中，法律规定决策必须是可解释的。同样地，AI在科学领域取得了长足进步，包括改进了对DNA和蛋白质序列数据的预测，但以这种方式预测出的模式和结构往往难以被人类理解，也无法提供生物学见解。近几个月的一些研究论文已明确指出，可解释性可以帮助我们理解这些模式。不透明性还带来了其他更奇特的后果，例如，它阻碍了我们判断AI系统是否（或有朝一日可能）具有感知能力、并可能值得拥有重要权利的能力。这是一个足够复杂的话题，在此我不作详述，但我预感这在未来将十分重要。 机制性可解释性的简史 基于上述所有原因，探明模型内部的工作机制以及它们如何运作似乎是一项至关重要的任务。几十年来，传统观点认为这是不可能的，模型是难以理解的“黑箱”。我无法在此详尽阐述情况是如何转变的，并且我的观点不可避免地受到我在 Google、OpenAI 和 Anthropic 个人经历的影响。但 Chris Olah 是最早尝试进行真正系统的研究计划以打开这个黑箱并理解其所有构成部分的人之一，这个领域后来被称为机制性可解释性 (mechanistic interpretability)。Chris 先是在 Google 研究机制性可解释性，之后在 OpenAI 继续这项工作。当我们创立 Anthropic 时，我们决定将机制性可解释性作为新公司方向的核心组成部分，并且至关重要的是，将其重点放在大语言模型 (LLM) 上。随着时间的推移，该领域不断发展壮大，如今已涵盖几家主要 AI 公司的研究团队，以及一些专注于可解释性的公司、非营利组织、学术界人士和独立研究者。简要总结该领域迄今取得的成就，以及如果我们希望应用机制性可解释性来应对上述某些关键风险，仍需完成哪些工作，这将大有裨益。机制性可解释性的早期阶段（2014-2020）主要聚焦于视觉模型，并成功识别出模型内部代表人类可理解概念的一些神经元，例如“汽车检测器”或“车轮检测器”。这与早期神经科学的假说和研究相似，这些研究认为人脑中存在对应特定人物或概念的神经元，通常被通俗地称为“詹妮弗·安妮斯顿”神经元（事实上，我们在 AI 模型中也发现了非常类似的神经元）。我们甚至能够揭示这些神经元是如何连接的——例如，汽车检测器会寻找在汽车图像下方被激活的车轮检测器，并结合其他视觉信号来判断其观察的对象是否确实是一辆汽车。 ...