Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
mstdn.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
A general-purpose Mastodon server with a 500 character limit. All languages are welcome.

Administered by:

Server stats:

16K
active users

mstdn.social: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.4

#Leanprover

18 posts7 participants0 posts today
Public
José A. Alonso

STP: Self-play LLM theorem provers with iterative conjecturing and proving. ~ Kefan Dong, Tengyu Ma. arxiv.org/abs/2502.00212 #AI #LLMs #ITP #LeanProver

arXiv logo
arXiv.orgSTP: Self-play LLM Theorem Provers with Iterative Conjecturing and ProvingA fundamental challenge in formal theorem proving by LLMs is the lack of high-quality training data. Although reinforcement learning or expert iteration partially mitigates this issue by alternating between LLM generating proofs and finetuning them on correctly generated ones, performance quickly plateaus due to the scarcity of correct proofs (sparse rewards). To keep improving the models with limited data, we draw inspiration from mathematicians, who continuously develop new results, partly by proposing novel conjectures or exercises (which are often variants of known results) and attempting to solve them. We design the Self-play Theorem Prover (STP) that simultaneously takes on two roles, conjecturer and prover, each providing training signals to the other. The conjecturer is trained iteratively on previously generated conjectures that are barely provable by the current prover, which incentivizes it to generate increasingly challenging conjectures over time. The prover attempts to prove the conjectures with standard expert iteration. We evaluate STP with both Lean and Isabelle formal versifiers. With 51.3 billion tokens generated during the training in Lean, STP proves 28.5% of the statements in the LeanWorkbook dataset, doubling the previous best result of 13.2% achieved through expert iteration. The final model achieves state-of-the-art performance among whole-proof generation methods on miniF2F-test (65.0%, pass@3200), Proofnet-test (23.9%, pass@3200) and PutnamBench (8/644, pass@3200). We release our code, model, and dataset in this URL: https://github.com/kfdong/STP.
Public
José A. Alonso

Lean formalization of generalization error bound by Rademacher complexity. ~ Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, Naoto Onda. arxiv.org/abs/2503.19605 #ITP #LeanProver

arXiv logo
arXiv.orgLean Formalization of Generalization Error Bound by Rademacher ComplexityWe formalize the generalization error bound using Rademacher complexity in the Lean 4 theorem prover. Generalization error quantifies the gap between a learning machine's performance on given training data versus unseen test data, and Rademacher complexity serves as an estimate of this error based on the complexity of learning machines, or hypothesis class. Unlike traditional methods such as PAC learning and VC dimension, Rademacher complexity is applicable across diverse machine learning scenarios including deep learning and kernel methods. We formalize key concepts and theorems, including the empirical and population Rademacher complexities, and establish generalization error bounds through formal proofs of McDiarmid's inequality, Hoeffding's lemma, and symmetrization arguments.
Public
Lean

Leo's talk, Verified Collaboration, presented as part of the Simon's Foundation Presidential Lecture series on mathematics and computer science has recently been posted.

Watch it here: youtube.com/watch?v=rmMYFmlUbJ8

There are some great examples of cross-disciplinary collaborative efforts highlighted, including the Liquid Tensor Experiment and SampCert, which Leo notes would have been impossible with the strength of Mathlib and the #LeanProver community behind it.

YouTubeLeonardo de Moura - Verified Collaboration: How Lean is Transforming Math...(March 12, 2025)By Simons Foundation
ExploreLive feeds
About