VALG: An Agentic System for ML Theory Research

Machine learning theory requires coordinating problem formulation, theorem targets, and proof mechanisms across data models, training protocols, oracle access, losses, metrics, and randomness. We investigate whether this process can be organized as an autonomous workflow. We present VALG, an agentic system combining multi-level Verification, Adaptive formulation of Learning-theory problems, and Graph-structured proof development. For each source-relative 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. Failed attempts are routed to derivation-, structure-, or formulation-level repair, with the latter producing explicitly related variants or relaxations. We evaluate VALG on nine subproblems from five COLT 2026 open problems. Two runs yield internally finalized candidates matching their source scopes, while seven yield restricted, special-case, or conditional results. VALG is open source at https://github.com/DechenZhang/VALG-ML-Theory-Agent.