VALG: An Agentic System for ML Theory Research

• URL: http://arxiv.org/abs/2608.13060v1
• Date: Thu, 13 Aug 2026 10:23:11 GMT
• Title: VALG: An Agentic System for ML Theory Research
• Abstract summary: We develop VALG, an agentic system that combines multi-level Verification, Adaptive formulation of Learning-theory problems, and Graph-structured proof development.<n>We evaluate VALG on nine subproblems from five COLT 2026 open problems.
• Score: 35.29223690479372
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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 papers

• A Formalization of the Mean-Field Derivation of the Vlasov Equation: AI-Assisted Lean Formalization as a Strategy Game [0.0]
  We formalize a research result in the Lean 4 proof assistant by having a mathematician direct an AI system, and frame the activity as a formalization game.<n>The objective is to turn a document into Lean. The game is won when the development compiles, contains no sorry, and a machine check shows the target theorems rest on Lean's foundational axioms alone.<n>The case study is a complete, axiom-clean formalization of well-posedness for the nonlinear Vlasov equation via Dobrushin's mean-field route.
  arXiv  Detail & Related papers  (2026-07-09T23:17:54Z)
• Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory [17.20738506776148]
  Asymptotic statistical theory is a challenging domain for AI-assisted formalization.<n>We propose a hypothesis-disciplined Lean 4 formalization pipeline built from multiple agents.<n>The resulting Lean development is axiom-clean and source-faithful.
  arXiv  Detail & Related papers  (2026-06-03T20:03:38Z)
• A Theoretical Framework for Self-Play Theorem Proving Algorithms [7.702779307300836]
  We provide a theoretical framework for understanding the self-improvement capabilities of self-play algorithms for theorem proving.<n>We show that if the underlying graph of theorems is well-connected, then a prover-conjecturer system, where the conjecturing algorithm is based on a reversible random walk, is sufficient to grow the set of proved theorems exponentially.
  arXiv  Detail & Related papers  (2026-06-01T08:12:47Z)
• Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models [8.948475969696075]
  Agentic theorem provers are pipelines that couple a mathematical reasoning model with library retrieval, subgoal-decomposition/search planner, and a proof assistant verifier.<n>We propose a distributional viewpoint and introduce provability, defined as the finite-horizon success probability of reaching a verified proof.<n>We provide a principled, component-sensitive explanation of when and why agentic theorem provers succeed on biased real-world problem distributions.
  arXiv  Detail & Related papers  (2026-02-11T05:22:24Z)
• Solving Inequality Proofs with Large Language Models [42.667163027148916]
  Inequality proving is crucial across diverse scientific and mathematical fields.<n>This makes it a demanding frontier for large language models (LLMs)<n>We release IneqMath, an expert-curated dataset of Olympiad-level inequalities.
  arXiv  Detail & Related papers  (2025-06-09T16:43:38Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheorem is a comprehensive informal theorem-proving framework exploiting natural language to enhance mathematical reasoning.<n>DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs.<n>We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference.
  arXiv  Detail & Related papers  (2025-05-29T17:59:39Z)
• Graph Stochastic Neural Process for Inductive Few-shot Knowledge Graph Completion [63.68647582680998]
  We focus on a task called inductive few-shot knowledge graph completion (I-FKGC) Inspired by the idea of inductive reasoning, we cast I-FKGC as an inductive reasoning problem. We present a neural process-based hypothesis extractor that models the joint distribution of hypothesis, from which we can sample a hypothesis for predictions. In the second module, based on the hypothesis, we propose a graph attention-based predictor to test if the triple in the query set aligns with the extracted hypothesis.
  arXiv  Detail & Related papers  (2024-08-03T13:37:40Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof.<n>Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  Large language models (LLMs) have shown promise in proving formal theorems using proof assistants such as Lean. Existing methods are difficult to reproduce or build on, due to private code, data, and compute requirements. This paper introduces LeanDojo: an open-source Lean toolkit consisting of toolkits, data, models. We develop ReProver: an LLM-based prover augmented with retrieval for selecting premises from a vast math library.
  arXiv  Detail & Related papers  (2023-06-27T17:05:32Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  We learn a neural generator that automatically synthesizes theorems and proofs for the purpose of training a theorem prover. Experiments on real-world tasks demonstrate that synthetic data from our approach improves the theorem prover.
  arXiv  Detail & Related papers  (2020-02-17T16:06:02Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.