6 papers
SorryDB: Can AI Provers Complete Real-World Lean Theorems?
Austin Letson, Leopoldo Sarra, Auguste Poiroux +9
We present SorryDB, a dynamically-updating benchmark of open Lean tasks drawn from 78 real world formalization projects on GitHub. Unlike existing static benchmarks, often composed…
Progress in Formalizing Sphere Packing in Dimension 8
Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee +4
In 2016, Viazovska famously solved the sphere packing problem in dimension , using modular forms to construct a 'magic' function satisfying optimality conditions determined by C…
Do LLMs Game Formalization? Evaluating Faithfulness in Logical Reasoning
Kyuhee Kim, Auguste Poiroux, Antoine Bosselut
Formal verification guarantees proof validity but not formalization faithfulness. For natural-language logical reasoning, where models construct axiom systems from scratch without…
Apertus: Democratizing Open and Compliant LLMs for Global Language Environments
Project Apertus, Alejandro Hernández-Cano, Alexander Hägele +100
We present Apertus, a fully open suite of large language models (LLMs) designed to address two systemic shortcomings in today's open model ecosystem: data compliance and multilingu…
RLMEval: Evaluating Research-Level Neural Theorem Proving
Auguste Poiroux, Antoine Bosselut, Viktor KunÄak
Despite impressive results on curated benchmarks, the practical impact of large language models (LLMs) on research-level neural theorem proving and proof autoformalization is still…
Reliable Evaluation and Benchmarks for Statement Autoformalization
Auguste Poiroux, Gail Weiss, Viktor KunÄak +1
Evaluating statement autoformalization, translating natural language mathematics into formal languages like Lean 4, remains a significant challenge, with few metrics, datasets, and…