Pith. sign in

REVIEW 3 major objections 5 minor 80 references

VALG: An Agentic System for ML Theory Research

T0 review · 3 major / 5 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read An agentic system called VALG organizes ML theory research as source-relative theorem development and, on nine subproblems from five COLT 2026 open problems, produces two finalized theorem candidates that match the full scope of their…

desk verdict A well-engineered agentic pipeline for ML theory exploration whose two headline 'full-scope solutions' rest on internal LLM self-review rather than a checkable mathematical artifact. read the letter →

arxiv 2608.13060 v1 pith:RJNJ4CZJ submitted 2026-08-13 cs.AI cs.LGmath.OCstat.ML

Dechen Zhang , Xuan Tang , Xinxiang Yin , Xingwu Chen , Jian Qian , Difan Zou This is my paper · ORCID
classification cs.AIcs.LGmath.OCstat.ML MSC 68Q32
keywords agentictheoremdevelopmentmachinelearningtheoryopenproblemsproofdependencygraphLLMverification1-bitmeanestimationdifferentialprivacyPACtensordecomposition
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper claims that open machine-learning theory research can be organized as an autonomous agentic workflow in which problem formulation, theorem target, and proof are developed together while the relation to the original question is preserved. The proposed system, VALG, fixes a mathematical specification per branch, represents the proof as a typed dependency graph, and routes failures to the derivation, the proof structure, or the theorem formulation; only formulation-level obstructions open a new, explicitly related variant. On nine subproblems from five COLT 2026 open problems, two runs produced internally finalized theorem candidates that match the full scope of their source briefs—non-adaptive order-optimal one-bit mean estimation and an anchored Pfaffian anti-concentration bound—while the other seven runs yielded restricted-method results, special cases, or conditional theorems. A sympathetic reader would take this as evidence that a structured agent, with strong LLM reviewers and human audit, can produce useful mathematical outcomes while honestly labeling partial progress.

What carries the argument

The load-bearing object is the source-relative theorem branch with its fixed theorem contract (notation, primitive assumptions, quantifiers, regime, exactly one goal), carried through a typed proof-dependency DAG from primitive assumptions through lemma-sized nodes to the target. The four-stage pipeline—sketch, global theorem-level diagnostic, local step proofs, assembly—plus independent reviewers (structural, rigor, citation, adversarial, then an aggregate) provide verification; failure-localized routing sends derivation flaws back to the step producer, graph flaws back to the sketch, and formulation obstructions to a new variant branch. The progress measure $P = \min\{C+B+H, \mathrm{cap}\}$, with caps for missing central quantifiers or assumed properties, formalizes what counts as full coverage versus partial progress.

What would settle it

Have an independent expert or a formal proof assistant verify the two full-scope candidates, Theorem 4.6 (fully non-adaptive one-bit mean estimation) and Theorem 4.13 (anchored Pfaffian sweep); a single invalid inequality at the localization-to-refinement interface or the projective-speed bound would refute the claim that the system produced full-scope solutions.

Watch

Extended reading notes

Core claim

On its own terms, the paper's central claim is that a source-relative theorem-development architecture can turn open ML-theory questions into mathematically categorized outcomes. Each branch fixes one theorem contract, checks theorem-level composition of a typed proof-dependency graph, and constructs local proofs in dependency order; when a proof attempt fails, the system localizes the cause and routes the smallest repair. Across nine subproblems the system produced twenty-two internally finalized theorem candidates: two match the source scope exactly (the order-optimal fully non-adaptive one-bit mean estimation protocol over the central-k-moment class, and the anchored coefficient-normalized Pfaffian sweep bound with explicit polynomial dependence on degree and radius), and the other seven are restricted-method results, special cases, or conditional theorems. The paper treats the two full-scope matches as conditional on internal verification plus rough human audit, and the weaker outcomes as mathematically distinct achievements that remain tied to their source problems.

Load-bearing premise

The whole evaluation rests on trusting the system's own LLM reviewers and a rough human audit; if those reviewers approve invalid proofs, the two claimed full-scope results are not established.

Editorial extensions

If this is right

  • If the two full-scope candidates are correct, fully non-adaptive one-bit protocols match the adaptive minimax sample complexity for the central-k-moment family, so interaction is not needed for order-optimal 1-bit mean estimation.
  • The anchored normalization result for Pfaffian boundaries gives a finite, explicit anti-concentration constant with polynomial dependence on degree and radius, and recovers the monic polynomial case exactly, suggesting a normalization principle for coefficient classes.
  • The remaining seven outcomes, being explicitly classified as restricted-method, special-case, or conditional, show that the architecture can deliver partial progress without silently replacing the source problem.
  • The failure-localized revision hierarchy means an unresolved proof can be escalated through derivation, graph, formulation, and then a source-related variant, making the reason for each relaxation auditable.
  • The separation of human-checkpoint design from contract-based agent review indicates that open-ended problem selection and proof checking can be given different verification regimes in one workflow.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • My inference: if the two full-scope candidates survive independent expert or formal verification, the same source-relative branch structure could serve as a general protocol for attacking open problems in learning theory, with the failure taxonomy acting as a map of why each source problem is hard.
  • My inference: the explicit cap formula for progress suggests a testable benchmark metric for future theorem-generation agents: any candidate should be scored not only by theorem correctness but by its source-relative scope class, which would penalize silent target switching.
  • My inference: a controlled experiment with known-solution theorems in the same five areas would isolate whether failure-localized routing, rather than the underlying LLM, is what improved outcomes.
  • My inference: the Pfaffian anchored normalization result points to a possible general normalization condition for any Pfaffian presentation—existence of a literal unit anchor and bounded chain—that, if always achievable with polynomial budgets, would settle the source problem's finiteness question.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper introduces VALG, an agentic workflow for machine-learning-theory research that separates problem formulation from proof development, represents proofs as typed dependency graphs, and routes failures to derivation, structure, or formulation-level repairs. The system is evaluated on nine subproblems drawn from five COLT 2026 open problems. The authors report that two runs produced internally finalized theorem candidates matching the full scope of their source subproblems (Theorems 4.5 and 4.6 in one-bit mean estimation), while the other seven runs produced restricted-method results, special cases, or conditional theorems. The paper presents the workflow, a progress metric P, a soundness metric S, and a novelty metric N, and it includes per-perspective case-study summaries with statements of assumptions and theorem conclusions.

Significance. If the two full-scope claims were independently verified, this would be a notable demonstration that an agentic system can generate plausible, source-faithful theorem candidates for open problems in ML theory, and the source-relative taxonomy of full-scope, relaxation, conditional, and blocked outcomes is a useful organizational contribution to the emerging literature on AI research agents. The paper is also transparent about its limitations: it ships open-source code and case-study logs, it explicitly distinguishes weaker outcomes from full-scope matches, and it concedes in Section 5 that expert verification is costly and that formalization remains open. Those strengths are real. However, the paper's central empirical claim rests on proof artifacts that are not present in the manuscript and on acceptance decisions made by the system's own LLM reviewers, so the significance is conditional pending external verification.

major comments (3)
  1. [§4 and Theorems 4.5/4.6; footnote 3] The central claim that two subproblems are "fully solved" is not supported by the evidence in the manuscript. The proofs of Theorems 4.5 and 4.6 are not included; Section 4 states only that the candidates were "checked through independent multi-perspective LLM reviewing and roughly audited by human," and footnote 3 concedes that "the correctness of the proof may also need to be verified by more experts." Because the theorems are long probabilistic constructions with nested confidence events, precommitted masks, and level-dependent weights, a rough human audit is not a substitute for a checkable proof. The authors should either include complete proofs in the paper or supplementary material, provide an independent verification (e.g., formalization or expert sign-off), or reframe the claims as "candidate theorems pending verification" throughout the abstract, introduction, and Section 4.
  2. [§4, Table 1 and the definition of P] The evaluation is circular in a load-bearing way. The progress score P = min{C+B+H, cap} is assigned by "a distinct agent" within VALG, and the final verdicts come from the aggregate reviewer, all of which run on the same underlying model (GPT-5.6-sol) as the producers. The conclusion that two of nine runs "fully solved" their subproblems is therefore the system's assessment of its own outputs, not an external ground truth. The manuscript needs an external evaluation component: for instance, human-expert scoring of the candidates, a comparison against known baselines, or a formal acceptance criterion. Without this, the demonstration is a process log rather than an established result about the open problems.
  3. [§4.2, Assumptions 4.25–4.31 and the reliance on Lau and Scarlett (2026b, Theorem 16)] Theorems 4.5 and 4.6 both invoke Lau and Scarlett (2026b, Theorem 16) as a localization primitive that is claimed to be fully non-adaptive with precommitted union-of-cell queries. Since the cited work is titled "Order-optimal sequential 1-bit mean estimation," the manuscript must make explicit that Theorem 16 indeed provides a precommitted, non-adaptive query bank rather than an adaptive protocol; the current text only asserts this. This is a concrete correctness risk for the main full-scope claims, and the authors should quote or verify the exact statement and hypotheses of Theorem 16 in the setting used here.
minor comments (5)
  1. [§4.2] The subsection presents only Perspective 1 and Perspective 3, but Table 1 lists three perspective branches for the non-adaptive one-bit mean estimation subproblem; the missing Perspective 2 should either be included or explicitly noted as not finalized.
  2. [§3.3] The revision-loop diagram in the text is garbled: "proof assembly→proof step→proof sketch→idea / global proof↗" is not readable as a hierarchy and should be rendered as a proper figure or list.
  3. [§4.1] In the subproblem 1 open question, the notation "r < k = o(r^2)" is ambiguous; it should be written as k = k(r) with r < k(r) and k(r) = o(r^2).
  4. [§4, first paragraph] The sentence "Finalized theory candidates have been checked through independent multi-perspective LLM reviewing and roughly audited by human" should specify what the human audit covered, how many auditors were involved, and which candidates were audited.
  5. [§5] The limitation stated in footnote 3 (that proof correctness still needs expert verification) is important enough to be moved into the main text of the conclusion, especially given the "fully solved" wording used earlier.

Circularity Check

1 steps flagged · score 6.0 of 10

The 'fully solved' outcome is defined by VALG's internal progress score and aggregate reviewer, so the central demonstration reduces to self-assessment rather than independent verification.

  1. self definitional [Section 4, introductory paragraph and Table 1 caption; footnote 3]
    "Results show that two of nine subproblems are fully solved while the remaining seven subproblems are partially solved. ... Progress P∈[0,10] is evaluated against the original paper’s subproblem by a distinct agent. ... Finalized theory candidates have been checked through independent multi-perspective LLM reviewing and roughly audited by human. (Footnote: The correctness of the proof may also need to be verified by more experts, especially the authors of these open-problem papers.)"

    The paper's central demonstration — that VALG solved two COLT subproblems in full scope — is not supported by an external proof check. 'Fully solved' is the value P=10 assigned by a VALG-internal 'distinct agent' using the rubric P=min{C+B+H, applicable cap}, and 'finalized' is a status conferred by VALG's aggregate final review. The conclusion therefore reduces, by construction, to the system's own evaluation: a candidate is counted as fully solving its subproblem when VALG's reviewers score it so. The footnote concedes that proof correctness still requires expert verification, confirming that the only evidence offered is the pipeline's self-assessment.

full rationale

The paper transparently labels most outcomes as 'internally finalized', 'partial progress', or 'conditional', and the theorem candidates are presented as such, which limits the circularity to the evaluation layer. However, the headline conclusion 'two of nine subproblems are fully solved' extends beyond the internal label: it is generated by the same pipeline that produced the candidates, via a progress score P computed by a 'distinct agent' inside VALG and a finalization verdict from VALG's aggregate reviewer. Table 1 reports P and ranks computed by VALG agents; no Lean/Coq formalization, independent expert proof check, or reproduction is supplied. Footnote 3 explicitly states the correctness of the proofs still needs verification by more experts. Thus the central demonstration — that the system achieves full-scope solutions — is equivalent to the system's own certification of its outputs. This is not a mathematical derivation that reduces an equation to an input, but it is a self-evaluative loop: the observed 'fully solved' status is defined as the system's internal verdict. No other circularity was found: Theorems 4.5 and 4.6 legitimately import the external Lau–Scarlett localizer, and the conditional/partial theorems are standard assumption–conclusion statements whose proofs are not included but are not claimed to follow from their conclusions. Score 6 reflects one load-bearing self-assessment step that makes the headline result depend on the system's own evaluation.

Assumptions & free parameters 3 free parameters · 4 assumptions · 2 invented entities

The paper's case-study theorems carry many hand-chosen constants and outcome-dependent certificate conditions. The central claim about system efficacy additionally depends on trusting the system's own reviewers, which is an unverified process assumption.

free parameters (3)
  • k = C_rank r^(5/3) (log r)^(5/2) = C_rank unspecified (universal constant)
    Proposal rank in Theorem 4.1 is chosen to make the probability bound Theta(r^{-5/3}(log r)^{-3/2}) work; the constant is asserted to exist but not numerically fixed.
  • q* = 1/4096 = 1/4096
    Interference threshold chosen by hand in the tensor upper-bound setup; appears in Assumptions 4.2 and 4.5.
  • Progress metric weights and caps (P = min{C+B+H, cap}) = C in [0,4], B in [0,3], H in [0,3], caps 3 and 7
    The evaluation metric is a hand-designed scoring rule with hand-set caps; the scores are assigned by the system's own distinct agent.
assumptions (4)
  • ad hoc to paper LLM-based reviewers can reliably detect invalid derivations and hidden assumptions
    Workflow 2 uses independent agent reviewers to accept or route proof artifacts; the paper provides no benchmark showing these reviewers catch errors.
  • domain assumption COLT 2026 open problems are accurately represented by the research briefs
    The subproblems are extracted from source papers; misrepresentation would invalidate the scope-matching claims.
  • domain assumption Lau and Scarlett (2026b) Theorem 16 balanced-code localizer is correct and applicable
    The 1-bit mean estimation results (Theorems 4.5 and 4.6) rely on this black-box component.
  • standard math Standard learning-theoretic background (PAC, SQ, DP, online learning) is used without proof
    The case-study theorems invoke standard definitions and results from the cited literature without deriving them.
invented entities (2)
  • Trajectory certificate C_2(delta, L_P, zeta, C_T)
    purpose: Outcome-dependent condition that guarantees positive limiting loss in Theorem 4.3
    The certificate is defined in terms of the trajectory itself (initial deficit, projector path length, smoothing scale), so it is not a falsifiable prediction.
  • Finite-path event C_path
    purpose: Controls total movement of balanced GD in Theorem 4.4 to force convergence to a positive loss
    Defined via E_path = sum of step distances; it is an outcome-dependent certificate rather than an independently testable quantity.

how reviews work

0 comments
Cite this review

Pith. "Pith review of VALG: An Agentic System for ML Theory Research." pith.science (2026). https://pith.science/paper/RJNJ4CZJ

@misc{pith2026260813060,
  author       = {Pith},
  title        = {Pith review of: VALG: An Agentic System for ML Theory Research},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/RJNJ4CZJ}},
  note         = {Machine review of arXiv:2608.13060}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2608.13060 by the authors.

Figure 1
Figure 1. The VALG workflow. Workflow 1 creates active perspective branches; Workflow 2 is shown for one branch. Teal, amber, and green denote producers, independent reviewers, and accepted output, respectively. Solid arrows show validated forward flow. A finalized branch does not stop the remaining branches. the desired theoretical guarantee, model and data setting, learning regime, or algorithmic family. It needs not fix ev… view at source ↗
Figure 2
Figure 2. Controlled revision in VALG. An independent review identifies the smallest repair target, the controller routes the diagnosis to the responsible stage, and the selected producer revises only the implicated part. The revised attempt must pass a fresh independent review or human checkpoint before downstream use. is possible. VALG therefore uses a hierarchy of revision loops that routes each diagnosis to the smallest s… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

80 extracted references · 49 canonical work pages

  1. [1]

    2026 , eprint =

    Order-Optimal Sequential 1-Bit Mean Estimation in General Tail Regimes , author =. 2026 , eprint =

    work page 2026

  2. [2]

    Pacific Journal of Mathematics , volume =

    On General Minimax Theorems , author =. Pacific Journal of Mathematics , volume =. 1958 , doi =

    work page 1958

  3. [3]

    Communications of the ACM , volume =

    A Theory of the Learnable , author =. Communications of the ACM , volume =. 1984 , doi =

    work page 1984

  4. [4]

    Information and Computation , volume =

    Learning Regular Sets from Queries and Counterexamples , author =. Information and Computation , volume =. 1987 , doi =

    work page 1987

  5. [5]

    Information and Control , volume =

    Language Identification in the Limit , author =. Information and Control , volume =. 1967 , doi =

    work page 1967

  6. [6]

    Statistical Learning Theory , author =

  7. [7]

    2014 , doi =

    Understanding Machine Learning: From Theory to Algorithms , author =. 2014 , doi =

    work page 2014

  8. [8]

    2019 , doi =

    High-Dimensional Statistics: A Non-Asymptotic Viewpoint , author =. 2019 , doi =

    work page 2019

Show all 80 references
  1. [9]

    2023 , url =

    Yao, Shunyu and Zhao, Jeffrey and Yu, Dian and Du, Nan and Shafran, Izhak and Narasimhan, Karthik and Cao, Yuan , booktitle =. 2023 , url =

    2023

  2. [10]

    Advances in Neural Information Processing Systems , volume =

    Reflexion: Language Agents with Verbal Reinforcement Learning , author =. Advances in Neural Information Processing Systems , volume =. 2023 , url =

    2023

  3. [11]

    Advances in Neural Information Processing Systems , volume =

    Self-Refine: Iterative Refinement with Self-Feedback , author =. Advances in Neural Information Processing Systems , volume =. 2023 , url =

    2023

  4. [12]

    Lu, Chris and Lu, Cong and Lange, Robert Tjarko and Foerster, Jakob and Clune, Jeff and Ha, David , year =. The. 2408.06292 , archiveprefix =

    arXiv

  5. [13]

    Agent Laboratory: Using

    Schmidgall, Samuel and Su, Yusheng and Wang, Ze and Sun, Ximeng and Wu, Jialian and Yu, Xiaodong and Liu, Jiang and Moor, Michael and Liu, Zicheng and Barsoum, Emad , year =. Agent Laboratory: Using. 2501.04227 , archiveprefix =

    arXiv

  6. [14]

    Accelerating Scientific Discovery with

    Gottweis, Juraj and Weng, Wei-Hung and Daryin, Alexander and others , journal =. Accelerating Scientific Discovery with. 2026 , doi =

    2026

  7. [15]

    2310.03302 , archiveprefix =

    Huang, Qian and Vora, Jian and Liang, Percy and Leskovec, Jure , year =. 2310.03302 , archiveprefix =

    arXiv

  8. [16]

    2410.07095 , archiveprefix =

    Chan, Jun Shern and Chowdhury, Neil and Jaffe, Oliver and Aung, James and Sherburn, Dane and Mays, Evan and Starace, Giulio and Liu, Kevin and Maksin, Leon and Patwardhan, Tejal and Weng, Lilian and Madry, Aleksander , year =. 2410.07095 , archiveprefix =

    arXiv

  9. [17]

    2411.15114 , archiveprefix =

    Wijk, Hjalmar and Lin, Tao and Becker, Joel and Jawhar, Sami and Parikh, Neev and Broadley, Thomas and Chan, Lawrence and Chen, Michael and Clymer, Josh and Dhyani, Jai and Ericheva, Elena and Garcia, Katharyn and Goodrich, Brian and Jurkovic, Nikola and Karnofsky, Holden and ...

    arXiv

  10. [18]

    and Kapoor, Sayash and Nadgir, Nitya and Stroebl, Benedikt and Narayanan, Arvind , year =

    Siegel, Zachary S. and Kapoor, Sayash and Nadgir, Nitya and Stroebl, Benedikt and Narayanan, Arvind , year =. 2409.11363 , archiveprefix =

    arXiv

  11. [19]

    2504.01848 , archiveprefix =

    Starace, Giulio and Jaffe, Oliver and Sherburn, Dane and Aung, James and Chan, Jun Shern and others , year =. 2504.01848 , archiveprefix =

    arXiv

  12. [20]

    and Burns, Benjamin and Adu-Ampratwum, Daniel and Huang, Xuhui and Ning, Xia and Gao, Song and Su, Yu and Sun, Huan , booktitle =

    Chen, Ziru and Chen, Shijie and Ning, Yuting and Zhang, Qianheng and Wang, Boshi and Yu, Botao and Li, Yifei and Liao, Zeyi and Wei, Chen and Lu, Zitong and Dey, Vishal and Xue, Mingyi and Baker, Frazier N. and Burns, Benjamin and Adu-Ampratwum, Daniel and Huang, Xuhui and Nin...

    2025

  13. [21]

    and Gu, Alex and Chalamala, Rahul and Song, Peiyang and Yu, Shixing and Godil, Saad and Prenger, Ryan and Anandkumar, Anima , booktitle =

    Yang, Kaiyu and Swope, Aidan M. and Gu, Alex and Chalamala, Rahul and Song, Peiyang and Yu, Shixing and Godil, Saad and Prenger, Ryan and Anandkumar, Anima , booktitle =. 2023 , eprint =

    2023

  14. [22]

    2607.09217 , archiveprefix =

    Kripner, Matej and Straka, Milan , year =. 2607.09217 , archiveprefix =

    arXiv

  15. [23]

    2605.17283 , archiveprefix =

    Ma, David and others , year =. 2605.17283 , archiveprefix =

    arXiv

  16. [24]

    2601.14027 , archiveprefix =

    Liu, Junqi and others , year =. 2601.14027 , archiveprefix =

  17. [25]

    2026 , eprint =

    Towards Autonomous Mathematics Research , author =. 2026 , eprint =

    2026

  18. [26]

    2026 , eprint =

    Automated Conjecture Resolution with Formal Verification , author =. 2026 , eprint =

    2026

  19. [27]

    2604.24021 , archiveprefix =

    An, Chenyang and Ye, Qihao and Pan, Minghao and Zhang, Jiayaun , year =. 2604.24021 , archiveprefix =

    arXiv

  20. [28]

    2026 , url =

    Schmitt, Johannes and Gehrunger, Tim and Dekoninck, Jasper and B. 2026 , url =

    2026

  21. [29]

    2605.06651 , archiveprefix =

    Zheng, Daniel and others , year =. 2605.06651 , archiveprefix =

    arXiv

  22. [30]

    2026 , eprint =

    Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory , author =. 2026 , eprint =

    2026

  23. [31]

    2026 , eprint =

    Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics , author =. 2026 , eprint =

    2026

  24. [32]

    Advances in Neural Information Processing Systems , volume =

    Beyond Lazy Training for Over-Parameterized Tensor Decomposition , author =. Advances in Neural Information Processing Systems , volume =. 2020 , eprint =

    2020

  25. [33]

    Proceedings of the 42nd International Conference on Machine Learning , pages =

    The Power of Random Features and the Limits of Distribution-Free Gradient Descent , author =. Proceedings of the 42nd International Conference on Machine Learning , pages =. 2025 , volume =

    2025

  26. [34]

    Orthogonalized

    Sharan, Vatsal and Valiant, Gregory , booktitle =. Orthogonalized. 2017 , volume =

    2017

  27. [35]

    Proceedings of Thirty Third Conference on Learning Theory , year =

    Approximate Is Good Enough: Probabilistic Variants of Dimensional and Margin Complexity , author =. Proceedings of Thirty Third Conference on Learning Theory , year =. 2003.04180 , url =

    2003 arXiv

  28. [36]

    2026 , eprint =

    Robust Mean Estimation under Quantization , author =. 2026 , eprint =

    2026

  29. [37]

    Invited Open Problem: Online Optimization of Piecewise-

    Balcan, Maria-Florina and Pegden, Wesley and Sharma, Dravyansh , booktitle =. Invited Open Problem: Online Optimization of Piecewise-. 2026 , volume =

    2026

  30. [38]

    Invited Open Problem: Does Differential Privacy Make

    Nissim, Kobbi and Stemmer, Uri and Tsfadia, Eliad , booktitle =. Invited Open Problem: Does Differential Privacy Make. 2026 , volume =

    2026

  31. [39]

    Open Problem: How Much Overparametrization Is Needed for

    Arvanitakis, Dionysis and Srinivas, Vaidehi and Vijayaraghavan, Aravindan , booktitle =. Open Problem: How Much Overparametrization Is Needed for. 2026 , volume =

    2026

  32. [40]

    Proceedings of the Thirty-Ninth Conference on Learning Theory , pages =

    Invited Open Problem: Is the Power of Deep Learning over Linear Models Inherently Distribution Dependent? , author =. Proceedings of the Thirty-Ninth Conference on Learning Theory , pages =. 2026 , volume =

    2026

  33. [41]

    Proceedings of the Thirty-Ninth Conference on Learning Theory , pages =

    Open Problem: Is Interaction Necessary for Order-Optimal 1-Bit Mean Estimation? , author =. Proceedings of the Thirty-Ninth Conference on Learning Theory , pages =. 2026 , volume =

    2026

  34. [42]

    Journal of Machine Learning Research , volume=

    Limitations of learning via embeddings in Euclidean half spaces , author=. Journal of Machine Learning Research , volume=

  35. [43]

    Journal of Privacy and Confidentiality , volume=

    Calibrating noise to sensitivity in private data analysis , author=. Journal of Privacy and Confidentiality , volume=

  36. [44]

    Machine learning , volume=

    Learning quickly when irrelevant attributes abound: A new linear-threshold algorithm , author=. Machine learning , volume=. 1988 , publisher=

    1988

  37. [45]

    Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing , pages=

    Private PAC learning implies finite Littlestone dimension , author=. Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing , pages=

  38. [46]

    2025 , eprint =

    Chao Yan , title =. 2025 , eprint =

    2025

  39. [47]

    2025 , eprint =

    Maria-Florina Balcan and Anh Tuan Nguyen and Dravyansh Sharma , title =. 2025 , eprint =

    2025

  40. [48]

    SIAM Journal on Matrix Analysis and Applications , volume =

    Uschmajew, Andrzej , title =. SIAM Journal on Matrix Analysis and Applications , volume =. 2012 , doi =

    2012

  41. [49]

    Advancing Mathematics by Guiding Human Intuition with

    Davies, Alex and Veli. Advancing Mathematics by Guiding Human Intuition with. Nature , volume =. 2021 , doi =

    2021

  42. [50]

    Nature , volume =

    Solving Olympiad Geometry without Human Demonstrations , author =. Nature , volume =. 2024 , doi =

    2024

  43. [51]

    Nature , volume =

    Mathematical Discoveries from Program Search with Large Language Models , author =. Nature , volume =. 2024 , doi =

    2024

  44. [52]

    Novikov, Alexander and V\ u, Ng\^an and Eisenberger, Marvin and Dupont, Emilien and Huang, Po-Sen and Wagner, Adam Zsolt and Shirobokov, Sergey and Kozlovskii, Borislav and Ruiz, Francisco J. R. and Mehrabian, Abbas and others , year =. 2506.13131 , archiveprefix =

    arXiv

  45. [53]

    2026 , eprint =

    Moonshine: An Autonomous Mathematical Research Agent Centered on Conjecture Generation , author =. 2026 , eprint =

    2026

  46. [54]

    2026 , eprint =

    Iteris: Agentic Research Loops for Computational Mathematics , author =. 2026 , eprint =

    2026

  47. [55]

    2026 , eprint =

    Agentic Neurosymbolic Collaboration for Mathematical Discovery: A Case Study in Combinatorial Design , author =. 2026 , eprint =

    2026

  48. [56]

    2605.22875 , archiveprefix =

    Zhao, Zelin and Yuan, Bo and Choi, Jaemoo and Chen, Yongxin , year =. 2605.22875 , archiveprefix =

    arXiv

  49. [57]

    2607.04394 , archiveprefix =

    Cao, Yichuan and Qiu, Ruichen and Liu, Junqi and Wang, Jiaqi and Guo, Dakai and Feng, Ruyong and Zhi, Lihong and Gao, Xiao-Shan , year =. 2607.04394 , archiveprefix =

    arXiv

  50. [58]

    2607.14178 , archiveprefix =

    He, Yutong and Li, Daibo and Li, Guohong and Geng, Jiahe and Huang, Zhengyang and Ren, Can and Zhang, Zekun and Liu, Yifan and Zhu, Shuchen and Zhang, Hengrui and others , year =. 2607.14178 , archiveprefix =

    arXiv

  51. [59]

    2205.11491 , archiveprefix =

    Lample, Guillaume and Lachaux, Marie-Anne and Lavril, Thibaut and Martinet, Xavier and Hayat, Amaury and Ebner, Gabriel and Rodriguez, Aur\'elien and Lacroix, Timoth\'ee , year =. 2205.11491 , archiveprefix =

    arXiv

  52. [60]

    Proceedings of the 7th Conference on Artificial Intelligence and Theorem Proving , year =

    An In-Context Learning Agent for Formal Theorem-Proving , author =. Proceedings of the 7th Conference on Artificial Intelligence and Theorem Proving , year =. 2310.04353 , url =

    arXiv

  53. [61]

    2405.14333 , archiveprefix =

    Xin, Huajian and Guo, Daya and Shao, Zhihong and Ren, Zhizhou and Zhu, Qihao and Liu, Bo and Ruan, Chong and Li, Wenda and Liang, Xiaodan , year =. 2405.14333 , archiveprefix =

    arXiv

  54. [62]

    Ren, Z. Z. and Shao, Zhihong and Song, Junxiao and Xin, Huajian and Wang, Haocheng and Zhao, Wanjia and Zhang, Liyue and Fu, Zhe and Zhu, Qihao and Yang, Dejian and others , year =. 2504.21801 , archiveprefix =

    arXiv

  55. [63]

    2407.10040 , archiveprefix =

    Lin, Haohan and Sun, Zhiqing and Welleck, Sean and Yang, Yiming , year =. 2407.10040 , archiveprefix =

    arXiv

  56. [64]

    2310.00656 , archiveprefix =

    Wang, Haiming and Xin, Huajian and Zheng, Chuanyang and Li, Lin and Liu, Zhengying and Cao, Qingxing and Huang, Yinya and Xiong, Jing and Shi, Han and Xie, Enze and others , year =. 2310.00656 , archiveprefix =

    arXiv

  57. [65]

    2604.26311 , archiveprefix =

    Zhang, Youyuan and Sun, Jialiang and Bi, Hangrui and Geng, Chuqin and Ma, Wenjie and Li, Zhaoyu and Si, Xujie , year =. 2604.26311 , archiveprefix =

    arXiv

  58. [66]

    Discover and Prove: An Open-Source Agentic Framework for Hard Mode Automated Theorem Proving in

    Liu, Chengwu and Yin, Yichun and Yuan, Ye and Xie, Jiaxuan and Li, Botao and Li, Siqi and Shen, Jianhao and Xu, Yan and Shang, Lifeng and Zhang, Ming , year =. Discover and Prove: An Open-Source Agentic Framework for Hard Mode Automated Theorem Proving in. 2604.15839 , archiveprefix =

    arXiv

  59. [67]

    2022 , eprint =

    Autoformalization with Large Language Models , author =. 2022 , eprint =

    2022

  60. [68]

    and Radev, Dragomir and Avigad, Jeremy , year =

    Azerbayev, Zhangir and Piotrowski, Bartosz and Schoelkopf, Hailey and Ayers, Edward W. and Radev, Dragomir and Avigad, Jeremy , year =. 2302.12433 , archiveprefix =

    arXiv

  61. [69]

    2023 , eprint =

    Multilingual Mathematical Autoformalization , author =. 2023 , eprint =

    2023

  62. [70]

    2025 , eprint =

    Autoformalization in the Era of Large Language Models: A Survey , author =. 2025 , eprint =

    2025

  63. [71]

    2510.15981 , archiveprefix =

    Cabral, Rafael and Do, Tuan Manh and Yu, Xuejun and Tai, Wai Ming and Feng, Zijin and Shen, Xin , year =. 2510.15981 , archiveprefix =

  64. [72]

    2026 , eprint =

    Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization , author =. 2026 , eprint =

    2026

  65. [73]

    2607.04655 , archiveprefix =

    Wang, Haocheng and Huang, Baiyu and Wan, Yingjia and Zhu, Xiao and Liu, Xiaoyang and Huang, Yinya and Guo, Zhijiang , year =. 2607.04655 , archiveprefix =

    arXiv

  66. [74]

    2026 , eprint =

    Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases , author =. 2026 , eprint =

    2026

  67. [75]

    2109.00110 , archiveprefix =

    Zheng, Kunhao and Han, Jesse Michael and Polu, Stanislas , year =. 2109.00110 , archiveprefix =

    arXiv

  68. [76]

    2024 , eprint =

    Tsoukalas, George and Lee, Jasper and Jennings, John and Xin, Jimmy and Ding, Michelle and Jennings, Michael and Thakur, Amitayush and Chaudhuri, Swarat , booktitle =. 2024 , eprint =

    2024

  69. [77]

    2605.28003 , archiveprefix =

    Son, Guijin and Yi, Seungyeop and Gwak, Minju and Ko, Hyunwoo and Jang, Wongi and Yu, Youngjae , year =. 2605.28003 , archiveprefix =

    arXiv

  70. [78]

    and Liu, Fanghui , year =

    Zhang, Yuanhe and Lee, Jason D. and Liu, Fanghui , year =. 2602.02285 , archiveprefix =

    arXiv

  71. [79]

    and Liu, Fanghui , year =

    Zhang, Yuanhe and Sun, Yuekai and Suzuki, Taiji and Lee, Jason D. and Liu, Fanghui , year =. 2606.05400 , archiveprefix =

    arXiv

  72. [80]

    Proceedings of the 58th Annual ACM Symposium on Theory of Computing , pages=

    Private Learning of Littlestone Classes, Revisited , author=. Proceedings of the 58th Annual ACM Symposium on Theory of Computing , pages=

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.