425 citations · 445 across the 12 of their papers we have counts for
5 papers · 1 filter
DecompRL: Solving Harder Problems by Learning Modular Code Generation
Juliette Decugis, Fabian Gloeckle, Francis Bach +2
How can Large Language Models (LLMs) solve problems they currently cannot? Repeated sampling scales test-time compute but GPU cost grows linearly with attempts, while reinforcement…
Formalizing Mathematics at Scale
Ahmad Rammal, Niket Patel, Fabian Gloeckle +5
We present AutoformBot, a multi-agent system for building an Autoformalized Textbook Library At Scale (Atlas) in Lean 4. AutoformBot orchestrates thousands of LLM agents, equipped…
WybeCoder: Verified Imperative Code Generation
Fabian Gloeckle, Mantas Baksys, Darius Feher +5
Recent progress in large language models (LLMs) has substantially advanced automatic code generation and formal theorem proving, yet software verification has not seen comparable g…
Automatic Textbook Formalization
Fabian Gloeckle, Ahmad Rammal, Charles Arnal +4
We present a case study where an automatic AI system formalizes a textbook with more than 500 pages of graduate-level algebraic combinatorics to Lean. The resulting formalization r…
LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics
Antoine Peyronnet, Fabian Gloeckle, Amaury Hayat
We present a new approach for benchmarking Large Language Model (LLM) capabilities on research-level mathematics. Existing benchmarks largely rely on static, hand-curated sets of c…