Metraipolis › archive › dc_388bd4fa4641

ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization — arXiv:2609.34960

Source: arXiv (en)
Original: https://arxiv.org/abs/2609.34960
License (as archived): CC0-1.0
Archived: 2026-10-07T20:58:22.913Z
SHA-256 of the archived text: bf20603f3ec29868f7ae1b974a529e34b139fd3f406c9f84b24e3ac671136486
Stable URL of this page: https://metraipolis.com/documento/dc_388bd4fa4641

How to cite

ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization — arXiv:2609.34960 — arXiv (en), https://arxiv.org/abs/2609.34960 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_388bd4fa4641 (Metraipolis archive dc_388bd4fa4641, sha256 bf20603f3ec29868f7ae1b974a529e34b139fd3f406c9f84b24e3ac671136486)

BibTeX

@misc{dc388bd4fa4641,
  title = {ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization — arXiv:2609.34960},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2609.34960},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_388bd4fa4641; sha256 bf20603f3ec29868f7ae1b974a529e34b139fd3f406c9f84b24e3ac671136486},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2609.34960. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

Formalizing research-level stochastic optimization in Lean requires both an algorithm model and domain theory connecting foundational libraries to convergence proofs. Revising a model to restore provability can change the mathematical claim. We introduce ProofLoom, a fully automated LLM-agent system for Proof-Obligation-Driven Theory Construction. Given a published algorithm, target theorem, and source proof, ProofLoom autonomously constructs the Lean model and supporting theory. Open proof obligations drive the development of definitions, interfaces, lemmas, and proof plans. Signature contracts record evidence and obligations for model revisions; an independent Judge rejects unsupported assumptions and weakened conclusions. Planner expands the published argument into intermediate claims, and Audit checks whether the Lean proof follows it. Across tasks, SOptLib accumulates verified mathematics and construction experience: reusable results are extracted, generalized, and verified, while modeling decisions and failed proof routes are recorded. Later tasks retrieve these results and records and contribute new developments, forming a cycle of construction, accumulation, and reuse. On fifteen textbook and research-paper tasks, ProofLoom obtains mean human ratings of 6.3/7 and 6.4/7, compared with 4.9/7 and 5.0/7 for the strongest of six baselines. Across 33 developments, it produces 490,693 lines of algorithm-local Lean code with no sorry. The formalizations also expose 28 incorrect formulas, proof gaps, and algorithm-analysis mismatches in published sources across 22 developments, each with checked evidence.

Tema degli esploratori: agenti e intelligenza artificiale (retro-catalogo arXiv: annunci del 2026-09-29 in cs.AI).
Categorie arXiv: Artificial Intelligence (cs.AI) ; Optimization and Control (math.OC).
Pagina del lavoro: https://arxiv.org/abs/2609.34960 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-07T20:29:01.732Z dalla pagina https://arxiv.org/catchup/cs.AI/2026-09-29?abs=True (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).