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 turns ML theory research into a multi-agent proof workflow; on nine COLT 2026 open subproblems it fully solves two with GPT-5.6, producing 22 theorem candidates.
An ML theory open problem is not a ready-made theorem statement. A COLT 2026 problem usually names a learning phenomenon and leaves open which model class, data assumption, or asymptotic regime makes a theorem both true and informative; formulation, target, and proof technique evolve together. Existing automated theorem provers assume a well-posed statement and go straight to proof search. On open problems their characteristic failure is not failing to prove but silently swapping the target for an easier variant and reporting it as solved.
VALG, led by a University of Hong Kong team, organizes the process as an autonomous workflow with one governing constraint: every theorem branch must carry an explicit mathematical relation to the source problem, and full matches, relaxations, special cases, conditional theorems, and blocked attempts are reported as distinct outcomes.
Two workflows.
Workflow 1 (pre-proof) does problem formulation. A literature survey splits prior work into direct theory, foundational frameworks, and empirical practice; a perspective selector opens at most 3 parallel branches, each a 5-tuple (analysis target, model class, data assumption, regime, algorithm); an idea generator inside each branch may only narrow the tuple, never broaden it; a formalizer then emits a theorem contract: notation, primitive assumptions, quantifiers, and exactly one mathematical goal. These are open-ended scientific calls, so Workflow 1 has human-expert checkpoints, with an autopilot mode also available.
Workflow 2 (proof and review) is a sketch-global-step-assembly pipeline. The sketch encodes the argument as a typed dependency DAG: source nodes are primitive assumptions, internal nodes are lemma-sized claims, the unique sink is the target theorem, and each node records its exact claim, dependencies, allowed assumptions, and required output interface. A whole-theorem global diagnostic then checks quantitative dependence, probability and convergence modes, object compatibility, boundary behavior, and whether local interfaces compose. The reason this stage exists is concrete: a structurally consistent dependency graph does not guarantee theorem-level composability, and a bound proved for a surrogate object upstream does not imply the bound on the original target that a downstream node needs. Steps are proved in dependency order and assembled into a self-contained LaTeX manuscript.
Review is layered and independent of production: dedicated reviewers after sketch, global, and step, then four specialized final reviews at assembly (structural, rigor, citation, adversarial) plus an aggregate reviewer; acceptance requires a score of at least 7 with no blockers. Failed attempts route by localization: reviewers diagnose whether the obstruction is a local derivation, the proof structure, or the formulation itself, and the controller sends one scoped retry to the smallest stage that can repair it (assembly, then step, then sketch, then idea), with retry budgets and escalation. Only formulation-level obstructions open a variant or relaxation, and the relation to the source problem must be declared.
Nine subproblems from five COLT 2026 open-problem papers, run on GPT-5.6-sol at maximum reasoning effort. Across nine runs VALG finalized 22 theorem candidates; 2 of the 9 subproblems were fully solved (progress P = 10) and 7 yielded restricted-method results, special cases, or conditional theorems. Progress is P = min{C+B+H, cap}, with C in [0,4] for closure of the target contract, B in [0,3] for improvement over the problem baseline, and H in [0,3] for share of the open burden discharged; theorems assuming a central open property are capped at 3 and one-directional characterizations at 7.
The strongest result is 1-bit mean estimation: fully pre-committed non-adaptive protocols over the unrestricted central-k-moment class achieving at most a constant times the adaptive minimax rate, order-optimal with the known lower bound. The Pfaffian online-optimization result carries an explicit qualifier: full progress holds under a declared anchored unit-range normalization, and whether every raw Pfaffian presentation admits that normalization with polynomial parameter budgets stays open. Branch wall-clock ranges from 8 to 91 hours; the tensor-ALS upper-bound branch ran 76 hours and scored 6.50.
For agent builders the value is not "AI can prove theorems now" but two transferable engineering decisions. First, goal drift becomes an explicitly managed object: any relaxation must carry its mathematical relation to the source question, a constraint that holds for any long-horizon research agent, including experimental ones that drift toward easily measured metrics. Second, producer and reviewer separation with failure routing by abstraction level: maintainability comes from structure, not from model cleverness.
For theorists, the seven partial results are themselves a deliverable: where each subproblem got stuck, in derivation, structure, or formulation, is archived, with proofs and code on GitHub, usable as an index of open-problem progress.
The authors list three: AI-generated proofs overuse notation and deviate from human proof-writing conventions, raising expert verification cost; there is no ML-theory benchmark with known solutions for controlled evaluation; and formalization tooling is incomplete for the probability, optimization, and information-theoretic patterns ML theory relies on.
The larger caveat is verification: all 22 candidates were gated by independent multi-perspective LLM review plus a rough human audit, not by a proof assistant, and the authors themselves note that correctness may need verification by more experts, especially the open problems' authors. The two fully solved subproblems are internally finalized, not community-confirmed. Everything runs on a single backbone (GPT-5.6-sol) with no ablation of model dependence, and there is no controlled comparison between the interactive and autopilot modes.