发表机构
The University of Hong Kong; Shenzhen Loop Area Institute; Northwestern Polytechnical University（香港大学; 深圳河套学院; 西北工业大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出VALG智能体系统，将机器学习理论研究过程组织为自主工作流，通过多环节验证与图结构证明开发，在COLT 2026开放问题子问题上验证了其有效性，相关代码已开源。
AI 中文摘要
机器学习理论通过数学框架研究学习过程，其中数据模型、训练协议、神谕访问、损失函数、度量指标和随机性共同构成了定理需要解释的现象。解决开放问题需要同步推进问题表述、定理目标和证明机制的开发。研究人员会提出假设，通过初步理论或实证分析进行检验，并不断修正假设和证明。本文探究该过程能否组织为面向机器学习理论研究的自主智能体工作流，开发了VALG系统，该系统结合了多级验证、学习理论问题的自适应表述以及图结构证明开发。在每个源相关定理分支中，VALG维护固定的数学规范，检查类型化证明依赖图的定理级组合，并按依赖顺序构建和审查局部证明。当证明尝试失败时，VALG会识别障碍是出在推导过程、证明结构还是定理表述中，并据此安排下一次尝试。表述级障碍会触发明确相关的变体或松弛，同时保留所得定理与源问题之间的数学关系。我们在COLT 2026的5个开放问题的9个子问题上对VALG进行评估，其中2次运行产生了与源问题范围匹配的内部最终定理候选，其余7次产生了受限方法结果、特殊情况或条件定理。这些案例研究表明VALG能在数学上区分源范围匹配、松弛、条件结果和受阻尝试。VALG为开源项目，网址为this https URL。
英文摘要
Machine learning theory studies learning procedures through mathematical setups in which the data model, training protocol, oracle access, loss, metric, and randomness define the phenomenon that a theorem is meant to explain. Solving an open problem therefore requires the problem formulation, theorem target, and proof mechanism to be developed in concert. Researchers formulate hypotheses, test them through preliminary theoretical or empirical analysis, and refine both assumptions and proofs. We investigate whether this process can be organized as an autonomous agentic workflow for ML theory research. We develop VALG, an agentic system that combines multi-level Verification, Adaptive formulation of Learning-theory problems, and Graph-structured proof development. Within each source-relative theorem branch, VALG maintains a fixed mathematical specification, checks the theorem-level composition of a typed proof-dependency graph, and constructs and reviews local proofs in dependency order. When a proof attempt fails, VALG identifies whether the obstruction lies in a derivation, the proof structure, or the theorem formulation and routes the next attempt accordingly. Formulation-level obstructions initiate an explicitly related variant or relaxation, preserving the mathematical relation between the resulting theorem and the source problem. We evaluate VALG on nine subproblems from five COLT 2026 open problems. Two runs produce internally finalized theorem candidates that match the scope of their source briefs; the remaining seven yield restricted-method results, special cases, or conditional theorems. These case studies show how VALG keeps source-scope matches, relaxations, conditional results, and blocked attempts mathematically distinct. VALG is open source at https://github.com/DechenZhang/VALG-ML-Theory-Agent.
