论文精读：不重训模型的两种极致——EASYPROVER 把 Lean 证明基础设施推到基准饱和，TokenEconomizer 把经验复用做成外挂成本控制器

一、引言：当模型不动时，工程还能走多远

过去两年，大语言模型（LLM）能力提升的主叙事几乎总与训练挂钩：更大的预训练语料、更精的强化学习配方、更贵的专家迭代。每一次模型换代，开发者都在追问同一个问题：除了等下一代模型，我们还能做什么？但 2026 年 10 月底出现的两篇论文，从两个截然不同的方向给出了同一个反叙事：在不重训模型的前提下，纯粹的工程杠杆仍然有巨大的、且远未被穷尽的空间。

第一篇是 Amazon Web Services 与 Case Western Reserve University 合作的形式化验证工作（一作 Debargha Ganguly 在 AWS 实习期间完成，作者群含 AWS Automated Reasoning 团队的 Soonho Kong、Aaron Tomb、Aman Goel 等） Scaling Lean Theorem Proving for Real-World Code Verification。它推出的 EASYPROVER 系统用现成前沿模型（off-the-shelf frontier model）加上一套精心设计的递归智能体运行时，不做任何微调、不训练任何策略或价值网络，就把 PutnamBench 打到 669/672、把 VERINA 打到 189/189 饱和；更关键的是，它用 AEGIS 数据管线自动生成了 11,533 条带内核检验标签的新任务，让同一个近乎饱和现有基准的证明器只能解出其中 52.7%，为整个领域重新划出了难度天花板。

第二篇是 UC Berkeley 与 Microsoft Research、Microsoft Security 合作的（一作 Aaron J. Li 在微软研究院实习期间完成） TokenEconomizer: Experience-Driven Black-Box Cost Control for Coding Agents。它面对的是商用编码智能体（coding agent）——把前沿模型与工具使用 harness 打包成 Claude Code、Codex、GitHub Copilot CLI 这类产品——的 token 成本问题：不改模型权重、不改智能体循环代码，只做一个外挂控制器（external controller），从已完成任务的轨迹中学习仓库级策略，就在三款商用智能体、五个智能体-模型设置上实现 18.4-30.9% 的平均降本，且 Pass@1 四升一平——这条路线对任何按 token 付费的企业用户都直接可部署。

两篇论文一个做「能力的极限」，一个做「成本的极限」，表面上毫无交集，底层却共享三条假设：

其一，前沿模型本身已经足够强，瓶颈在模型外围的系统设计——证明搜索的上下文管理、算力的弹性供给，或者任务流之间的经验组织。两篇论文分别在不同领域把这一假设变成了可检验的事实；

其二，验证信号比模型输出更可信——Lean 内核的检验、正则检测器对轨迹的复核，都让系统不需要相信模型的自述；

其三，可复现的数值比叙事更有说服力——每一条主张都锚定在可复核的度量上（内核检验的证明、全额入账的配对成本），而不是示范性样例。

第一篇的贡献可以概括为两条：(1) 一个近乎饱和当前基准的证明系统——EASYPROVER 组合递归隔离上下文智能体、异步搜索、并行 tactic 探测与 INFINILEAN 弹性推导服务，用现成前沿模型、零额外训练解出 PutnamBench 669/672、IMO 2026 全部 6 题、NTP4VC 597/600、VERINA 全部 189 题（证明或反驳），每个报告结果都是内核检验的；(2) 一个更难的验证测试集——AEGIS 产出 2,045 个差分验证的 Rust-Lean 程序对与 11,533 条候选规格，EASYPROVER 在 2,000 条抽样上 30 分钟预算内证明 1,054 条（52.7%），证明率从 Easy 的 66.7% 降到 Hard 的 37.6%——任务远离饱和，且因管线无需专家标注，加算力即可再生成，同一任务还可用于评测其他证明器或充当 RLVR 奖励。

第二篇的贡献同样三条：(1) 把编码智能体成本优化形式化为任务序列上的问题，定义了含控制器开销的累积端到端核算协议，并用成本画像识别出固定策略的仓库依赖效应与三个可行动的余量来源；(2) 提出 TokenEconomizer 外挂控制器，从完成轨迹学习微技能激活、工具剪枝、失败循环干预三条元策略的环境特异策略；(3) 跨三个主流编码智能体、四个基准、579 个任务验证降本在每个设置下成立且任务成功率相当。三项贡献构成完整闭环：先定义问题与度量、再给方法、最后跨域验证。

值得一先点破的是两篇论文最有趣的对称：EASYPROVER 证明「不加训练也能逼近能力天花板」，TokenEconomizer 证明「不动模型也能逼近成本地板」。天花板与地板之间的整个区间，就是工程的主场——也是本篇精读要带读者走一遍的地图。

两篇论文的发表时间也值得一提：EASYPROVER 于 2026 年 10 月 28 日提交 arXiv（2610.38174），TokenEconomizer 于 2026 年 10 月 15 日提交（2610.22732），相隔不到两周——这种时间上的耦合并非偶然，它反映了社区对「训练之外的空间」的注意力正在快速聚集。

把这两篇放在一起读，能看到一条完整的 training-free 路线光谱：一端是基础设施规模化（用递归并行与弹性算力换取搜索宽度），另一端是经验资产化（用轨迹沉淀与门控复用换取成本削减）。本篇精读将分别拆解两者，再合评这条路线的深层逻辑。

二、EASYPROVER 与 AEGIS：把 Lean 定理证明推到基准饱和

📄 原文链接

2.1 背景：证明器跑赢了基准

LLM 加证明助手（proof assistant）的组合已经能产出竞赛数学与程序正确性的机器检验证明。但「能产出」与「能稳定产出」之间隔着系统设计的鸿沟——同一模型接不同 harness 的成绩差异，往往大于不同模型接同一 harness 的差异。但搭建一个有效的证明智能体，远不止「一个前沿模型加一个证明检查器」：智能体必须分解目标、寻找或证明中间引理、从失败的路径中恢复，而这一切都发生在有限的上下文窗口和算力预算内。更麻烦的是，Lean 的验证器反馈是局部的——它告诉你每一步能否通过推导（elaboration），但一个糟糕分解的代价可能要到很多步之后才显现。

与此同时，评测本身出现了危机。多个形式化推理基准已经接近饱和（miniF2F 上已有系统报告 100%），而现有的验证式编程基准又太小——每个验证任务都需要程序行为的形式化陈述、程序模型和有意义的证明义务（proof obligation），撰写这些需要编程、形式规约与定理证明三重专家知识，导致现有基准只有几百条任务（VERINA 189 条、CLEVER 161 条、AlgoVeri 77 条、DafnyBench 亦是百级）。小而静态的基准还面临记忆化与数据污染（contamination）的暴露。

评测一个证明智能体，需要它解不了的任务；评测一个即将饱和所有基准的智能体，需要一个能不断再生的任务源。自动生成验证任务可以同时解决两个问题——前提是规格能捕捉预期行为、证明难度有梯度分布。

这两重困难在数学证明与程序验证上形态不同。数学证明依赖选对抽象、分层搭建辅助引理；程序验证则额外叠加递归程序结构、数据表示、不变量与实现级证明义务。已有基准又各自带伤：miniF2F、PutnamBench 覆盖奥数数学，VERINA、CLEVER、AlgoVeri 与工业级 NTP4VC 套件覆盖已验证代码，但都是静态的——现有缓解手段（新前提分割、n 元组重叠审计、发布日期截断）只能检测或限制固定任务集内的污染，不能产出新任务。而测试只给有限正确性证据，用作训练奖励时会诱导智能体利用测试装置而非实现预期行为；证明则针对形式规格认证正确性且检验廉价——内核检验标签因此可直接用作可验证奖励强化学习（RLVR）的奖励。

于是这篇论文做了两件事：先造一个近乎饱和现有基准的证明器，再造一个让它饱和不了的测试集。

2.2 定位：无训练的递归证明运行时

EASYPROVER 的定位选择非常鲜明。相关工作里，Goedel-Prover-V2、DeepSeek-Prover-V2、Seed-Prover 等主流系统都依赖精选证明语料上的训练、专家迭代（expert iteration）或强化学习；Goedel-Code-Prover 训练策略把验证目标归约为内核检验的引理。EASYPROVER 明确不训练、不微调，使用现成的 Anthropic Fable-5 模型，没有单独训练的策略网络或价值网络，也没有额外的私有证明语料——神经定理证明社区多年积累的「步进生成 + 前提选择 + A*/MCTS 搜索」范式，在这里被整体替换为「整段证明的递归智能体搜索」。

它的搜索与蒙特卡洛树搜索（MCTS）松散类比，但有一个本质区别：父智能体直接读取子智能体返回的内容（完成的证明、反例或部分发现），基于内容做继续、修订或扩展的决策，而不是维护基于访问次数或 rollout 的平均价值估计——用语言模型的内容理解替代统计价值函数。每个智能体跑一个 ReAct 式循环，交替模型调用与工具调用，Lean 工具经模型上下文协议（MCP）暴露——递归委派的对象不是模板化的子程序，而是与父辈同构的完整智能体。

与近邻工作的边界。 证明搜索面上，前文已列训练系证明器。数据面上，AEGIS 与三类前驱划清界限：自博弈证明器（STP）、内在动机猜想器与执行打分的推理器都让同一模型既出题又解题，而 AEGIS 把任务生成与求解分开，并给每条冻结语句标注内核检验的证明或其否定的证明——反驳提供负标签，这是只产证明或只靠执行打分的闭环都不提供的；语句与信任策略一旦固定，任何人都可复核标签。自动形式化（autoformalization）把非正式数学陈述映射为形式陈述，AEGIS 的规格智能体做的是一种特化的自动形式化——把自然语言编程题变成关于提取程序本身的 Lean 语句；每条标签对该程序正确，即使翻译不完美亦然（差分验证另行提供 Lean 程序行为似 Rust 源的证据）。防作弊上，Leanstral 会在证明失败时转而尝试证否、DeepSeek-Prover 用并行反驳筛选语句，而 EASYPROVER 把「证明或反驳」作为一等任务设定，并用冻结前缀、Lean Comparator 与公理白名单系统性封堵削弱语句、留 sorry、引入公理三类作弊。

2.3 问题定义：内核检验的双极判定

问题形式化非常干净。每个任务固定一个 Lean 4 环境 Γ 和一个命题 P，目标是要么证出 P、要么证出其否定 ¬P 的内核检验证明（kernel-checked proof）——对数学任务与程序验证任务同样适用。文件前缀（包括目标定理签名）被冻结，只有证明体可以改动。一个完成的证明被接受，当且仅当它通过 Lean Comparator 的独立检查——用共享的只读工具链运行 lake env lean 与 #print axioms，且不依赖搜索期间的语言服务器。智能体自己报告的成功、或某次局部 tactic 探测的成功，都不算数。任何人持有相同环境与公理策略都能复核被接受的证明：其保证锚定在冻结语句、允许的公理与 Lean 内核三件事上。

这个「证明或反驳」（proof or refutation）的双极设定贯穿全文：它既让任务判定更完整（反例也是有效解），也为后续训练数据提供了罕见的负标签。

在系统接口层面，现有 Lean 智能体接口（从 LeanDojo 到 lean-lsp-mcp）都在智能体同机上运行 Lean、以本地文件路径引用证明，因此每个证明器绑定单一 Lean 服务器；提示词库（如 lean4-skills）则为这类智能体打包 Lean 专业知识。INFINILEAN 的无状态服务化正是针对这一约束：客户端经网络发送 Lean 源码，负载均衡池中任何就绪副本可查任何证明——证明检查从「进程内依赖」变成「网络服务」。

2.4 解法：四个工程组件的组合拳

架构上，EASYPROVER 把三件事彻底分开：证明搜索（图 1）、交互式 Lean 推导（图 3）、以及最终证明验证——搜索可以大胆试错，因为接受口径握在第三方的手里。智能体通过递归委派与并行 tactic 探测探索证明策略，INFINILEAN 独立于智能体执行地服务推导请求。整个异步智能体运行时采用 ReAct 式循环——模型响应与编码及 Lean 工具调用交替进行，工具经模型上下文协议（Model Context Protocol, MCP）暴露；API 轮数上限与墙上时钟截止约束执行，提示词缓存（prompt caching）与紧凑工具响应压缩 token 与通信开销。

递归子智能体与上下文隔离。 父智能体启动子智能体去探索备选证明策略或辅助引理；每个子智能体获得全新的上下文、项目私有副本，以及与父辈相同的完整工具集（包括继续派生的 Agent 工具），因此委派可以递归。子智能体只返回完成的证明、反例或部分发现——一个子智能体可能花几十次工具调用推导出一条辅助引理，但父智能体只收到引理本身，失败的尝试与诊断不会污染父辈上下文。

上下文隔离把全树的探索总量与任何单个智能体必须保留的历史解耦，这是系统能在单次运行中跑起 300 多个子智能体的前提。异步返回则保证早到的发现不被晚到的分支拖住：一个子智能体找到反例，父辈下一回合就能砍掉整个子树。已完成的子任务结果在父智能体的下一个回合即返回，不必等待未完成的兄弟分支，早期发现可以实时重定向搜索方向。与 UCT 式 MCTS 的对照在这里再次显形：UCT 用统计规则选节点扩展、用随机 rollout 的平均回报更新节点价值；EASYPROVER 的父智能体拿到的是每个子智能体返回结果的内容本身——完成的证明、反例或部分发现——由语言模型读懂内容后决定继续、修订或扩展。这本质上是把价值函数外包给语言模型的世界知识：一条「此路有反例」的返回比任何数值估值都更能剪枝。

并发规模由资源准入控制兜底：两个进程级信号量分别把活跃子智能体上限设为 64、并发昂贵 Lean 查询上限设为 16，每个 harness 进程独立限制智能体执行与 Lean 负载。候选证明在锁保护下从分支工作区晋升到解文件，harness 对晋升文件重新做构建与接受标准检查、失败即回滚；第一个被接受的候选终止整个搜索。

并行 tactic 探测。 在单次证明尝试内部，tactic 探测器通过 Lean 语言服务器与自动化 worker 并发运行多个候选 tactic 与自动化推理工具；某个候选成功时，探测器只返回那条 tactic，丢弃所有失败探测的轨迹——智能体因此可以尝试许多局部续写而不必把每条探测轨迹塞进自己的上下文。论文给了一个直观的数字：返回的 tactic 约 30 token，而被丢弃的探测轨迹总计约 30,000 token——一千倍的上下文压缩，且这一比率完全来自「只上交成功」的信息过滤策略。

INFINILEAN 无状态弹性推导服务。 现有 Lean 接口（LeanDojo、lean-lsp-mcp 等）让 Lean 与智能体跑在同一台机器上、以本地文件路径引用证明，因此每个证明器绑定单一 Lean 服务器——搜索宽度受单机容量封顶。INFINILEAN 反其道而行：一个无状态服务，客户端通过 JSON-RPC 直接发送 Lean 源码，负载均衡池中任何就绪副本（预装固定 Lean 与 Mathlib 版本）都能服务任何请求——任何副本查任何证明。

每个副本组合了三样东西：Lean 语言服务器 MCP 接口、临时工作区、预载 Mathlib 的 REPL worker 池。复用 worker 摊销了导入成本：冷启动导入需要数十秒，而热 worker 上的推导只需约 0.2 秒——两个数量级的差距。副本跑在 Kubernetes 上，目标追踪自动扩缩容（target-tracking autoscaling）按需调整数量；搜索期间的交互推导与最终接受检查（由 Lean Comparator 独立执行）彻底分离。这是把「证明检查」从进程内库变成云原生微服务的完整工程：无状态换来了水平扩展，预热换来了低延迟，版本锁定换来了可复现。

AEGIS 数据管线。 论文的第二贡献是把竞赛编程题转化为「真实实现之上的 Lean 验证任务」。数据表示经过精心设计以同时落进两种语言：字符串变 ASCII 字节数组、矩阵是所有权行的向量、图保留边表输入、树与链表用所有权递归枚举（Box 包装在翻译中消失、得到 Lean 归纳类型）；每个结构化输入只解析一次、渲染为匹配的 Rust 与 Lean 字面量；整数、序列长度与测试集规模都有界以保 Lean 求值可行；少量浮点题用容差输出比较。

编码智能体对 LeetCode 题目写安全 Rust（safe Rust）解，保留单纯函数、一阶数据（整数、布尔、列表、嵌套列表、字符串、树、链表）等管线可支持的接口，排除有状态或基于类的接口及哈希表、闭包、嵌套引用、无限制别名等不支持特性。随后是五级流水线式的差分验证（differential validation）：cargo test 跑全部保留参考用例，CHARON 提取 Rust 程序，AENEAS 把它翻译为可执行的 Lean 函数式模型，Lean 在相同输入上求值模型，逐对比较 Rust 与 Lean 输出——一个实现被接受当且仅当全部参考测试通过且每个输出匹配。2,356 道尝试的题目中 2,045 道（86.8%）通过全部阶段（Rust 测试、提取、翻译、Lean 推导、差分求值）。随后规格智能体（specification agent）为每个程序实例撰写性质：它收到原题、完整提取的 Lean 程序、其签名与若干差分验证的示例，用 Lean 语言服务器工具撰写关于该程序、能通过推导的定理语句（证明体留 sorry）配自然语言描述——请求的性质涵盖功能正确性、完全性、输出边界与形状、边界情形、关系性行为等「应成立」类，以及缺失前置条件或差一界等「应失败」类；语句经去重、剔除平凡或空洞断言与推导错误后被冻结，交由证明智能体证明或反驳。论文防 reward hacking 的组织学设计在于：写语句的智能体先于且独立于解题的智能体，证明器无法挑一个更简单的命题来证；语句冻结后，任务的难度就锁死了。防作弊设计有三重：语句前缀冻结使证明器无法偷换更简单的命题；Lean Comparator 要求编译无 sorry 且公理闭包在白名单内；AEGIS 中写语句与解语句是不同的智能体。可选的反例筛选（Plausible 属性测试）在证明搜索前抓起草错误——对可判定命题采样具体输入，找到的反例进入同一证明或反驳管线且只在 Lean 检查后才计为反驳——但筛选不产生正标签。

证明结果与奖励。 EASYPROVER 尝试在不改变语句的前提下证明 P 或 ¬P；只要证明或反驳在任务的信任策略下通过接受检查，任务即算解决——无论规格被要求成立还是失败。同一结果同时校验规格：证明确认「应成立」的规格，反驳确认「应失败」的规格，相反结果标记极性不匹配；未解任务不给信号。当 AEGIS 用作 RLVR 环境时，这些结果直接作为证明器与规格智能体的奖励——实现检查奖励编码智能体、内核检验结果奖励规格与证明智能体。管线还支持变异测试（mutation testing）：对已验证程序的小编辑产生貌似合理但不正确的变体，其规格产生更多负标签（论文生成了这类任务但未评估）。

2.5 实验证据：饱和与不饱和的双面结果

报告协议。 计数一个证明当且仅当：目标语句未变、文件编译无 sorry、目标的公理闭包在基准白名单内；内核检验的否定证明计为反驳。以下所有数字都经此口径。对比时须注意设置差异：部分基线报告的是 proved（只计证明）、部分是 resolved（证明或反驳），EASYPROVER 报告 resolved 且 pass@k 为 1。

形式数学。 EASYPROVER 单次运行解出 PutnamBench 669/672（99.6%），比 Chung et al. 报告的最强自然语言引导配置（597/672）多 72 题；同时解出 IMO 2026 全部 6 道形式化题目、Putnam 2025 全部 12 题、miniF2F 99.6%。把表 1 的对比基线完整铺开更能看出这个位置的意义：Goedel-Prover-V2 在 PutnamBench 上是 13.0%（@184 尝试预算）；LongCat-Flash-Prover 97.1% miniF2F、41.5% PutnamBench；Seed-Prover 初版 50.4%（657 题）、后续 87.9%（660 题）；Hilbert 递归证明系统 70.0%（@1840）；Chung et al. 的蓝图生成与精化管线加自然语言引导达到 88.8%（@4）并拿下 IMO 2025 的 4/6 与 USAMO 2026 的 3/6；PutnamBench 官方榜单与 Zhang et al. 报告了 100%，Axiom Math 与 Zhang et al. 各自报告 IMO 2026 6/6。

EASYPROVER 的独特之处在于：这些结果全部来自单次运行（one run）、无训练、无尝试预算堆叠，且在 IMO 2025 与 USAMO 2026 两列留空（未评估）、只报其他系统的已发表数字——克制本身即口径。论文对污染（contamination）的诚实值得注意：模型训练截止未公开，无法排除竞赛题非正式解出现在训练数据中的可能——但这只影响结果解读，不影响正确性，因为每个被接受的证明都经内核检验；而 AEGIS 的语句由管线生成、在本工作之前不存在，天然免疫这一问题。这一区分（「结果可信」与「能力解读可信」的分离）是处理所有近饱和基准报告的规范姿势。

代码验证。 如果说数学基准的成绩还可能被训练污染稀释，代码验证基准则更接近真实工程义务。把表 2 的基线铺开：Li et al. 评测的通用 LLM 在 pass@128 下 VERINA 只有 10.6-19.6%、CLEVER 11.2-23.6%、AlgoVeri 5.2-18.2%；神经证明器（Goedel-Prover 等）在同一预算下 VERINA 15.9-24.3%、AlgoVeri 19.5-23.4%；Li et al. 自己的层级搜索（pass@32）把 VERINA 拉到 68.8%、CLEVER 54.0%、AlgoVeri 62.3%；Xu et al. 的通用 LLM 在 NTP4VC 上 pass@8 仅 0.00-1.67%、专用证明器 2.17-3.00%；Harmonic 报告 VERINA proved 160/189（84.7%）、resolved 183/189（96.8%）；Logical Intelligence 报告 100%。EASYPROVER 单次运行 resolved：VERINA 189/189、AlgoVeri 77/77 全部解决；NTP4VC 597/600（99.5%，其中 588 个证明、9 个反驳——9 个验证条件本身不成立，以内核检验的反驳解决）；CLEVER 上解决可翻译到 Lean 4.32 工具链的 143 道任务中的 113 道（79.0%，161 题全集的 70.2%，其余 18 题无法翻译到该工具链）。与最强报告持平或超出，且全部为单次运行、无尝试预算。图 5 另给出 NTP4VC 每个已解任务的时间与成本分布（对 588 个证明与 9 个反驳分别归一化）及证明成本与时间按子智能体使用的分组——resolved 口径下逐任务的算力账单是公开的。

AEGIS 上的不饱和——这是全文最重要的数字。 从 11,533 条候选规格中按 LeetCode 难度与规格类别分层抽样 2,000 条（覆盖 1,257 个翻译程序；排除已被 Plausible 反例筛选驳回的语句与「要求失败」类别），每条 30 分钟预算：EASYPROVER 尝试 1,997 条（3 条因故未跑），证明 1,054 条（52.7%），943 条未解。按规格类别，边界情形（edge case）证明率最高 84.1%，显式契约（explicit contracts）最低仅 31.0%；按 LeetCode 难度，Easy 66.7%、Hard 37.6%——难度与义务密度都清晰地传导到了证明率。同一个近乎饱和所有现有基准的证明器，在新任务上留下接近一半的未解空间——这正是论文想要的结果：基准的价值不在被解出，而在区分。

证明规模与案例研究。 附录 A 到 I 给出 7 个完整案例（含全部 Rust 源码、AENEAS 生成的 Lean 定义与被接受的证明），这是论文最「实」的部分：Rust 源码 19-67 行，AENEAS 翻译 83-387 行，被接受的证明 289-1,167 行；1,054 份证明合计 145,646 物理行，中位数 104 行，最大 1,167 行。每份计数包含注释、数学模型、辅助引理、循环不变量、连接生成代码与模型的引理以及目标证明——支撑性定义与引理本身就是提交的验证开发的一部分。

翻译引入的义务在案例里纤毫毕现：每个 Rust 循环被拆成返回 Result (ControlFlow σ α) 的循环体（cont 携带下一循环状态、done 携带最终结果）加一个用 AENEAS 循环组合子构建的驱动器，嵌套循环生成更多组件；index_mut 返回当前元素连同重建更新后向量的后向函数（backward function），一次源码级 swap 变成数个单子更新步骤；定宽值如 Std.U32、Std.I64 暴露 .val 数学投影，算术与宽度转换（cast）引入显式范围义务——证明「完全性」（totality）需要证明失败分支不可达，即使失败在数学上不可能发生。

偶奇位独立排序案例中，被冻结的定理只主张输出长度与输入相等，但最弱前置条件（weakest-precondition）判断 f x {| v => Q v |} 断言计算以 ok v 终止且 Q(v) 成立——后置条件为 True 仍能证明完全性，因为失败与发散都不满足该判断；即便如此，证明仍须自底向上建立五层规格：拆分循环的精确长度不变量（处理 i 个位置后两个临时长度恰为 (i+1)/2 与 i/2）、两个内层选择排序循环的长度保持、外层循环的提升、发射循环连接游标与结果长度及奇偶游标的四分量不变量，最后组合出顶层函数的完全性与精确输出长度。唯一未解的自底向上归并排序案例（附录 H）最能说明难度的来源：连「非空且至多 50,000 元素前置条件下的纯完全性」定理都因八个循环与耦合游标界而搁浅——冻结定理的注释细致论证了所有访问在界内、所有 Usize 计算远离 2^64-1、元素值无算术、每个循环严格单调有界，直觉上「显然成立」，但耦合不变量的组合复杂度仍压垮了 30 分钟预算。这正是「实现级义务」的典型形态：数学内容平凡、证明工程量不平凡。附录 I 归纳了跨案例的五类重复义务：弱后置条件、输入边界、可变性、关系性定理（连接两次独立执行）、完全性——大部分证明长度花在把数学主张连接到具体表示与生成控制流的安全执行上（三角和与对角线案例中，目标定理及其证明只占最后 25 与 38 行）。

2.6 根源解释：为什么这套工程能赢

拆开看，EASYPROVER 的优势不来自任何单点创新，而来自四个乘法因子——每个因子都是一次「解耦」：把一件事从另一件事的约束里解放出来。四个因子相乘，才有无训练系统对训练系统的全面反超。

因子一：上下文隔离解耦搜索宽度与上下文深度。 递归委派让全树探索不再受单个智能体上下文窗口限制；每个子智能体的失败历史被就地掩埋，只把结晶后的引理或反例上交。这与 MCTS 用统计平均压缩信息不同——语言模型能读懂「这是一个完成的证明」与「这是一个反例」的内容差异，从而做出比访问计数更聪明的分支决策。论文用一句话点破这类比：搜索结构像 MCTS，但节点值更新靠的是返回结果的内容，而非 rollout 回报的平均。

因子二：无状态推导服务解耦搜索规模与单机容量。 最难的证明单次运行用了 300 多个子智能体，其推导需求远超单机 Lean 容量；INFINILEAN 把推导变成可水平扩缩的云服务——请求经 JSON-RPC 直接携带 Lean 源码、Kubernetes 上按需目标追踪扩缩副本数、每副本带临时工作区与预载 Mathlib 的 REPL worker 池——热 worker 0.2 秒对冷导入数十秒的差距，让「试错一万次、只留一次」的搜索策略在经济上成立。而最终接受仍由独立的 Lean Comparator 在共享只读工具链上复核，与服务化推导互不干扰。 因子三：双极标签解耦任务生成与专家标注。 AEGIS 不需要人类写任务：任务从公共竞赛题自动翻译生成，标签由内核检验的证明或反驳自动产生，负标签（反驳）是只产证明或只靠执行打分的自博弈系统都不提供的。管线无需专家标注，加算力即可生成更多任务；变异测试还能从已验证程序派生貌似合理但不正确的变体、产生更多负标签（生成了但未评估）。

因子四：接受协议重建信任模型。 证明搜索期间的任何信号（智能体自述成功、局部 tactic 探测通过、语言服务器的即时反馈）都不构成接受；唯一口径是冻结语句 + 独立工具链上的 Lean Comparator 复核 + 公理白名单。这个信任模型让「谁都能复核」成为系统性质：同一环境与公理策略下任何人可重查被接受的证明。对一切声称「可验证」的系统而言，这一条是分水岭——可验证性必须是系统属性，而不是演示属性。

2.7 知识反推：我们能从数据里读出什么

从这些结果可以反推出几条关于「模型已封装能力」的知识：

其一，前沿模型内部已经储备了足够解 Putnam 级数学与真实代码验证的知识，缺的是组织这些知识的搜索结构与消化失败的上下文经济学——一旦失败可以被隔离与掩埋，模型的知识就能被完整兑现。无训练系统在 AEGIS 上仍有 52.7% 的证明率，说明即便面对从未见过的实现级义务，模型的可组合推理也远未枯竭；反过来，未解的 943 条则标注了纯搜索路线的知识盲区边界。

其二，「证明或反驳」的判定比「证明」更贴近验证的本质：NTP4VC 上 9 个任务以反驳解决，说明部分验证条件本身就不成立；只统计证明的系统会低估可解率——这一观察对一切「验证条件由人写定」的工业验证场景（验证条件本身可能有 bug）都有直接警示意义。 其三，拒绝作弊的语句冻结机制反过来界定了「解决」的语义：PutnamBench 榜单上一些 100% 报告或许经不起「冻结前缀 + 无 sorry + 公理白名单」口径的复检——论文没有点名，但口径本身就是对排行榜文化的温和纠偏。

其四，现有基准的难度与真实代码验证的难度之间存在结构性断层：数学函数的证明义务是「选择正确的抽象」，而翻译后的真实实现叠加了定宽算术、显式失败、生成循环、类型转换与函数化的可变性（functionalized mutation）五层实现级义务——52.7% 对 99.6% 的落差度量了这个断层。案例研究把这个断层落到地面：6 个已解案例的 Rust 源码只有 19-67 行，被接受的证明却是其 4-17 倍长（289-1,167 行），多出的部分几乎全部服务于「数学上显然、工程上繁琐」的安全执行论证。

未做与未来。 论文明确列出留白：不消融 harness 的单个组件（每个配置需全基准重跑，代价过高），特别是没有对比「同模型把 Lean 当工具而无 harness」的裸基线；在 AEGIS 上评测其他证明器、把 AEGIS 用于强化学习与多教师在线蒸馏（multi-teacher on-policy distillation）均留作未来工作。

2.8 通用灵感：超出定理证明的启示

• 把昂贵检查器做成无状态服务是所有「LLM 高频试错 + 高成本验证器」场景的通用模式：任何可以脱离会话状态运行的检查（编译、测试、仿真、求解器）都值得微服务化、池化与预热，使试错成本与检查延迟解耦。判断标准很简单：如果验证器冷启动成本高于单次检查成本的两个数量级（如 Lean 的数十秒导入对 0.2 秒推导），预热池化就是净赚。
• 冻结命题、独立复核、白名单公理的接受协议，是所有「智能体可能作弊」场景的模板：不让执行者自己宣布成功，用独立通道按既定标准复核，且标准（允许的公理）显式声明。值得注意的是这套协议直接对应三类已知作弊手法——削弱定理语句、留下 sorry、引入投机公理——每类各有一道闸门，防的是具体漏洞而非抽象的「不诚信」。
• 自动生成任务 + 双极标签为可验证奖励的强化学习（RLVR）提供了可持续的数据源：任务生成与求解分离、语句冻结先于证明、负标签自动获得，这三点共同防止了智能体通过弱化任务来骗取奖励（reward hacking）。对训练团队的现实意义是：数据预算可以从「雇专家写任务」转向「租算力跑管线」，边际成本随规模递减。
• 反例是第一公民。 把「证伪」与「证明」放在同一接受级别，不仅让 9 个不成立的 NTP4VC 验证条件被正确解决，也让 AEGIS 能产出「应失败」规格的负标签。任何构建训练或评测环境的系统都值得问一句：我的标签体系里，反驳值多少？
• 翻译不完美不挡验证。 AEGIS 的每条语句都关于提取出的 Lean 程序本身，因此标签对该程序无条件正确——差分验证另行（而非同时）保证 Lean 程序行为似 Rust 源。把「语义保真」与「逻辑正确」拆成两个独立可验证的命题，是自动化管线里对付不完美组件的通用架构手法。
• 论文公开承认未做组件消融（每个配置需要全基准重跑），也没有对比「同模型直接用 Lean 工具无 harness」的基线——这两个空缺恰好是后续工作的入口。

三、TokenEconomizer：把经验复用做成外挂成本控制器

📄 原文链接 | 代码链接

3.1 背景：孤立任务评测与连续开发现实的错位

前沿编码智能体（Claude Code、Codex、GitHub Copilot CLI）的能力以高昂的 token 成本为代价：每一轮计费都包含持久的系统与工具前缀（prefix）加上不断膨胀的交互历史，早先的内容在轨迹中被反复计费——缓存折扣了回放上下文但并未消除其成本。这意味着轨迹成本近似随轮数的平方增长，长轨迹的边际成本远高于短轨迹。而 token 效率的研究几乎都在孤立任务层面进行——模型级的降推理力度（reasoning effort）省 token 但掉成功率，harness 级的工具配置与辅助指令需要手工调整，轨迹压缩、观察过滤等更定向的方法需要改智能体循环或引入训练组件。更重要的是，任务内优化忽略了软件开发的连续性：真实开发者在同一个演进中的代码库里持续构建、更新与维护，同一环境内的已完成执行，本应为后续任务提供可复用的经验。社区其实已开始响应这一错位——SWE-Bench-CL 评测持续修复、SWE Context Bench 评测上下文学习、AgentStream 评测流式任务——但经验复用侧的方法（语言课程、工作流记忆、可执行技能库、技能自演化）大多不经由智能体暴露的接口行动，或者不加区分地注入仓库上下文（已有研究指出无区分的仓库上下文可能升成本而不升成功率）。这留下了一个清晰空位：通过商用智能体现有接口、且按证据选择性复用经验的成本控制器。

论文的先导实验（cost profiling）很能说明问题：在 60 个 SWE-Bench 任务（6 仓库各 10 题，Claude Code + Opus 4.8 高推理力度，回顾式分析）上测试三种流行开源插件式固定策略——RTK v0.45.0（作为 shell 工具的预执行 hook 改写命令以压缩输出）、Serena（语言服务器支撑的 MCP 符号级导航）、RepoMap（Aider 仓库地图，按交叉引用图中心度排序并在 2,048 token 预算内渲染签名、每任务生成一次作为项目指令注入）——没有一种能在所有仓库上一致降本。

具体数字（表 3）：三者都在 Django 上降本（RTK -19.9%、Serena -15.4%、RepoMap -16.2%）、都在 SymPy 上升本（+7.3%、+30.8%、+9.8%）；scikit-learn 上只有 RTK 降（-6.9%）而 Serena +28.6%、RepoMap +30.5%；Sphinx 上只有 RepoMap 降（-7.5%）；xarray 上 RTK -16.8% 但 Serena +4.7%。固定策略在不同仓库上的效果方向都不一致，且 Serena 是唯一汇总升本的策略（这也解释了主实验为何排除它——工具剪枝可能移除其未用的服务器、混淆对比）。

与此同时，默认轨迹暴露了三个可削减成本的来源：

1. 操作知识被反复重新发现：动作以键归约（shell 命令小写化、折叠空白、去前导目录变换、只取前 6 个 token；文件工具取工具名加文件基名）后统计——在一个仓库中至少半数任务里重复出现的动作，占其工具调用收发字节的 12-28%；与更早任务重复的调用比例从第 2-3 个任务的 14% 上升到有 5 个前序任务后的 30%；而对照另一个仓库的完整历史只匹配 7%（且主要是通用 setup 与测试命令）——重复是仓库特异的，不是通用命令的巧合。
2. 多数加载的工具从未被调用：智能体每轮看到 23 个工具 schema（每个仓库完全相同的目录），但没有仓库调用超过 7 个；16 个工具从未被调用，3 个工具（Bash、Read、Edit）占全部调用的 98%，其余工具跨仓库稀疏而参差地使用。固定的精简接口固然能移除共享开销，但也会压制个别仓库局部有用的工具——这正是「基于证据的可恢复剪枝」的动机。
3. 失败轨迹消耗不成比例的成本：10 个失败执行占任务的 17%，却占总花费的 32%；45 条轨迹重复了更早的失败签名（归一化的失败输出首行错误），60 个任务 51% 的花费落在首次重复之后——但重复不等于失败（50 个成功运行中 36 个也有重复签名、重复后花费的大半落在最终成功的运行里）；仓库差异也很大（Matplotlib 失败 45 轮 vs 成功 20 轮，Sphinx 失败 36 轮 vs 成功 31 轮），一刀切的轮数上限无法区分，守卫必须把当前运行长度与该仓库成功运行的分布对比、且应在终止前先尝试重定向。

3.2 定位：黑盒外挂控制器

TokenEconomizer 的定位是「经验驱动的黑盒成本控制器」：它把智能体当作黑盒，只通过其暴露的提示词设置、工具配置与事件流行动，监控执行事件，不改模型权重也不改智能体循环代码。这一选择让它可以即插即用地跟随智能体升级——模型换代、harness 更新都不需要重新适配内核，也不需要模型访问权或重训练。

与之对照，此前的成本控制方法分两大阵营，各有缺口：轨迹内方法做上下文压缩（提示词压缩、shell 输出压缩、工具观察剪枝、轨迹缩减）、检索收窄（仓库地图、代码知识图谱、结构感知侦察、训练式检索智能体）或接口限制（工具限制与检索、接口增强、极简实现插件）；模型级方法做级联与路由。前者固定且任务局部（效果随仓库漂移，本文的成本画像正是证据），后者在每个查询上以质量换成本。运行时方法（纠正反馈、早退检查、预算估计、隐状态失败检测）同样不学习跨任务经验。TokenEconomizer 则用已完成轨迹去适配每个环境的指令前缀、工具集与停止策略。与模型级方法（级联、路由）的根本区别在于：级联与路由在每个查询上用质量换成本，而 TokenEconomizer 保持模型与推理力度固定、移除的是环境内重复发生的成本——它优化的是摊销（amortized）成本而非单次成本，这也是它能在降本的同时偶尔提质的结构性原因。先前工作的空位由此清晰：轨迹内的上下文控制与接口限制是固定且任务局部的（成本画像证明其效果随仓库漂移）、经验复用方法又不经由商用智能体的暴露接口行动——「自适应 + 黑盒 + 经验驱动」三者同时成立的控制器此前并不存在。作者在附录 A 中进一步指出，TokenEconomizer 只是「外挂控制器」这一更大设计类的一个实例：同一模式可扩展到按任务选推理力度或模型、在学习到的时点压缩上下文、跨任务复用环境搭建等 harness 暴露的其他控制面。

3.3 问题定义：任务流上的累积成本最小化

「黑盒」在此有精确含义：控制器不读模型权重、不读内部状态、不改一行智能体代码，只通过三个暴露面行动——指令前缀（注入微技能手册）、工具配置（决定加载集）、实时事件流（监控 rollout 并在规则触发时经 LLM 裁判干预）。它的每次模型调用（提议者、工具法官、轨迹法官、重定向撰写者）都与任务智能体同模型同路由并计入成本。

优化单元是一个环境内按时间顺序的任务流 τ1,…,τn。控制器维护仓库状态 Si−1（微技能与证据、工具使用历史、轮次统计），在任务 τi 开始前输出三元组 (ΔPi, Ui, Bi)——注入的微技能集、加载的工具集、失败循环干预的轮次预算；任务跑完后从轨迹 ξi 更新状态到 Si（状态更新函数写成 Si = F(Si-1, τi, ξi, yi)。因果性由构造保证：Si-1 只由先于 i 的任务构成、失败守卫只观察轨迹前缀，任何对 τi 的决策都不依赖流中更晚的任务——无未来泄漏）。ΔPi 只依赖 Si-1、渲染为插在 harness 指令与任务描述之间的短手册；Ui 限定为仍似有用的目录工具；Bi 校准在线失败循环守卫何时重定向或终止。控制器也可以选择不激活任何微技能、保留全工具目录、从不干预——即完全退回默认配置。目标是最小化平均单任务缓存感知成本（cache-aware cost，Eq. 4），把控制器自身的所有辅助模型调用（微技能提议、工具判定、轨迹判定、改写撰写）都计入触发它的任务，同时约束成功率不低于默认执行减去容差 ϵ（Eq. 6）。作者强调 Eq. 6 是设计目标而非评测时调参规则——没有在看到结果后选 ϵ，实验只报告相对配对默认执行的观测成本变化与成功率差。成本核算的诚实性是这篇论文的方法论亮点：每个辅助调用恰好一次地计入触发它的任务边界（如周期性任务后更新记入触发它的任务），缓存读取按提供方报告的 token 类别计价（不重建为全新输入），任务智能体用量与所有归属控制器调用写入同一执行记录后才求值——共享核算路径防止被优化方法把工作挪进辅助调用或靠模型路由拿未报告折扣。所有方法跑在同一答案泄露防护（answer-key guard，容器内 GitHub 域名解析到不可达地址、Claude Code 与 Copilot CLI 另加拒绝引用 GitHub 的 pre-execution hook）之后，杜绝了取巧空间。

跨 harness 适配是「黑盒」主张的试金石，实现上靠适配器而非新元策略。三个 harness 各有怪癖，适配过程本身就是一份接口考古：Claude Code 以 headless JSON 事件流为轨迹、disallowed-tools 移除 schema、重定向以同容器新调用重启 CLI；Codex 的工具只能按能力包（capability package）整体开关——子智能体协作、目标跟踪、图像输入、捆绑技能与交互聊天指引等 headless 运行用不到的包整组剪除；Copilot CLI 的事件流不报 token 用量，控制器改读其调试日志，且发现其 deny-tool 只拒执行仍每轮计费 schema，必须用 excluded-tools 才真正移除。三个 harness 的版本（Claude Code 2.1.170、Codex 0.153.1、Copilot CLI 1.0.84-7）全部锁定，所有付费控制器调用与任务智能体同模型同路由；厂商事件流先被规约成含工具名、参数、观察、模型输出、用量与评分结果的公共表示，元策略只消费这个规约接口——「一套元策略、N 个适配器」的架构让控制器可以跟随智能体生态自然扩张。

3.4 解法：三条元策略，环境内自学策略

优化单元与控制接口的定义先于三条元策略：优化单元是一个环境内按时间顺序的任务流；控制接口是三条通道——任务间（激活的技能渲染进指令前缀）、每任务前（加载的工具集）、rollout 中（事件流上的实时干预）。三条元策略与三条通道一一对应：微技能走指令通道、剪枝走工具通道、失败守卫走事件通道，互不共享状态以外的耦合。

论文区分了三个层次：元策略（meta-strategy）是环境无关的通用过程；策略（policy）是元策略在特定环境中学到的决策；固定策略（fixed strategy）则是处处同配置的 RTK/RepoMap 之流。三条元策略共享同一设计模式——廉价的轨迹信号配保守的动作，且每个动作都带恢复路径。这个模式重复出现三次不是巧合，而是同一约束下的收敛解：控制器对环境一无所知（S0 为空），任何激进动作都必须有后悔药。

元策略一：经验接地的微技能注入。 控制器定期（第 4 个任务后每 5 个任务）把最近 8 个任务的摘要（command 模板、测试调用、编辑文件名、布尔标志、遇到的错误——不含解法文本或金补丁）交给 LLM 提议者，起草至多 4 条候选微技能（micro-skill）——每条是关于该仓库的单行操作性事实（如「测试用原生 runner 而非 pytest」「源码从树内导入、无需重装」），配可执行的三类检测器：scope（正则或内置谓词，选择技能相关的任务）、confirm/contradict（命令与输出中的证实/证伪证据）、need（所指浪费是否发生或所载事实是否被用到）。提议的 prompt 明确禁止把技能写成对探索或工具使用的禁令、禁止包含任务特定的修复——只许陈述跨任务成立的仓库级事实。每个任务结束后，检测器在轨迹的命令与输出上运行：被触发的任务若显示指令为假（如技能说已装的包报 import 错误）即证伪，否则证实。每个任务结束后，scope 检测器判断轨迹是否触发了该技能的场景，confirm/contradict 检测器判断事实被证实或证伪，need 检测器判断任务是否本可受益于它。激活需双重条件，分别回答「可靠吗」与「值得吗」：其一是可靠性——在编辑文件集互不重叠的 3 个任务上被证实，保证证据反映仓库级规律而非某个议题的局部巧合；其二是值得性——需求率（触发该技能场景的轨迹中确实需要它的比例）在至少 4 次触发上不低于 0.4，保证反复注入物有所值。两个条件缺一不可：只看可靠性会注入「正确但没人用」的事实（案例 d 的无需重装技能即因需求率 0/10 而永不激活），只看需求率则可能被议题局部的巧合骗过。准入之后还有逐任务的复核与账本维护。支持度（support）记账决定生死：q(f) 对历史证实按指数衰减（γ=0.8）折旧、对证伪按不对称权重（λ=5）加权求和，一旦跌破零该技能永久退休、其标识符永不再激活（提议者可以新标识符重新提议替代品）。高风险技能（如测试命令、构建步骤——错了会毁掉整次运行）在满足证实条件后首次证伪即退休。三套机制各司其职：证实数管晋升、需求率管逐任务注入、支持度管退休——一个有准入、有考核、有退出机制的信念账本。这种不对称是刻意的：该退休而未退休的技能会在此后每一轮的前缀里被反复计费，而过早退休的技能还能以新标识符被重新提议——两类错误的成本天然不对称。

在准入与退休之间，在准入与退休之间，生命周期管理还有两处精巧的设计。其一是提议门槛：每个候选必须引用窗口内至少 2 个检测器证实它的任务，且被准入时其检测器回溯运行于窗口任务之上，带着既有证据入场、可立即激活；对已存在的技能只能原 id 重发并只允许改 contradict 检测器，其余任何改动被拒绝——防止「换个说法重启不良信念」。

其二是证据的地域性约束：确认（confirmation）要求 3 次证实的编辑文件集互不重叠，从而保证证据反映仓库级规律而非单一模块的局部巧合——附录案例 (e) 中一条关于 sphinx python 域测试文件的技能有 7 次证实、但除一次外全部来自编辑了同名 python.py 的任务，终其流未获激活；案例 (b) 中一条 sphinx 复现技能的前两次证实都编辑了 conf.py、只计一次，直到第 5、6 个任务（不同文件）补齐互不重叠的第三次才获激活。附录案例 (d) 则展示了需求门的价值：一条「sympy 从树内源码导入、无需重装」的技能有 10 次证实零证伪，但没有任何任务真的执行它所警告的多余重装（需求率 0/10 < 0.4），于是被确认却不注入——正确但无用的知识不该占用每轮计费的前缀。案例 (c) 是教科书级的失败与自愈：「用 pytest 跑 sympy 测试」的高风险技能因证实检测器只匹配命令本身而非通过结果，被 40 次证实推入激活，首次注入后一条 ModuleNotFoundError 触发证伪、λ=5 的权重将其立刻清退；同一仓库的另一条流随后学出了正确的原生 runner 技能（python -c “import sympy; sympy.test(…)"），把默认 15 轮的任务压到 11 轮。

元策略二：工具剪枝。 画像里「23 个 schema、16 个从未调用、3 个占 98%」的事实决定了这条策略的收益下限。控制器永远保留 shell 执行与文件读、写、编辑等核心工具；其余工具走双重移除判据：连续 3 个已完成任务未调用（未用历史判据），或 LLM 法官评估其与任务描述的相关性时判为无关（描述中的 PR、issue、commit 与文件链接均以占位符掩码）。为从误删中恢复，每 5 个任务做一次全目录重审（re-audit）——重审不加法官调用、直接加载全目录；重审中被调用的工具永不再屏蔽（只有从未调用的工具才可能被屏蔽，恢复因此单调收敛）。剪枝单位在 Codex 上是能力包（capability package）而非单个工具，因为其配置只支持成组开关。附录的实例给出了直观规模。Django 流上 Claude Code 默认每任务首请求 42-46k prompt token，任务 2 起法官掩蔽 19 个工具（AskUserQuestion、Cron 系列、Task 系列、Workflow 等）后首请求降到 15,003-16,295 token——单这一项就砍掉了约六成的首请求开销；Copilot CLI 上 19 个工具中掩蔽 10 个（factories_manage、fetch_copilot_cli_documentation、sql 等），首请求从 25-26k 降到 10-11k。

元策略三：失败循环干预。 前文的画像已经说明为什么止损难做：失败任务吃掉 32% 的花费，但成功运行也会重复失败签名、仓库间轨迹长度差异巨大。干预的分层结构正是针对这个难度的：最底层是每步零成本的规则触发器，维护重复命令与错误计数、编辑翻搅、不同编辑文件数、状态无变化、重复验证失败的运行计数器；触发器只在开启时咨询 LLM 裁判，且至多每 5 轮一次，每次「有进展」裁决后间隔再增 5 轮（上限 20 轮）——裁判的费用本身也被节流。失败签名（failure signature）取失败输出的首行错误（traceback、失败测试或断言），剥离数字、内存地址与文件路径，使同方式失败的输出可匹配。轮次预算 Bi = β × 成功任务轮数的第 90 百分位（β=1.25），用高百分位而非最大值防止单个异常长成功撑爆预算、让成功运行普遍长的仓库获得成比例更大的预算；它是「异常长」的参照而非硬停止点。每次工具调用后，基于规则的触发器（无模型调用）检查重复失败签名、密集错误输出或超出预算；触发后 LLM 裁判复核近期动作摘要，区分「无进展的循环」与「困难但仍在推进」。确信（置信度阈值 0.7）的卡死判定先做一次改写重定向（redirect）——由独立的重定向撰写者生成 2-4 句的干预文本，点名摘要中实际可见的重复模式（反复编辑同一文件、重跑同一测试同样失败）并提出实质不同的下一步（换个文件或根因假设、重读失败测试的期望、先验证新假设再编辑），明确不许叫停或降低力度；失败模式复发且法官再次判卡死才终止 rollout。

裁判不能否决的强制停止（forced stop）是最后防线：轮数（跨重定向累计）达 κ=2.5 倍预算 Bi，且严格停滞规则三条件同时成立——编辑翻搅（单文件至少 4 次编辑或至少 3 个文件被编辑）、密集错误（至少 6 个错误输出）、重复（至少 20% 失败输出重复早先签名）。附录案例 (h) 中，一次重定向让默认 42 轮的任务在 31 轮内完成（重定向后智能体重读测试期望、一次通过 7 项测试）；案例 (i) 中强制停止让一个默认与干预都会失败的任务提前 7 轮止损（学到的预算 Bi=10.25 轮，2.5Bi 处触发）。

3.5 实验证据：30 个仓库-设置单元全绿

主结果。 质量度量按基准取官方口径：SWE-Bench 用官方评分器的 Pass@1、Web-Bench 用官方推荐的累积 Pass@2、安全基准用检测 F1；效率度量是平均缓存感知成本。每设置三种子，种子间只差智能体自身的非确定性。具体覆盖五个智能体-模型设置——Claude Code 配 Sonnet 5 与 Opus 4.8、Copilot CLI 配 Sonnet 5、Codex 配 GPT-5.6 Terra 与 GPT-5.6 Sol——各跑同样 277 个 SWE-Bench 任务（6 仓库：scikit-learn 60、SymPy 60、Django 40、Sphinx 44、Matplotlib 34、xarray 39，含 199 个 Verified 与 78 个全量分割任务）、三个种子。任务流的构造颇有讲究：xarray 的 22 个 Verified 任务中最老的 13 个在 2019-2021 年间稀疏分布，流改用 2022 年 4 月起的 9 个 Verified 任务与 30 个全量分割任务按 base commit 序交错，使相邻任务通常相隔数天（issue 日期中位间隔 4 天）；scikit-learn 与 SymPy 从全量分割补的任务经作者逐一在官方镜像应用金补丁并跑官方评估验证（61-200 行改动的金补丁、按补丁大小均匀间隔采样）。

TokenEconomizer 单独使用即降本 18.4-30.9%，五设置明细为：Claude Code+Sonnet 5 降 23.6%（Pass@1 74.7→76.0）、Claude Code+Opus 4.8 降 30.9%（74.0→73.0，唯一回落）、Copilot CLI+Sonnet 5 降 18.4%（75.0→77.6）、Codex+GPT-5.6 Terra 降 24.7%（73.8→74.7）、Codex+GPT-5.6 Sol 降 26.1%（80.1→81.7）。对照之下，中推理努力降 16.8-28.9% 但 Pass@1 掉 1.8-7.2 点、低推理努力降 31.0-45.5% 但掉 4.6-10.3 点；RTK 与 RepoMap 单独使用节省小而不一致（RTK 为 -1.1% 至 +4.5%，RepoMap 为 -6.1% 至 +6.5%）。TokenEconomizer 变体占据了成本-质量帕累托前沿上所有不低于默认通过率的点——降推理努力的点位深在左下（省得多、掉得更多），RTK/RepoMap 的点位在默认附近忽左忽右，TE 系变体独占右上区域。

一致性。 这是论文最硬的一张图：6 仓库 × 5 设置共 30 个仓库-设置单元，TokenEconomizer 与 TE+RTK 在全部 30 个单元降本（幅度 5.2-40.1%），TE+RepoMap 在 29/30 降本；对照之下 RTK 单独使 12 个单元升本（图上标注 12/30）、RepoMap 单独使 15 个单元升本（15/30）、TE 只有 0/30 升本、TE+RTK 0/30、TE+RepoMap 仅 1/30。**汇总均值会掩盖个体环境的成本上升（固定策略正是这样翻车的），逐单元报告才是成本控制论文该有的证据标准。**顺带一提，RTK 在 Codex+GPT-5.6 Sol 单独使用时甚至升 4.5%，而叠加 TE 后转为降 23.3%——自适应控制器甚至能驯服一个不稳定的固定策略。在 Opus 4.8 上叠加 RTK 把节省从 30.9% 推到 33.2% 且 Pass@1（74.8）回到默认之上。

累积动态。 每个仓库从零开始（S0 为空、无任何先验），除 xarray 外所有仓库在 TokenEconomizer 下起初更贵（控制器在学习、提议与判定的开销先行），但全部仓库到第 6 个任务转为止亏，此后持续更便宜并保持到底，流末累积节省 16.9-32.0%。

这条「先亏后赚」的学习曲线本身是经验资产化路线的定价曲线：学习期投入的是控制器调用与试探性注入，回报期兑现的是此后每个任务的前缀瘦身与止损。部署者可以据此估算回本周期——在 20-60 个任务的流上大约是第 6 个任务。

泛化。 三个域外基准的设置与结果值得逐一展开。Web-Bench 取 5 个项目共 102 个连续任务（calculator 与 table 基于 HTML/CSS/JS 各 21 题、expressjs 20 题、react 20 题、zustand 20 题），按基准官方协议每任务两次尝试、首次失败带测试错误重试（因为每题建立在前一题之上、单次失败会终止整条流），报告 Pass@2 且成本含两次尝试：三设置降本 21.2%（Pass@2 69.3→73.3）、16.0%（64.0→66.5）、18.7%（60.8→59.3）。CredData 凭证检测从 333 仓剔除 19 个无真密钥行者、按真密钥行数四分位成比例抽 100 仓（选中仓 1-799 行真密钥、中位 8.5）；ReposVul 从 Python 分割 1,310 实例剔除 298 个修复不删行者与 109 个过期者、按漏洞行数四分位抽 100（1-411 行、中位 5），行级严格评分（报对函数但报错行记零分，比此前工作按函数级二元 F1 更严）。

两基准的特殊结构在于：每个任务都是不同仓库下的同一固定审计提示，程序性重复存在而仓库连续性不存在——故仓库级微技能被禁用、只留工具剪枝与失败守卫两条元策略。这恰好构成一次自然实验：CredData 降本 16.5-19.6% 且 F1 三设置全升（67.9→70.1、68.0→69.2、68.2→67.7），ReposVul 降本 6.4-9.3%、F1 亦全升（17.5→19.6、19.4→20.1、21.6→22.5）。降幅随轨迹内可复用结构与可削减空间伸缩——短轨迹的只读审计省得少，连续建库的 Web 开发省得多。

消融。 两个 Claude Code 设置上：工具剪枝单列贡献最大（Sonnet 5 -13.2%、Opus 4.8 -17.7%，因为它作用于每轮每任务），微技能注入紧随（-11.8% 与 -14.3%），失败循环守卫个位数（-7.1% 与 -5.4%）；Pass@1 上微技能单列在 Sonnet 5 反升到 77.3、守卫单列升到 76.2，工具剪枝单列 74.3/73.5 略低于默认但差距在 3 点内；三者的组合（-23.6% 与 -30.9%）明显超过任何单列之和的简单叠加，且没有任何单列复现全栈的节省。活动统计显示三条元策略几乎互不干扰：约五分之一的被提议技能在流内退休（账本在修订信念而非囤积信念），轨迹裁判每流咨询 10-13 次但约十任务才一次重定向、二十任务不到一次终止。

消融的进一步细节。 活动统计（附录 H，按流平均）还揭示三条元策略互不干扰的量化证据：全栈组合中各策略的动作计数与其单列变体几乎一致（如 Sonnet 5 流上每流提出 12.1 条候选、确认 8.4 条、退休 2.6 条，单列微技能为 11.4/7.2/2.1；屏蔽 schema 14.8 个、重审 3.1 次，单列剪枝为 15.1/3.3）。计数本身也说明各策略多么克制：约五分之一的候选技能在流内退休——账本在持续修订信念而非囤积信念；轨迹法官每流被咨询 10-13 次但约十任务才产生一次重定向、二十任务不足一次终止，多数升级以「有进展」或「不确定」告终。这些参数全部服务于一个设计立场——组合的每一部分都按「保守准入、激进清退、可恢复」运作，谁也不抢谁的地盘。

配置的唯一性。 一套超参数（附录表 4，全部在主实验前于早期开发运行中固定）服务三个 harness、五个设置、四个基准，唯一随基准变化的是流结构所迫的调整：Web-Bench 流只有 20-21 个任务、成功轮数百分位来不及热身，故守卫用预登记的 30 轮预算预热直到 5 个任务通过；安全审计每个任务一个新仓库，仓库级微技能永远没有同仓库的后续任务可应用，故关闭注入、只留工具剪枝与失败守卫两条元策略。30 个单元全绿而无逐环境调参，说明元策略捕捉的是智能体工作的共性规律——重复的操作事实、未用的接口、无产出的循环——而非某个智能体或数据集的伪影。这套共享配置同时是默认而非约束：每个参数都是带方向的旋钮，用户可沿成本-质量前沿按优先级调整。

3.6 根源解释：为什么经验资产化能一致奏效

成本结构本身是重复的。 12-28% 的字节来自重复动作、每轮 23 个 schema 中 16 个从未用、失败任务占 17% 任务却吃 32% 成本——这三块余量是环境级结构，不是任务级噪声；固定策略之所以忽升忽降，是因为它对同一结构不做环境适配。经验性证据是决定性的：跨仓库对照只匹配 7%（通用命令），而同仓库第 5 个任务起重复率达 30%——可学习的是仓库特异的重复，而非笼统的命令冗余。这 23 个百分点的差值，就是经验资产化的原料。

微技能的粒度选对了可验证性甜蜜点。 一行操作性事实可以在每条后续轨迹上被正则检测器免费复核，其效度在整个流中持续受检，而非创建时检验一次；它不含任务特定内容，注入错了也能被 λ=5 的一次证伪快速清退。可执行技能库与自然语言课程都不具备这种「逐任务可验证性」。 每个决策都有恢复路径，使错误决策的代价有界。 过时的技能被证伪退休、错剪的工具在重审回归、误判的循环先被重定向而非直接终止——保守动作加恢复机制，让控制器在没有任何环境先验的情况下敢做激进试探。恢复路径的存在也改变了参数语义：需求门、未用连击、预算边际都成了带方向的旋钮（论文附录逐一说明每个旋钮拧向何处、换什么风险），用户可沿成本-质量前沿按优先级选择。 微技能的粒度同时是对「持续计费」的回应。 论文附录还论证了为什么是一行事实而非可执行技能库或自然语言课程：其一，它对准观测到的成本——前沿智能体已能解大多数任务，可削减的花费大头在逐任务重新发现同一环境事实，而非解题能力缺失；其二，它逐任务可验证——检测器在每条后续轨迹上免费复核一行关于命令与输出的事实，而一条泛化课程是否有用很难从轨迹读出；其三，它便宜且低风险——手册每轮计费故每条必须精短且挣得自己的位置，且因为它陈述事实而非解法，不把早先任务的任务特定内容带入后续任务。

• 跨 harness 一致性指向的是 harness 之上的共性。 一套元策略、一套参数在三款智能体上同时成立，说明可削减成本不属于任何一款 harness 的实现细节，而属于「智能体 + 工具接口 + 任务流」这一抽象结构的固有属性——这也预示该思路可以平移到任何同构系统（数据分析智能体、运维智能体、测试智能体）。跨 harness 一致性因此不只是稳健性指标，更是普适性证据。
• 降本与提质并不必然冲突。 四个设置 Pass@1 上升并非偶然，机制上各有出处：省下的上下文（更少工具 schema、更少失败探测的噪声）本身减少了注意力干扰；重定向把智能体从死胡同里拉回正轨（案例 h 从 42 轮到 31 轮完成）；微技能则直接免掉了「发现环境怎么工作」的反复试错（案例 a 从 15 轮到 11 轮）——削减的是熵，不是能力。这也是整条经验资产化路线最重要的辩护词：它不是在压缩智能体，而是在压缩智能体周围的可预测浪费。

3.7 知识反推：轨迹数据告诉我们什么

其一，前沿智能体在一个仓库里的花费高度可预测：第二个任务起就有 14% 的调用与更早任务重复，五个前序任务后升到 30%——「智能体在重新学同一个环境」不是修辞，是可计量的浪费。

其二，失败可以被早期识别但不可以被简单规则识别：成功运行也会重复失败签名，仓库间失败轨迹长度差异巨大（Matplotlib 失败 45 轮 vs 成功 20 轮，Sphinx 失败 36 轮 vs 成功 31 轮），因此有效的止损必须参照该环境自己的成功分布，并由语义裁判区分停滞与推进。 其三，工具目录的「默认全载」是一种隐性税：23 个 schema 每轮计费而 16 个从未被用、3 个占 98% 调用——接口设计者应当意识到，给智能体看的每一样东西都是要花钱的，而多数部署从未审视过这笔固定开销。

其四，SWE-Bench 是经验复用的保守测试：流内任务相互独立（各自从 base commit 新检出、互不继承编辑）、跨 1.9-8.5 年仓库历史漂移，真实开发者会话回到增量演进的代码库，可复用经验只会更多——Web-Bench 上较短流仍有 16-21% 节省正是佐证。换句话说，本文报告的节省幅度更像是真实部署的下界而非上界。

局限性（论文自述）。 每条元策略都可能误判：微技能可能过时、被剪的工具可能忽然必要、困难但多产的任务可能被误判为失败循环。但每个决策都配恢复路径以限制损害——过时技能被轨迹证伪后退休、错剪工具在下次重审回归、失败循环干预先重定向后终止并放过不确定情形。实验覆盖三个广泛使用的编码智能体但不包括 Pi 等更精简的 harness；由于控制器只依赖提示词、工具配置与事件流，支持新 harness 只需适配器而非新元策略。最后，SWE-Bench 流由相关但独立的修复构成、并非真实用户会话——连续会话应提供更多可复用经验，交互式编码工作流是自然的下一步测试场。

3.8 通用灵感：超出编码智能体的启示

• 「外挂控制器 + 暴露接口」是智能体生态的一个独立产品层：只要一个智能体暴露提示词、工具配置与事件流，就可以被一个不改其内核的控制器优化；模型与 harness 迭代越快，这一层的价值越稳定。附录 A 展望了同一模式下的其他控制面：按任务选推理力度或模型、在学习到的时点压缩上下文、跨任务复用环境搭建——每一个都是潜在的独立产品。
• 不对称错误成本设计（λ=5 的一次证伪压倒多次证实）适用于一切「持续计费的信念系统」：错误信念的持有成本随时间复利，清退机制应当比准入机制激进得多。凡是「每轮都付费」的东西——注入的指令、加载的工具、保留的记忆——都该配一套指数折旧加不对称惩罚的账本。
• 廉价的规则触发 + 昂贵的语义裁决是干预类设计的经济最优结构：每步无模型调用的计数器筛选，把 LLM 裁判的调用频率压到每流十几次（且随「有进展」裁决自动拉长间隔），裁决后仍保留改写、终止两级递进的响应，最后还有规则兜底的强制停止——分层不是两层，而是一个每层都比上层便宜、都比下层智能的栈。
• 把基准变成答案泄露防护下的配对实验（所有方法同任务同顺序同防护、种子只差智能体自身非确定性、控制器开销全额入账）是评测方法论的示范，值得所有系统类论文效仿。
• 「逐任务可验证的信念」是 Agent 记忆系统的新设计维度。 与把经验存成可执行技能或泛化课程不同，微技能证明了「事实 + 检测器」这一最小单元的价值：它的效度可随流持续复核、它的成本（每轮计费）倒逼准入纪律、它的错误可被单次证伪清退。任何要给智能体挂长期记忆的团队都该问：这条记忆多久被重新验证一次？占多少前缀？错了怎么退场？

四、双篇合评：training-free 路线的两种极致

当代智能体系统可以粗略分成四层：模型权重、智能体循环（harness）、运行时基础设施（算力编排与服务化）、跨任务的资产生命周期（记忆与经验管理）。训练路线改的是第一层；两篇论文证明，第一层之上的每一层都还有独立可观的收益空间——EASYPROVER 主攻第三层（运行时与验证基础设施），TokenEconomizer 主攻第四层（经验资产），而两者都没动第一、二层——这正是「training-free」的字面含义与结构含义。这种分层视角也解释了为什么两者的收益可以与训练路线叠加而非互斥：换更强的模型，EASYPROVER 的搜索直接变宽、TokenEconomizer 的技能照常学习——工程杠杆对模型进步是单调放大的，而不是被替代的。

把两篇论文并置，最有趣的是它们在「不重训模型」这同一约束下做出的截然相反的杠杆选择。

EASYPROVER 选择基础设施规模化：用空间换成功率。 它的核心洞察是，前沿模型的知识储备已足以覆盖现有基准，缺的是让这些知识被完整兑现的搜索组织——于是它把赌注押在三个方向的可扩展性上：递归委派让搜索宽度脱离上下文深度约束（300+ 子智能体），无状态推导服务让验证吞吐脱离单机容量约束（0.2 秒热推导对数十秒冷导入），自动数据管线让任务供给脱离专家标注约束（11,533 条候选规格）。它的成本结构是运行时重、知识零：每一次运行都要付出大量算力，但不需要任何训练投资；它的收益是能力边界的直接推进——饱和一个基准，再自造一个更难的。

TokenEconomizer 选择经验资产化：用时间换成本。 它的核心洞察是，智能体的开销高度结构化且结构可学习——于是它把赌注押在轨迹的沉淀与门控复用上：微技能把「这个仓库怎么工作」压缩成可逐任务验证的一行事实，工具剪枝把接口收敛到实际使用的子集，失败守卫用该环境自己的成功分布校准止损点。它的成本结构是学习期小亏、成熟期持续省（所有仓库第 6 个任务后转亏为盈，流末累积省 16.9-32.0%）；它的收益是帕累托前沿的扩张而非边界的推进——同样的钱做更多事，同样的任务更快止损。

两条路线在三个设计维度上形成精确的对偶：

下表把这对偶在五个设计维度上对齐（其中「失败的处理」与「重复的消除」两行最能看出两种哲学的分野）：

表格里最后一行值得展开：两条路线各自埋着一个未被完全解决的隐忧。EASYPROVER 的成绩单没有总账——每题 30 分钟预算 × 2,000 题的算力成本、INFINILEAN 副本池的运维开销都未折算进对比叙事，这是「无限算力换饱和」路线的固有盲点；TokenEconomizer 的每个误判都已有恢复路径，但恢复本身有延迟（错剪的工具要等最多 5 个任务后的重审），在短任务流里这个延迟窗口不可忽略。工程路线的成熟，最终要靠把这些隐忧也纳入度量的诚实。

成本视角下的镜像对照。 有意思的是，两篇论文都隐式承认了对方的约束。EASYPROVER 的并行 tactic 探测（丢弃 30,000 token 只留 30 token）本质上是一种昂贵的上下文经济学——它用算力换上下文纯净度，如果没有 INFINILEAN 把单次推导压到 0.2 秒，这种「万倍试错」策略在经济上不成立；换言之，它的能力纪录是用不设上限的算力预算换来的（论文虽给出 NTP4VC 的单任务时间与成本分布，却未报告总账）。TokenEconomizer 走的是相反方向：它把每一分可避免的开销都视为待清除的浪费，却因此只能优化既有能力之下的成本前沿，无法把系统推过当前能力边界——30/30 单元降本是效率的胜利，不是能力的胜利。一个用成本换能力，一个用能力余量换成本——两条曲线在帕累托空间里恰好互补。

对「验证」的两种用法。 两篇论文对验证信号的用法也构成对偶。EASYPROVER 里验证是最终裁决：Lean 内核的接受检查是唯一计数口径，智能体的自我报告与局部探测成功都不算数，验证一次、终身有效（任何人可用同环境与公理策略复核）。TokenEconomizer 里验证是持续过程：微技能的每条后续轨迹都被检测器免费复核，信念的效度在整个流中持续受检而非一次定终身。前者是司法式的终审判决，后者是审计式的持续监督——但两者都把「不信模型自述、只信可复核证据」贯彻到了系统每一层。对正在构建智能体产品的团队，这一条可以直接当成验收标准：你的系统里，哪些信号是自我报告的？哪些是独立可复核的？两者的比例，往往就是系统可信度的比例。

与固定策略的互补与冲突。 合评里也该记录 TokenEconomizer 与固定策略的组合结果——它提供了「组合收益并不简单」的直接证据：在 Opus 4.8（TE 单独比默认低 1.0 点）上，加 RepoMap 或 RTK 把 Pass@1 拉回 75.1 与 74.8（高于默认），组合在三设置中拿到最高 Pass@1；但节省并不叠加——RepoMap 每轮为其地图计费，TE+RepoMap 在五设置中的四个节省反而少于 TE 单独，RTK 的加入在 Opus 4.8 上加分（30.9%→33.2%）却在别处最多减 5.2 个点。作者的解释是信息互补：微技能说「怎么在这个仓库操作」、RepoMap 的排序签名回答「修复属于哪里」、RTK 的压缩日志保持失败信息在更短上下文中的显著性——组合换的是质量，代价是部分节省，哪个组合更优取决于设置。

数据与任务设计的对偶。 在任务供给上，两篇论文同样构成镜像。EASYPROVER 面临的是「基准太少太饱和」，于是 AEGIS 用「公共题源 + 自动翻译 + 内核检验双极标签」造出源源不断的新任务，其防污染逻辑是任务在本工作之前不存在；TokenEconomizer 面临的是「评测与真实使用错位」，于是把评测单元从孤立任务改成时序任务流（任务按 base commit 时间排序、控制器只能学习该仓库更早的历史），其防泄漏逻辑是答案防护加时序因果（任何决策不依赖流中更晚的任务）。一个扩展任务的「空间」，一个扩展评测的「时间」——但都指向同一个主张：静态快照式评测正在失效，评测要么能再生、要么能累积。对基准构建者而言，这是比任何单个分数都重要的方法论信号。

更深层地，两篇论文共同验证了同一个判断：模型外围的系统层存在独立的、可量化的进步空间。EASYPROVER 证明了搜索组织与验证基础设施的改进可以直接兑换成基准纪录（PutnamBench 669/672 对此前最强 597/672）；TokenEconomizer 证明了经验组织的改进可以直接兑换成一致的成本削减（30/30 单元全绿，对照固定策略 12-15 个单元反升）。两者都用「可复核的数值」替代了「看起来更强」的叙事——内核检验的证明、全额入账的配对成本——这种度量纪律本身就该被视为贡献的一部分。

两条路线也各自指出了对方的天花板——这是把它们放在一起读才看得见的第三层价值。EASYPROVER 的 AEGIS 证明纯基础设施路线撞到真实代码验证的复杂度时仍会留下近半未解空间（52.7%），这部分缺口大概率要靠训练（论文自己把 AEGIS 定位为 RLVR 奖励环境）来填补；TokenEconomizer 的上限受制于轨迹中可复用结构的密度（ReposVul 短轨迹只省 6.4-9.3%），且其微技能是环境局部的，不产生跨环境可迁移的能力。一个的产物（可验证任务与双极标签）恰是另一个（以及所有训练路线）的燃料——这种互补性暗示下一阶段的最优解很可能是两者接续：先用基础设施规模化生产数据（AEGIS 已把自己定位为 RLVR 奖励环境），再用经验资产化压缩其训练与部署成本。放到更长的周期看，基础设施规模化负责把能力上限推上去、经验资产化负责把单位成本压下来，两条曲线的剪刀差就是 training-free 路线为整个领域赢得的战略空间。

值得最后强调的是时间维度上的接续逻辑：基础设施规模化产出的可验证任务与双极标签，恰好是训练路线最稀缺的燃料；而训练与部署的规模化，又恰恰最需要经验资产化提供的成本削减。这两篇论文不是两条平行线，而是一个循环的两半——上一步的产物是下一步的原料，工程路线自己就能滚起来。

五、结语

这两篇论文放在同一天读，像是一次刻意安排的对照实验：同一个「不重训」约束，一个走向证明搜索的深度与宽度，一个走向任务流的经济学；一个的产物是可验证的知识（证明与任务），一个的产物是可复用的经验（技能与策略）。EASYPROVER 把「不训练」做成了进攻性武器：一个现成模型加一套认真设计的递归运行时与弹性验证服务，就能把形式数学与代码验证基准推到饱和，再自动造出更难的基准把自己打回 52.7%——它的每一次胜利都附着一个内核检验的封印。TokenEconomizer 把「不训练」做成了防守性艺术：一个不碰模型不碰循环的外挂控制器，从自己走过的轨迹里学出仓库级的省钱策略，在三个商用智能体、30 个仓库-设置单元上无一例外地降本——它的每一分节省都带着全额入账的凭据。

两条路线也共同暴露了 training-free 范式的边界：EASYPROVER 的能力跃迁依赖「现成前沿模型已封装了足够知识」这一前提——对知识确实不在模型里的领域（如未形式化的新数学），同样的基础设施只能给出更宽的失败搜索；TokenEconomizer 的收益依赖「成本结构可从历史学习」——对每个任务都是全新环境的场景，控制器退化为两条最朴素的元策略。承认边界不是否定：恰恰是把边界画清楚，才知道下一份力气该花在哪里。

它们共同提醒我们：在追逐下一个训练范式的喧嚣里，工程杠杆的复利仍在安静地积累。值得注意的是，两篇论文的作者构成也暗示了这条路线的产业重量：一篇出自 AWS 的自动推理团队（形式化验证本来就是 AWS 的看家本领），一篇出自微软研究院与 UC Berkeley（Ion Stoica 等系统学派的重镇）——系统社区正在把四十年的基础设施与经济学直觉注入智能体栈。上下文的隔离经济学、检查器的微服务化、信念的不对称清退、轨迹的资产化复用——这些设计没有一个是「新智能体架构」，但每一个都在可复核的度量上兑现了训练路线难以企及的确定收益。对于在真实业务里部署智能体的团队，这个信号值得认真对待：在加预算换更强模型之前，先检查你的系统是否已经把现成模型的能力兑现干净、把重复的花费修剪到位。模型会继续换代，而这两套方法论——一个把基础设施用到极致，一个把经验用到极致——都不会随模型换代而贬值。EASYPROVER 的递归运行时与弹性验证服务对任何更强的模型都是即插即用的放大器（更强的子智能体直接翻译成更宽的搜索与更高的证明率）；TokenEconomizer 的三条元策略对任何暴露提示词、工具与事件流的 harness 都是即插即用的减震器（它的全部参数在主实验前固定、跨三 harness 四基准一套通用）。当下一波训练范式的红利见顶时，这两类工程杠杆大概率仍在那里，安静地兑现着复利。

如果要用一句话分别记住这两篇论文：EASYPROVER 告诉我们，当模型的失败可以被便宜地隔离与掩埋时，搜索宽度就是新的智能；TokenEconomizer 告诉我们，当环境的重复可以被便宜地检测与复用时，经验就是新的折扣。两句合起来，就是 training-free 路线的全部纲领。

最后给不同读者的落点建议：做形式化验证或证明助手的读者，AEGIS 的双极标签管线与 INFINILEAN 的无状态化设计是最值得移植的两件东西；做智能体平台或 DevInfra 的读者，TokenEconomizer 的「元策略-环境策略」两层抽象与全额入账的评测协议可以直接抄作业；做研究的读者，两篇论文各自标注的留白——AEGIS 作为 RLVR 环境的首次训练实验、TokenEconomizer 在真实用户连续会话上的验证——就是现成的下一题。

（完）