VALG：面向机器学习理论研究的Agentic系统

机器学习理论通过数学设定来研究学习过程，其中数据模型、训练协议、oracle访问、损失、度量与随机性共同定义了定理所要解释的现象。因此，解决一个公开问题需要问题形式化、定理目标与证明机制协同发展。研究者提出假设，通过初步的理论或实证分析加以检验，并同时打磨假设与证明。我们研究这一过程能否被组织为面向机器学习理论研究的自主agentic工作流。我们开发了VALG，一个结合多层验证（Verification）、学习理论问题自适应形式化（Adaptive formulation）与图结构证明开发（Graph-structured proof development）的agentic系统。在每个相对于源问题的定理分支内，VALG维护固定的数学规范，检查类型化证明依赖图在定理层面的组合，并按依赖顺序构建与审查局部证明。当一次证明尝试失败时，VALG判断障碍出在推导、证明结构还是定理形式化，并据此路由下一次尝试。形式化层面的障碍会触发显式相关的变体或松弛，从而保持所得定理与源问题之间的数学联系。我们在来自五个COLT 2026公开问题的九个子问题上评估VALG。两次运行产出了与其源问题简报范围匹配的内部定稿定理候选；其余七次给出受限方法结果、特殊情形或条件定理。这些案例研究展示了VALG如何使源范围匹配、松弛、条件结果与受阻尝试在数学上保持清晰区分。VALG已开源于 https://github.com/DechenZhang/VALG-ML-Theory-Agent。