VALG: An Agentic System for ML Theory Research
Abstract
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.
Related
- Solver Agent: an Agentic AI Framework for Theoretical Physics Computations Applied to F-theory Uplifts of O3-planes and S-folds
- CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference
- Approximation Theory of Laplacian-Based Neural Operators for Reaction-Diffusion System
- Torus Bifurcation in the Hopf-Langford type system through Averaging Theory
- From Formulation to Articulation: Considerations for AI-Assisted Research in Information Theory
BibTeX
@misc{zhang2026valg,
title = {{VALG: An Agentic System for ML Theory Research}},
author = {Dechen Zhang and Xuan Tang and Xinxiang Yin and Xingwu Chen and Jian Qian and Difan Zou},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2608.13060},
eprint = {2608.13060},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2608.13060},
}
RIS
TY - UNPB
TI - VALG: An Agentic System for ML Theory Research
AU - Dechen Zhang
AU - Xuan Tang
AU - Xinxiang Yin
AU - Xingwu Chen
AU - Jian Qian
AU - Difan Zou
PY - 2026
DA - 2026/09/10
PB - arXiv
DO - 10.48550/arxiv.2608.13060
UR - https://arxiv.org/abs/2608.13060
AB - 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.
ER -