VALG: An Agentic System for ML Theory Research

TL;DR - VALG is an autonomous agentic workflow for formulating and proving machine-learning theory results. It matters because it explicitly distinguishes complete source-aligned theorems from relaxations, conditional findings, special cases, and failed attempts.

• Uses multi-level verification, adaptive problem formulation, and graph-structured proof development.
• Maintains fixed mathematical specifications and typed proof-dependency graphs within each theorem branch.
• Diagnoses failures as derivation, proof-structure, or theorem-formulation problems and routes retries accordingly.
• Across nine COLT 2026 subproblems, two runs finalized source-aligned theorem candidates; seven produced restricted, special-case, or conditional results.