# VALG: An Agentic System for ML Theory Research arXiv: https://arxiv.org/abs/2608.13060 ยท HTML: https://mlsanity.com/paper/2608.13060/ ## Key facts - Cited by 2 papers in the map (data through 14 Oct 2026). - Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use. - Builds on 55 of its 72 references that are in the map. - First posted on arXiv 13 Aug 2026. ## Placed in - LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/) ## Builds on (most cited first, 30 of 55) - [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022) - [Reflexion: Language Agents with Verbal Reinforcement Learning](https://mlsanity.com/paper/2303.11366/) (2023) - [Self-Refine: Iterative Refinement with Self-Feedback](https://mlsanity.com/paper/2303.17651/) (2023) - [The AI Scientist: Towards Fully Automated Open-Ended Scientific Discovery](https://mlsanity.com/paper/2408.06292/) (2024) - [AlphaEvolve: A coding agent for scientific and algorithmic discovery](https://mlsanity.com/paper/2506.13131/) (2025) - [MLE-bench: Evaluating Machine Learning Agents on Machine Learning Engineering](https://mlsanity.com/paper/2410.07095/) (2024) - [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023) - [Agent Laboratory: Using LLM Agents as Research Assistants](https://mlsanity.com/paper/2501.04227/) (2025) - [Accelerating scientific discovery with Co-Scientist](https://mlsanity.com/paper/2502.18864/) (2025) - [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021) - [MLAgentBench: Evaluating Language Agents on Machine Learning Experimentation](https://mlsanity.com/paper/2310.03302/) (2023) - [PaperBench: Evaluating AI's Ability to Replicate AI Research](https://mlsanity.com/paper/2504.01848/) (2025) - [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025) - [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022) - [ScienceAgentBench: Toward Rigorous Assessment of Language Agents for Data-Driven Scientific Discovery](https://mlsanity.com/paper/2410.05080/) (2024) - [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024) - [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022) - [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023) - [RE-Bench: Evaluating frontier AI R&D capabilities of language model agents against human experts](https://mlsanity.com/paper/2411.15114/) (2024) - [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024) - [CORE-Bench: Fostering the Credibility of Published Research Through a Computational Reproducibility Agent Benchmark](https://mlsanity.com/paper/2409.11363/) (2024) - [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023) - [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023) - [Lean-STaR: Learning to Interleave Thinking and Proving](https://mlsanity.com/paper/2407.10040/) (2024) - [Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics](https://mlsanity.com/paper/2601.14027/) (2026) - [Towards Autonomous Mathematics Research](https://mlsanity.com/paper/2602.10177/) (2026) - [Multilingual Mathematical Autoformalization](https://mlsanity.com/paper/2311.03755/) (2023) - [Automated Conjecture Resolution with Formal Verification](https://mlsanity.com/paper/2604.03789/) (2026) - [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025) - [ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization](https://mlsanity.com/paper/2510.15981/) (2025) ## Built on by (most cited first, 2 of 2) - [Non-Adaptive 1-Bit Mean Estimation: Minimax Rates and the Sample-Interval Tradeoff](https://mlsanity.com/paper/2609.08564/) (2026) - [TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science](https://mlsanity.com/paper/2609.35606/) (2026) ## Abstract (arXiv) 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.