VALG: An Agentic System for ML Theory Research
Dechen Zhang, Xuan Tang, Xinxiang Yin, Xingwu Chen, Jian Qian, Difan Zou
cs.AI, cs.LG, math.OC, stat.ML
2026-08-13
多智能体系统 VALG 把理论证明拆成依赖 DAG 加分层审查,在 9 道 COLT 2026 子问题上完整解出 2 道,定稿 22 个定理候选。
ML 理论的开放题与「证明这条定理」不是一回事。COLT 2026 公开征集的题目通常只点名一个学习现象,哪个模型类、哪种数据假设、哪个渐近 regime 下定理既成立又有信息量,要研究者自己定;问题形式化、定理目标、证明机制三者一起演化。现有自动定理证明系统默认题目已经良定,直接进证明搜索;丢给开放题,典型的失败不是证不出来,是悄悄把目标换成一个更容易的变体,再当作原题已解来汇报。
VALG(香港大学牵头)把这个过程组织成自治工作流,核心约束是每条定理分支与原题的数学关系必须显式:完整解、松弛、特例、条件定理、被卡住,五种结局分开报告,不许混。
系统分两个工作流。
Workflow 1(证明前)做问题形式化。文献调研把已有工作分成直接理论来源、基础理论框架、经验实践三层找 gap;视角选择器开出至多 3 个并行分支,每个视角是一个五元组(分析目标、模型类、数据假设、regime、算法);分支内的想法生成器只能收窄五元组、不能放宽,形式化后产出「定理合同」:符号、原始假设、量词,外加恰好一个数学目标。这些是开放性的科学判断,Workflow 1 设了人类专家 checkpoint,也保留全自动 autopilot 模式。
Workflow 2(证明与审查)走 sketch-global-step-assembly 四段。sketch 把论证写成带类型的依赖 DAG:源节点是原始假设,中间节点是引理级命题,唯一汇点是目标定理,每个节点记录精确声明、依赖、允许假设与输出接口。global 阶段做整定理级诊断,查量级依赖、概率与收敛模式、对象兼容性、边界行为、局部接口能否组合。这一步的存在理由很具体:依赖图结构自洽不代表定理级可组合,上游给代理对象证的界推不出下游要的原始目标的界。step 按依赖序逐节点写局部证明,assembly 汇成自洽的 LaTeX 稿件。
审查与生产分离:sketch、global、step 各配独立 reviewer,assembly 过结构、严谨性、引用、对抗四路专项终审加一路聚合终审,接受门槛是总分不低于 7 且无 blocker。失败后的重试按定位路由:先诊断障碍在局部推导、证明结构还是定理表述,控制器把一次 scoped 重试发给能修的最小层级(assembly、step、sketch、idea 逐级),重试预算耗尽就升级。只有表述级障碍才触发变体或松弛,且必须声明与原题的关系。
5 篇 COLT 2026 开放题论文的 9 个子问题,骨干 GPT-5.6-sol(最大推理力度),9 次运行定稿 22 个定理候选。进展度 P = min{C+B+H, 上限}:C∈[0,4] 计目标合同封闭度,B∈[0,3] 计相对原基线的改进,H∈[0,3] 计卸下的开放负担;假设了中心未解性质的定理封顶 3 分,只证了刻画一面的封顶 7 分。
| 子问题 | 最好进展 | 结局 |
| 1-bit 均值估计(非自适应) | P=10 | 完整解:全预承诺协议达到自适应 minimax 速率 |
| 线上优化 Pfaffian 边界 | P=10 | anchored 归一化下的充要刻画,归一化普适性仍开放 |
| 其余 7 个(tensor ALS、深度 vs 线性、私有 PAC 等) | 2.256.50 | 受限方法结果、特例或条件定理 |
1-bit 那条是硬结果:在无约束中心 k 阶矩类上构造出完全预承诺的非自适应 1-bit 协议,样本数不超过 Ck·rk(自适应 minimax 速率),配合已知 1-bit 下界即为阶最优。Pfaffian 那条的满分带限定,作者明说完整进展只在「声明的 anchored 单位区间归一化」下成立,原始 Pfaffian 表示是否都能以多项式参数预算归入该归一化是开放的。耗时上,单分支从 8 小时到 91 小时不等,tensor ALS 上界分支跑 76 小时拿到 6.50。
对做 agent 的人,这篇的价值不在「AI 会证定理了」,在两个可迁移的工程决策。其一,目标漂移成为显式管理对象:任何松弛、变体都必须携带与原题的数学关系,这个约束对所有长程研究 agent 都成立,实验型智能体同样会在「换个好测的指标」上漂移。其二,生产者与审查者分离、失败按抽象层级路由,可维护性来自结构而非模型聪明。
对理论圈,7 个部分进展本身也是产出:每个子问题卡在推导、结构还是表述,被归档得清清楚楚,证明与代码开在 GitHub 上,可以当开放题的进展索引用。
作者自列三条:AI 生成的证明过度使用记号、偏离人类证明写作惯例,推高专家验证成本;缺带已知解的 ML 理论 benchmark,做不了受控评估;面向 ML 理论的概率、优化、信息论证明模式,现有形式化工具还不完整。
更大的存疑在验证环节:22 个候选的把关是「独立多视角 LLM 审查 + 粗略人工审计」,没有证明器背书,作者也明说正确性可能还需更多专家、尤其是开放题原作者核验;两个「完整解」在文中的地位是内部定稿,不是社区确认的解答。另外全部 case 只用了 GPT-5.6-sol 一个骨干,方法对模型能力的依赖没有消融,人类 checkpoint 与 autopilot 的差异也没有对照实验。