VALG：以自适应图证明挑战COLT 2026，AI推进9个前沿理论难题

VALG: An Agentic System for ML Theory Research

在人工智能与数学推理的交叉领域，大语言模型正在经历从“做题”到“做科研”的范式跃迁。以往的大模型数学基准测试，无论是 Putnam 还是各类竞赛题库，本质上都预设了一个绝对封闭的边界：前提公理固定、目标命题清晰、证明路径唯一收敛。然而，真正的理论科学研究——尤其是机器学习理论（Machine Learning Theory）——其探索过程远比单纯的定理证明复杂。一个未解的理论开放问题往往只勾勒出某种学习现象的轮廓，研究者必须在探索过程中同步构思问题形式化、设计技术假设、权衡渐近体制，并在推导受阻时反复修正问题本身。

ArXiv URL：https://arxiv.org/abs/2608.13060v1

西北工业大学、深圳河套学院与香港大学的研究团队提出了 VALG。这是一个专门面向机器学习理论研究的自主智能体系统，其命名致敬了统计学习理论与计算学习领域的四位先驱：Leslie Valiant、Dana Angluin、Nick Littlestone 与 E. Mark Gold。该系统首次直面了机器学习理论推导中“假设、定理目标与证明机制协同演化”的科研现实，通过自适应问题形式化（Adaptive Formulation）、类型化图结构证明展开（Graph-structured Proof）以及多维度验证（Multi-level Verification）三大机制，让智能体学会在探索受阻时合规地松弛条件、隔离特例，而不是悄无声息地“偷换概念”。

为了检验这一系统的真实科研能力，研究团队没有选择已被充分研究的合成数据集，而是直接让 VALG 挑战计算学习理论顶级会议 COLT 2026 刚刚提出的 5 篇开放问题论文，覆盖张量分解的交替最小二乘法（ALS）过参数化界限、差分隐私 PAC 学习、单比特均值估计等前沿方向。在独立的 9 个子问题攻坚中，VALG 共产出了 22 个内部定稿的定理候选，其中 2 个子问题达成了与原题设定完全匹配的完整解决，其余 7 个子问题也严格给出了受限算法、特定体制下的松弛解或条件定理。这一成果展现了智能体系统协助甚至独立推进前沿机器学习理论研究的可行路径。

机器学习理论研究的“原罪”与形式化鸿沟

要理解 VALG 的技术构思，必须先看透机器学习理论研究的独特性。在纯粹的代数或数论中，命题形式通常是刚性的，如果假设条件发生变动，问题往往就变成了另一个命题。但在统计学习理论中，一个典型结果的成立高度依赖于对数据分布的尾部条件、假设空间的复杂度、预言机（Oracle）的访问权限、优化算法的更新协议以及渐近参数体制的联合设定。

这种高度的自由度带来了一种科学探索上的双刃剑效应。当人类研究者面对一个极其艰难的开放猜想时，常见且健康的推进方式是引入更强的正则性假设、退守到低维特例，或者证明一个带有附加条件的弱化版本。这种松弛往往能揭示核心的技术瓶颈在哪里。但如果在自动化推理中缺乏严密的谱系追踪，语言模型极易产生严重的“目标漂移”：为了让推导得以闭合，智能体可能会在中间步骤隐式引入过于严苛的非平凡假设，或者将原本针对无界分布的结论悄然缩减为紧致支撑集，最终交付一个形式上自洽但实际上已经偏离原科学问题的平庸定理。

现有面向数学的智能体框架普遍无法应对这一挑战。形式化证明系统（如基于 Lean 4 的证明器）虽然能做到绝对严谨，但其运行逻辑建立在“先写好精确的形式化定理陈述，再寻找交互策略”的前提上，无法处理数学规范尚未成型的探索初期。而一般的自然语言多智能体研究系统，虽然具备检索和头脑风暴能力，却往往采用整篇生成的黑盒模式，其长链条数学推导既难以被局部检验，也无法精准定位证明失败究竟源于局部计算代数失误，还是源于定理假设本身的内在矛盾。

VALG 的双工作流：从假设共演到图结构证明

针对上述痛点，VALG 将整个理论研究生命周期明确解构为两个紧密咬合的核心阶段：负责前证明探索与规范确立的 Workflow 1，以及负责依赖图构建与深度审查的 Workflow 2。这种分治设计将“确定我们在证明什么”与“完成严谨推导”进行了机制层面的解耦。

在 Workflow 1（前证明阶段）中，系统并不急于写出第一行推导，而是首先将原始研究简报映射至相关文献脉络，发掘不同的技术切入视角。每一个可行且不重叠的思路，都会被形式化智能体锁死为一个具有数学契约性质的独立分支。这一步至关重要：智能体必须显式固定所有符号体系、原始假设（Primitive Assumptions）、全称与存在量词的作用域、参数渐近体制，以及唯一确定的数学目标。一旦形式化完成，该分支便获得不可随意更改的规范约束，任何后续对假设的修改都不能在当前分支内被隐式掩盖。此外，系统在该阶段设置了交互模式与自主模式的检查点，允许人类专家在分支成型时进行纠偏与筛选。

进入 Workflow 2（证明与审查阶段）后，VALG 摒弃了单体式（Monolithic）的证明生成，转而构建了一套四阶段递进流水线：大纲设计（Sketch）、全局诊断（Global Diagnostic）、局部步进证明（Step）、最终统稿组装（Assembly）。

以往的分步生成方法经常遇到一个致命缺陷：局部的依赖图在拓扑结构上看似完整，但某个前置引理输出的定量界限其实并不足以支撑下游引理的输入需求，或者递归论证无法闭合。VALG 引入的全局诊断阶段便充当了“机制编译器”的角色，在展开费时的局部推导之前，优先排查高难度断言的数学来源、跨引理接口的类型兼容性以及边界极限条件的合法性。只有通过了全局诊断，系统才会沿着拓扑排序逐个生成各个引理的完整局部推导，并最终将其组装为自洽的 LaTeX 论文底稿。

Workflow 1: 视角探索 ──> 符号与假设锁定 ──> 单一目标契约化

                                                     │

                                                     ▼

Workflow 2: 证明大纲 ──> 全局接口诊断 ──> 局部引理推导 ──> 统稿组装

               ▲              │               │              │

               └──────────────┴────── 结构化审查与定向回溯 ───┘

为了确保生成的推导经得起推敲，VALG 配备了四类彼此独立的专业审稿智能体，在组装完成后实施多维盲审：

• 结构审查（Structural Review）：严格比对组装终稿与初始设定，核实所有依赖项是否完全闭合，强制要求排查统稿阶段是否被偷运进了未经声明的额外假设，确保数学自包含性。

• 严谨性审查（Rigor Review）：穿透抽象的引理标签，逐行审查代数变形与推导细节，专门审计量词顺序颠倒、常数依赖关系的漂移、概率收敛模式（如依概率收敛与几乎必然收敛的混淆）以及极限交换的合法性。

• 文献与引用审查（Citation Review）：不仅检查 BibTeX 格式，更逐条核验所引用的经典外部定理在当前设定的特定参数体制下，其前置条件是否已被完全释放（Discharged），杜绝“滥用结论”。

• 对抗性审查（Adversarial Review）：扮演极其挑剔的审稿人角色，针对证明中最薄弱的命题构造边界特例、退化情形、极值体制以及潜在的反例攻击，任何未解决的高风险反例都会直接阻断评审。

最小修复作用域：错误定向与数学血统追踪

任何真实的数学研究都伴随着大量的失败尝试。VALG 区别于传统推理系统最显著的技术特征，在于其具备分级的错误诊断与定向回溯机制（Revision Loops）。当证明过程受到审查阻击时，系统不会机械地全盘推倒重来，而是精确识别阻碍所处的层级，并将其路由至能够修复该缺陷的最小上游阶段。

如果仅仅是局部代数变形出现差错或放缩过松，控制器只会触发局部证明的重写；如果发现中间两个引理之间由于常数因子或范数形式不匹配而无法衔接，则回退至全局诊断或证明大纲进行接口调整。最为关键的是，当对抗性审查或严谨性审查确认当前的定理目标在原始假设下根本不可能成立（即存在内在数学障碍）时，系统绝不允许证明阶段私自添加假设。此时，该阻碍会被定性为“形式化层级阻碍”（Formulation-level Obstruction），并强制回退至 Workflow 1。

在这种机制下，系统会派生出一个与原问题具有明确数学血统关联的新分支——例如一个明确标注的“松弛条件版本”、“受限算法特例”或“条件依存定理”。这种血统跟踪确保了最终产出的科研成果具有极高的透明度：每一个定稿命题都清晰地记录了自身相对于最初科学猜想的演进坐标，彻底杜绝了模型用解决简单平凡特例来冒充攻克重大难题的伪证现象。

实战检验：攻坚 COLT 2026 开放前沿问题

为了验证 VALG 在高难度、非平庸环境下的实际效能，研究团队选取了 COLT 2026 最新公开的 5 篇开放问题论文作为试验场。这些问题涵盖了现代学习理论的核心阵地，包括非凸优化、统计查询复杂度、差分隐私以及在线学习。测试完全使用 GPT-5.6-sol 作为底层基础模型，设置最高推理计算预算，对抽取的 9 个代表性子问题展开端到端独立求解。

在整个实验中，VALG 共产出了 22 个通过了内部多维度严密审查的定理候选。其中，系统在 2 个子问题上直接取得了内部定稿且完全覆盖原题设定范围的完整解；而在其余 7 个子问题上，系统展现出了极高水准的学术严谨性，均在遭遇阻碍后给出了具有明确理论贡献的松弛解、受限算法分析或特例证明，无一出现虚妄的“幻觉证明”。

一个极具代表性的案例来自对张量分解中交替最小二乘法（ALS）与梯度下降（GD）所需过参数化程度的探究。原问题考察由高斯扰动平滑生成的低秩张量分解，关注是否存在某种迭代算法，在使用严格亚二次阶的超参数化秩 $k=o(r^2)$ 时，能在多项式时间内以高概率从随机初始化收敛至全局最优解。

面对这一长期悬而未决的难题，VALG 并没有给出虚假的全面解决宣称，而是精准定位了 Gram 矩阵相干性干扰的技术难点，成功在一个具有合理物理意义的弱干扰与尺度平衡体制下，构造并证明了一个严格亚二次秩的上界定理：

系统形式化了关于基底列范数上下界、累积 Gram 交叉项约束以及尺度敏感平滑界限等一系列技术假设，并设计了结合“可证认证建议机制（Certified Proposal）”、“同步着陆”与“独立重启循环 ALS”的精细算法流水线，成功证明了该算法在上述设定下能以高概率实现任意相对精度的张量重构，并且计算复杂度严格在多项式时间内。对于下界子问题，VALG 则通过投影子空间分析，证明了在特定环境维度 $n \ge 8r^{5/4}$ 和超线性秩体制下受限投影梯度的阻碍性质。这些结果完整展示了从假设引入、机制构造到误差界放缩的全过程，为原论文作者后续彻底解决该开放问题提供了极具参考价值的阶梯。

从做题工具到自主科学发现系统的演进意义

回顾 VALG 的技术构架与实验成果，它的价值不仅在于输出了几篇数学论文草稿，更在于为 AI 介入高阶理论科学探索确立了一套范式规范。

长期以来，学术界对于大模型辅助理论科学研究一直存有深刻的疑虑：一方面担忧其长程逻辑中的幻觉与隐蔽代数错误难以排查，另一方面则警惕其在遭遇逻辑断点时通过弱化命题来进行“偷换概念”。VALG 通过将形式化契约、图结构解耦、对抗性盲审以及血统溯源机制融为一体，向我们展示了严肃的“智能体科学工作流”应当具备的形态。它告诉我们，一个优秀的 AI 理论研究者不仅要擅长在顺境中完成引理推导，更要学会在逆境中识别推导阻碍的真实属性，并诚实、严谨地绘制出通向真理的边界地图。

随着这一框架的开源，理论计算机科学与统计学习领域的研究者正迎来一种新型的研究协作模式：人类学者负责提出宏观猜想、把握科学品味，而智能体系统则可以在严密受控的探索轨道上，自主遍历潜在的形式化路径，筛查反例，构建局部证明网络。从单纯的文献总结到参与前沿难题的攻坚，AI 正在真正步入理论科学创新的深水区。