Seventy3 是一档借助 NotebookLM 解读前沿论文的播客——不是念摘要，也不是泛泛而谈，而是让 AI 帮你把论文掰开揉碎，说人话。我们蹲在人工智能、大模型、机器人算法、crypto 这几个领域，每期挑一篇值得关注的工作，用对话的方式聊给你听。你可以在通勤路上听，做实验的时候听，也可以当背景音放着，让新知识自然地长进脑子里。

如果你正在做有意思的研究，想让更多人看到——不管你是博士生、独立研究者还是实验室的博士后——把论文发给我们，我们帮你用 AI 做一期深度解读，让你的工作被更多同路人发现。

联系小助手微信：seventy3_podcast（加群/投稿论文）

今天的这篇的主题是：

Agents’ Last Exam

Summary

近期的人工智能系统在一系列广泛的基准测试中取得了优异的成绩，然而这些进步并未能在众多专业领域中转化为具备经济意义的落地应用。我们认为，这一差距很大程度上源于评估环节的问题：目前被广泛使用的基准测试缺乏对真实且具备经济价值的工作流程进行持续性的性能测量。

本文介绍了“Agent 的终极考场”（Agents' Last Exam, 简称 ALE），这是一个旨在评估 AI Agent 在具有可验证结果、长流程、具备经济价值且贴近现实世界任务中表现的基准测试。ALE 是与 250 多位行业专家合作开发的，其覆盖的非物理产业均参考了 O*NET / SOC 2018（美国联邦职业分类体系）进行定义。它围绕一个包含 55 个子领域、归类为 13 个行业集群的任务分类体系展开，涵盖 1000 多个任务。

目前的结果表明，最难的梯队距离“饱和”还差得远：在主流的框架（harness）和骨干模型（backbone）配置下，平均完全通过率低于 1%。ALE 被设计为一个动态发展的基准测试：随着新工作流程和新行业的不断加入，其任务池将持续扩大。更广泛地说，ALE 的定位不仅是另一个排行榜，更是缩小基准测试的成功与对国内生产总值（GDP）产生实际影响之间差距的工具。

原文链接：https://arxiv.org/abs/2606.05405

Seventy3 是一档借助 NotebookLM 解读前沿论文的播客——不是念摘要，也不是泛泛而谈，而是让 AI 帮你把论文掰开揉碎，说人话。我们蹲在人工智能、大模型、机器人算法、crypto 这几个领域，每期挑一篇值得关注的工作，用对话的方式聊给你听。你可以在通勤路上听，做实验的时候听，也可以当背景音放着，让新知识自然地长进脑子里。

如果你正在做有意思的研究，想让更多人看到——不管你是博士生、独立研究者还是实验室的博士后——把论文发给我们，我们帮你用 AI 做一期深度解读，让你的工作被更多同路人发现。

联系小助手微信：seventy3_podcast（加群/投稿论文）

今天的这篇的主题是：

Self-Harness: Harnesses That Improve Themselves

Summary

Based LLM-based agent（基于大语言模型的智能体）的性能受其基座模型以及协调其与环境交互的框架/驾驭系统（harness）共同塑造。由于不同的模型表现出截然不同的行为特征，因此有效的 harness 设计本质上是需要针对特定模型定制的。然而，智能体 harness 至今在很大程度上仍由人类专家手动工程化构建，随着现代 LLM 日益多样化且快速迭代，这种范式在扩展性方面表现极差。

在本文中，我们提出了 Self-Harness——一种全新的范式，在此范式下，基于 LLM 的智能体可以在不依赖人类工程师或更强外部智能体的情况下，自我改进其运行 harness。我们将 Self-Harness 实例化为一个包含三个阶段的迭代循环：

1. 弱点挖掘（Weakness Mining）：从执行轨迹中识别特定模型的失败模式；

2. Harness 方案提出（Harness Proposal）：生成与这些失败紧密相关的、多样化且最小化的 harness 修正方案；

3. 方案验证（Proposal Validation）：仅在通过回归测试后才接受候选的修改。

我们在 Terminal-Bench-2.0 上使用一个极简的初始 harness 以及来自不同家族的三款基座模型（MiniMax M2.5、Qwen3.5-35B-A3B 和 GLM-5）对 Self-Harness 进行了实例化评估。在这三款模型上，Self-Harness 均一致提升了性能，保留测试集（held-out）的通过率分别从 40.5% 提升至 61.9%、从 23.8% 提升至 38.1%，以及从 42.9% 提升至 57.1%。

定性分析进一步表明，Self-Harness 并不仅仅是添加通用的指令，而是有效地将特定模型的弱点转化为具体、可执行的 harness 改动。这些结果表明，基于 LLM 的智能体不仅能被其 harness 塑造，还能开辟一条参与重塑自身 harness 的演进路径。

原文链接：https://arxiv.org/abs/2606.09498

Seventy3 是一档借助 NotebookLM 解读前沿论文的播客——不是念摘要，也不是泛泛而谈，而是让 AI 帮你把论文掰开揉碎，说人话。我们蹲在人工智能、大模型、机器人算法、crypto 这几个领域，每期挑一篇值得关注的工作，用对话的方式聊给你听。你可以在通勤路上听，做实验的时候听，也可以当背景音放着，让新知识自然地长进脑子里。

如果你正在做有意思的研究，想让更多人看到——不管你是博士生、独立研究者还是实验室的博士后——把论文发给我们，我们帮你用 AI 做一期深度解读，让你的工作被更多同路人发现。

联系小助手微信：seventy3_podcast（加群/投稿论文）

今天的这篇的主题是：

MiniMax Sparse Attention

Summary

超长上下文能力正在成为前沿大语言模型（LLM）不可或缺的能力：智能体工作流（agentic workflows）、代码仓库级别的代码推理（repository-scale code reasoning）以及持久化记忆（persistent memory）都要求模型能够联合关注数十万到数百万级别的 token。然而，softmax 注意力机制的二次计算复杂度，使得这种能力在实际部署规模下难以实现。

我们提出了 MiniMax 稀疏注意力（MiniMax Sparse Attention, MSA），这是一种基于分组查询注意力（Grouped Query Attention, GQA）构建的块级稀疏注意力机制。MSA 包含一个轻量级的索引分支（Index Branch），用于对键值（key-value）块进行评分，并为每个 GQA 组独立选择一个 Top-k 子集，从而实现针对不同组的稀疏检索，同时保持高效的块级执行；随后，**主分支（Main Branch）**仅在被选中的块上执行精确的块稀疏注意力计算。

MSA 的设计遵循简单性与可扩展性原则，经过刻意精简，使其能够在广泛的 GPU 平台上直接高效部署。为了将稀疏性转化为实际的速度提升，我们进一步针对 MSA 设计了专用的 GPU 执行路径：该路径采用无指数运算（exp-free）的 Top-k 选择机制以及 KV 外置稀疏注意力（KV-outer sparse attention），在块粒度访问模式下提升张量核心（tensor core）的利用率。

在一个具有原生多模态训练能力的 109B 参数模型上，MSA 的性能与 GQA 基本相当，同时在 100 万 token 上下文长度下，将每个 token 的注意力计算量降低了 28.4 倍。结合我们共同设计的 GPU 内核（kernel），MSA 在 H800 GPU 上实现了 14.2 倍的预填充（prefill）加速以及 7.6 倍的解码（decoding）端到端速度提升。

原文链接：https://arxiv.org/abs/2606.13392

Seventy3 是一档借助 NotebookLM 解读前沿论文的播客——不是念摘要，也不是泛泛而谈，而是让 AI 帮你把论文掰开揉碎，说人话。我们蹲在人工智能、大模型、机器人算法、crypto 这几个领域，每期挑一篇值得关注的工作，用对话的方式聊给你听。你可以在通勤路上听，做实验的时候听，也可以当背景音放着，让新知识自然地长进脑子里。

如果你正在做有意思的研究，想让更多人看到——不管你是博士生、独立研究者还是实验室的博士后——把论文发给我们，我们帮你用 AI 做一期深度解读，让你的工作被更多同路人发现。

联系小助手微信：seventy3_podcast（加群/投稿论文）

今天的这篇的主题是：

Language Models Need Sleep: Learning to Self-Modify and Consolidate Memories

Summary

过去几十年见证了机器学习算法设计领域的重大进步，从早期针对特定任务的浅层模型研究，到如今更加通用的深度大语言模型（Large Language Models, LLMs）。尽管现有模型在需要即时预测或上下文学习（in-context learning）的任务中展现出了良好的效果，但它们仍然缺乏持续学习的能力，也无法有效地将其随时间积累的上下文知识迁移到长期参数中。

受到人类学习过程的启发，我们引入了一种称为 “睡眠（Sleep）”范式 的方法，使模型能够持续学习，通过回放（replay）机制将短期且脆弱的记忆蒸馏为稳定的长期知识，并通过“做梦（Dreaming）”过程递归地实现自我改进。

更具体地说，睡眠过程包含两个阶段：

（1）记忆巩固（Memory Consolidation）：
这是一个向上的蒸馏过程，称为知识播种（Knowledge Seeding）。在该过程中，将较小版本自身模型（smaller-self）的记忆蒸馏到一个更大的网络中，从而在保留已有知识的同时提供更大的容量。作为概念验证，我们提出了一种新的用于知识播种的广义蒸馏过程（Generalized Distillation process），即结合了**在策略蒸馏（on-policy distillation）**与基于强化学习（Reinforcement Learning, RL）的模仿学习（imitation learning）的蒸馏方法。

（2）做梦（Dreaming）：
这是一个自我改进阶段。在该阶段，模型利用强化学习生成一个合成数据课程（curriculum of synthetic data），用于反复练习新知识，并在无需人工监督的情况下优化已有能力。

我们在长时间跨度任务（long-horizon tasks）、持续学习任务（continual learning）、知识融入任务（knowledge incorporation）以及少样本泛化任务（few-shot generalization tasks）上的实验结果，验证了睡眠阶段的重要性。

原文链接：https://arxiv.org/abs/2606.03979

Seventy3 是一档借助 NotebookLM 解读前沿论文的播客——不是念摘要，也不是泛泛而谈，而是让 AI 帮你把论文掰开揉碎，说人话。我们蹲在人工智能、大模型、机器人算法、crypto 这几个领域，每期挑一篇值得关注的工作，用对话的方式聊给你听。你可以在通勤路上听，做实验的时候听，也可以当背景音放着，让新知识自然地长进脑子里。

如果你正在做有意思的研究，想让更多人看到——不管你是博士生、独立研究者还是实验室的博士后——把论文发给我们，我们帮你用 AI 做一期深度解读，让你的工作被更多同路人发现。

联系小助手微信：seventy3_podcast（加群/投稿论文）

今天的这篇的主题是：

Nested Learning: The Illusion of Deep Learning Architecture

Summary

尽管近年来取得了显著进展，尤其是在语言模型的发展方面，但关于这类模型如何能够持续学习/记忆、自我改进以及寻找有效解决方案，仍然存在一些根本性的挑战和未解问题。在本文中，我们提出了一种新的学习范式，称为嵌套学习（Nested Learning, NL）。该范式以一种统一的方式，将机器学习模型表示为一组嵌套的、多层次的和/或并行的优化问题，其中每一个优化问题都具有其自身的上下文流（context flow）。

通过 NL 的视角来看，现有的深度学习方法通过压缩自身的上下文流来从数据中学习，而**上下文学习（in-context learning）**则自然地在大规模模型中涌现出来。NL 提出了一种设计理念：通过引入更多层次来设计具有更强表达能力的学习算法，从而实现更高阶的上下文学习，并有可能解锁有效的持续学习能力。

我们通过以下三个核心贡献来阐述并倡导 NL：

（1）表达性优化器（Expressive Optimizers）：
我们展示了，诸如 Adam、带动量的 SGD（SGD with Momentum）等已知的基于梯度的优化器，实际上是联想记忆模块（associative memory modules），其目标是通过梯度下降来压缩梯度信息。在这一洞见的基础上，我们提出了其他更具表达能力的优化器，它们具备深层记忆能力和/或更强大的学习规则。

（2）自修改学习模块（Self-Modifying Learning Module）：
利用 NL 对学习算法的洞察，我们提出了一种序列模型，该模型能够通过学习自身的更新算法，来学习如何修改自身。

（3）连续记忆系统（Continuum Memory System）：
我们提出了一种新的记忆系统表述方式，将传统的长短期记忆（long/short-term memory）视角进行了推广。结合我们的自修改序列模型与连续记忆系统，我们提出了一种持续学习模块，称为 Hope。实验结果表明，该模块在语言建模、知识融入、少样本泛化任务、持续学习任务以及长上下文推理任务中均展现出了良好的潜力。

原文链接：https://arxiv.org/abs/2512.24695

Seventy3 是一档借助 NotebookLM 解读前沿论文的播客——不是念摘要，也不是泛泛而谈，而是让 AI 帮你把论文掰开揉碎，说人话。我们蹲在人工智能、大模型、机器人算法、crypto 这几个领域，每期挑一篇值得关注的工作，用对话的方式聊给你听。你可以在通勤路上听，做实验的时候听，也可以当背景音放着，让新知识自然地长进脑子里。

如果你正在做有意思的研究，想让更多人看到——不管你是博士生、独立研究者还是实验室的博士后——把论文发给我们，我们帮你用 AI 做一期深度解读，让你的工作被更多同路人发现。

联系小助手微信：seventy3_podcast（加群/投稿论文）

今天的这篇的主题是：

Learn from your own latents and not from tokens: A sample-complexity theory

Summary

生成模型——从扩散模型（diffusion models）到大型语言模型（LLMs）——已经取得了卓越的性能，但代价是需要规模远超生物学习系统的数据进行训练，其训练数据量通常比生物学习者所需的数据高出数个数量级。

近年来，一种新的学习范式逐渐兴起：网络不再预测原始输入，而是预测自身对于相关视图（related views）或被遮蔽区域（masked regions）的潜在表示（latent representations），代表性方法包括 data2vec 和 JEPA（Joint Embedding Predictive Architecture）。这一思想也与神经科学中关于大脑皮层**预测编码（predictive coding）**的理论相呼应。

尽管这些方法已经取得了优异的实验效果，但其理论基础仍然缺乏充分理解。其中两个核心问题是：

1. 预测潜在表示究竟能够在多大程度上提升数据效率（data efficiency）？

2. 将这种潜在预测机制堆叠成多尺度层次结构（multi-scale hierarchies）是否能够进一步带来收益？

本文针对这两个问题给出了理论回答。

作者采用了一种**可解析的概率上下文无关文法（Probabilistic Context-Free Grammar，PCFG）**作为数据生成模型，以模拟自然语言和图像所具有的组合结构（compositional structure）。

在该模型中，数据的生成过程如下：

• 首先构造一个深度为 LL 的隐藏符号树（latent tree）；

• 然后递归应用文法产生式（production rules）；

• 最终生成由可观测 token 构成的字符串。

在这一数据模型下，作者证明：

• 无论是监督学习（supervised learning）还是基于 Token 的自监督学习（token-level self-supervised learning），若要恢复隐藏树结构，都需要**关于树深度 LL 指数增长（exponential in LL）**数量的训练样本。

• 相比之下，**潜在表示预测（latent prediction）仅需与树深度 LL 无关（constant in LL）**的样本数量（除去对数因子），即可恢复相同的隐藏结构。

这意味着，相对于传统监督学习和 Token 级自监督学习，潜在预测能够将样本复杂度从指数级降低到常数级（忽略对数项）。

作者进一步通过三方面验证了这一理论结果：

1. 层次聚类算法（hierarchical clustering algorithm）；

2. 一个端到端神经网络，其中每一层都包含预测器（predictor）和聚类器（clusterer）模块，并通过梯度下降不断预测自身的潜在表示，实现逐层的潜在预测；

3. 首次对 data2vec 的样本复杂度进行了理论分析，证明 data2vec 实际上隐式地（implicitly）执行了层次化潜在预测（hierarchical latent prediction）。

基于这些分析，作者进一步指出：

由于 data2vec 已经在内部实现了层次化的潜在预测，因此再显式地构建多层预测结构（例如 H-JEPA 这类层次化 JEPA 架构）所带来的额外收益其实非常有限，在很大程度上是**冗余（largely redundant）**的。

总体而言，本文从理论上解释了为什么预测潜在表示能够显著提高数据效率，并表明这种优势已经能够通过 data2vec 等方法自然实现，而无需额外设计复杂的层次化预测架构。

原文链接：https://arxiv.org/abs/2605.27734

Seventy3 是一档借助 NotebookLM 解读前沿论文的播客——不是念摘要，也不是泛泛而谈，而是让 AI 帮你把论文掰开揉碎，说人话。我们蹲在人工智能、大模型、机器人算法、crypto 这几个领域，每期挑一篇值得关注的工作，用对话的方式聊给你听。你可以在通勤路上听，做实验的时候听，也可以当背景音放着，让新知识自然地长进脑子里。

如果你正在做有意思的研究，想让更多人看到——不管你是博士生、独立研究者还是实验室的博士后——把论文发给我们，我们帮你用 AI 做一期深度解读，让你的工作被更多同路人发现。

联系小助手微信：seventy3_podcast（加群/投稿论文）

今天的这篇的主题是：

Learning Agent-Compatible Context Management for Long-Horizon Tasks

Summary

大语言模型（LLM）智能体在现实应用中越来越多地需要完成长时程任务（long-horizon tasks），例如网络搜索（web search）和深度研究（deep research）。然而，随着交互上下文不断累积，智能体容易出现**长上下文退化（long-context degradation）和推理能力下降（reasoning failures）**等问题。

现有工作通常通过**上下文管理（context management）来缓解这一问题，例如由智能体自身控制上下文，或采用固定策略（如摘要生成）对上下文进行压缩。然而，这些方法往往需要重新训练智能体以适应相应策略，因此对于闭源智能体（closed-source agents）**而言难以应用；同时，它们也忽略了不同智能体可能需要采用不同上下文管理策略这一事实。

为此，我们提出 Adaptive Context Management（AdaCoM）。AdaCoM 并不修改智能体本身，而是训练一个外部大语言模型（external LLM）作为上下文管理器，通过灵活的上下文修改操作（flexible modification actions）以及端到端强化学习（end-to-end reinforcement learning），为一个保持冻结（frozen）的智能体动态管理其上下文。

在多个不同智能体以及网络搜索和深度研究基准上的实验表明，AdaCoM 能够在**删除过时信息（pruning stale content）**的同时，尽可能保留任务约束（task constraints）和执行进度（task progress），从而显著提升智能体的整体性能。

进一步分析学习得到的上下文管理策略，我们发现了一种保真度—可靠性权衡（Fidelity–Reliability Trade-off）：

• 基础 ReAct 表现较强的智能体，更适合采用**高保真（higher-fidelity）**的上下文保留策略，即尽可能保留完整上下文，以维持其推理能力。

• 基础性能较弱的智能体，则需要采用更加激进的上下文压缩策略，以避免过长上下文导致推理失稳，使其始终保持在一个**可靠的推理工作区间（reliable reasoning regime）**内。

此外，我们还进行了跨智能体迁移实验（transfer experiments）。结果表明，AdaCoM 在能力水平相近（以原始 ReAct 性能为衡量标准）的智能体之间具有最佳的迁移效果。这说明，一个为某类智能体训练得到的上下文管理器，可以较容易地复用于能力相近的其他智能体。

这些结果表明，将上下文管理从智能体本身解耦出来，并通过一个可复用的外部上下文管理器进行学习和优化，是构建长时程智能体系统的一条切实可行的发展路径。

原文链接：https://arxiv.org/abs/2605.30785

Seventy3 是一档借助 NotebookLM 解读前沿论文的播客——不是念摘要，也不是泛泛而谈，而是让 AI 帮你把论文掰开揉碎，说人话。我们蹲在人工智能、大模型、机器人算法、crypto 这几个领域，每期挑一篇值得关注的工作，用对话的方式聊给你听。你可以在通勤路上听，做实验的时候听，也可以当背景音放着，让新知识自然地长进脑子里。

如果你正在做有意思的研究，想让更多人看到——不管你是博士生、独立研究者还是实验室的博士后——把论文发给我们，我们帮你用 AI 做一期深度解读，让你的工作被更多同路人发现。

联系小助手微信：seventy3_podcast（加群/投稿论文）

今天的这篇的主题是：

AUTOLAB: Can Frontier Models Solve Long-Horizon Auto Research and Engineering Tasks?

Summary

科学研究和工程创新本质上都是一个长时程（long-horizon）的迭代优化过程：不断提出改进方案、开展实验、测量结果，并持续优化已有成果。然而，目前针对前沿大语言模型的基准测试主要关注单轮回答（single-turn responses）或短时程智能体轨迹（short-horizon agent trajectories），无法充分评估智能体在长时间尺度上持续迭代改进所面临的挑战。

为弥补这一空白，我们提出 AutoLab——一个面向**超长时程闭环优化（ultra long-horizon closed-loop optimization）**的新型基准测试。

AutoLab 包含 36 个由领域专家设计的真实任务，覆盖四类具有代表性的应用场景：

• 系统优化（system optimization）；

• 谜题与挑战（puzzle & challenge）；

• 模型开发（model development）；

• CUDA Kernel 优化（CUDA kernel optimization）。

每个任务都提供一个**功能正确但刻意设计得性能欠佳（correct but deliberately suboptimal）的初始版本，并要求智能体在严格限定的墙钟时间（wall-clock time）**预算内不断改进该方案。

我们对 17 个当前最先进的大语言模型进行了评测。实验结果表明，决定最终成功与否的最关键因素，并不是智能体第一次尝试的质量，而是在整个优化过程中持续进行基准测试（benchmarking）、修改方案（editing）以及根据实验反馈不断迭代（incorporating empirical feedback）的能力。

具体而言：

• Claude Opus 4.6 展现出了较强的长时程优化能力，能够持续推进任务并不断改进结果；

• 而大多数前沿模型（包括多个闭源商业模型）则表现出明显不足，要么过早停止优化（terminate prematurely），要么在几乎没有取得有效进展的情况下耗尽全部时间预算。

这些实验结果进一步说明，对于自主智能体而言，**时间意识（time awareness）以及持续迭代优化（persistent iteration）**是实现长期自主工作的关键能力，而不仅仅是生成一次高质量的初始解。

为了促进这一方向的发展，我们将 AutoLab 的完整内容全部开源，包括：

• 基准任务（benchmark）；

• 评测 Harness（evaluation harness）；

• 全部任务相关工件（task artifacts）。

希望借此推动能够真正胜任长时程自主优化任务的智能体研究。

原文链接：https://arxiv.org/abs/2606.05080

Seventy3 是一档借助 NotebookLM 解读前沿论文的播客——不是念摘要，也不是泛泛而谈，而是让 AI 帮你把论文掰开揉碎，说人话。我们蹲在人工智能、大模型、机器人算法、crypto 这几个领域，每期挑一篇值得关注的工作，用对话的方式聊给你听。你可以在通勤路上听，做实验的时候听，也可以当背景音放着，让新知识自然地长进脑子里。

如果你正在做有意思的研究，想让更多人看到——不管你是博士生、独立研究者还是实验室的博士后——把论文发给我们，我们帮你用 AI 做一期深度解读，让你的工作被更多同路人发现。

联系小助手微信：seventy3_podcast（加群/投稿论文）

今天的这篇的主题是：

Summary

智能体 Harness 通过控制工具使用、反馈机制、结果验证、记忆管理以及错误修复等环节，决定了大语言模型的实际性能。然而，传统的测试时计算开销（test-time compute）指标——例如 Token 数量、工具调用次数、运行时间（wall time）或计算成本——无法区分哪些反馈真正有助于任务完成，哪些只是冗余、无效或不稳定的交互。

我们提出 有效反馈计算（Effective Feedback Compute，EFC），作为一种基于执行轨迹（trace-level）的扩展指标，用于度量那些具有信息价值（informative）、有效（valid）、**非冗余（non-redundant）且能够被后续执行保留和利用（retained）**的反馈。

在此基础上，我们进一步提出了多个衍生指标，以适用于真实智能体运行轨迹和不同类型任务：

• Estimated-EFC：EFC 的估计版本；

• NRS-EFC：一种基于非冗余与稳定性（Non-Redundant Stable）原则构建的 EFC 指标；

• Harness 效率（Harness Efficiency，η）；

• 任务需求归一化（task-demand normalization），用于在不同复杂度任务之间进行公平比较。

我们在合成实验（synthetic）、真实数据（real）、**留出测试集（held-out）以及前瞻性实验（prospective evaluations）**中进行了全面评估。结果表明，以 EFC 为横轴建立的扩展规律，相比传统的原始计算量指标（raw compute）以及 SAS 指标，能够更准确地解释智能体性能。

具体而言：

• 在受控扩展实验中，采用 Oracle-EFC / Dtask（按任务需求归一化后的理想 EFC）作为尺度变量时，模型拟合优度达到 R² = 0.99；

• 在真实运行轨迹中，采用 NRS-EFC / Dtask 时，拟合优度仍达到 R² = 0.93；

• 相比之下，传统原始计算量指标与性能之间几乎不存在相关性，甚至出现负相关。

最后，我们提出的系统 \ours 将 EFC 作为现有 Harness 的一个**协同控制层（companion control layer）**进行集成。在相同实验设置下，该方法：

• 将平均任务通过率（pass rate）由 61.2% 提升至 68.2%；

• 同时将平均原始计算成本由 213.8 降低至 85.1。

这些结果表明，Harness 的有效扩展并不依赖于投入更多原始计算资源，而是依赖于能够持续保留、满足任务需求的高质量反馈（durable, task-sufficient feedback）。因此，相比单纯增加计算量，提升反馈质量与反馈利用效率才是推动智能体性能扩展的关键。

原文链接：https://arxiv.org/abs/2605.29682

Seventy3 是一档借助 NotebookLM 解读前沿论文的播客——不是念摘要，也不是泛泛而谈，而是让 AI 帮你把论文掰开揉碎，说人话。我们蹲在人工智能、大模型、机器人算法、crypto 这几个领域，每期挑一篇值得关注的工作，用对话的方式聊给你听。你可以在通勤路上听，做实验的时候听，也可以当背景音放着，让新知识自然地长进脑子里。

如果你正在做有意思的研究，想让更多人看到——不管你是博士生、独立研究者还是实验室的博士后——把论文发给我们，我们帮你用 AI 做一期深度解读，让你的工作被更多同路人发现。

联系小助手微信：seventy3_podcast（加群/投稿论文）

今天的这篇的主题是：

LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

Summary

大型语言模型（LLMs）在**非形式化数学推理（informal mathematical reasoning）**方面已展现出较强能力，但在生成能够被 Lean 等形式化证明语言机械验证（mechanically verifiable）的证明时，仍然存在较大困难。

我们提出 LEAP，一个智能体化（agentic）的框架，使通用基础模型（general-purpose foundation models）能够在自动形式化定理证明（automated formal theorem proving）任务上达到当前最先进（state-of-the-art）的性能。

LEAP 充分利用了基础模型已有的能力，包括：

• 非形式化数学推理（informal reasoning）；

• 指令遵循（instruction following）；

• 迭代式自我改进（iterative self-refinement）。

通过将复杂证明任务拆解为多个较小的子问题，LEAP 在 Lean 编译器的持续交互反馈下，将形式化证明的构造过程与非形式化证明思路（informal blueprints）有效衔接，从而逐步完成形式化证明。

为了突破现有基准逐渐趋于饱和的问题，我们进一步提出了 Lean-IMO-Bench，一个由 Lean 形式化表示的国际数学奥林匹克（IMO）风格题目组成的新基准。该基准中的题目虽然题干较短，但证明过程高度非套路化（non-routine），通常包含多个推理步骤，并覆盖了广泛的难度范围，因此能够更严格地评估形式化证明能力。

实验结果表明，在 2025 年 Putnam 数学竞赛（北美本科生年度数学竞赛）上，LEAP 成功解决了全部 12 道题目，与近期前沿形式化数学模型取得的突破性成果相当。

在 Lean-IMO-Bench 上，LEAP 更显著提升了通用大语言模型的一次性形式化证明成功率（one-shot formal solve rate）：由不足 10% 提升至 70%，明显超过了此前由一个专门面向 IMO、达到金牌水平的系统所创造的 48% 基准成绩。

此外，我们还展示了 LEAP 在数学研究中的实际应用价值。该系统能够自主完成复杂证明的形式化工作，用于解决开放性的组合数学问题。其中包括为 Knuth 关于偶数阶 Cayley 图哈密顿分解（Hamiltonian decomposition of even-order Cayley graphs）中的一个关键子问题，自动构造并验证了一份形式化证明。

这些结果表明，LEAP 不仅显著提升了通用大语言模型的形式化证明能力，也展示了其作为数学研究辅助工具在前沿科研中的潜力。

原文链接：https://arxiv.org/abs/2606.03303