8 papers
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…
Efficient RL Training for LLMs with Experience Replay
Charles Arnal, Vivien Cabannes, Taco Cohen +2
While Experience Replay - the practice of storing rollouts and reusing them multiple times during training - is a foundational technique in general RL, it remains largely unexplore…
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…
Asymmetric REINFORCE for off-Policy Reinforcement Learning: Balancing positive and negative rewards
Charles Arnal, Gaëtan Narozniak, Vivien Cabannes +3
Reinforcement learning (RL) is increasingly used to align large language models (LLMs). Off-policy methods offer greater implementation simplicity and data efficiency than on-polic…
Provable Benefits of In-Tool Learning for Large Language Models
Sam Houliston, Ambroise Odonnat, Charles Arnal +1
Tool-augmented language models, equipped with retrieval, memory, or external APIs, are reshaping AI, yet their theoretical advantages remain underexplored. In this paper, we addres…
Prompt Selection Matters: Enhancing Text Annotations for Social Sciences with Large Language Models
Louis Abraham, Charles Arnal, Antoine Marie
Large Language Models have recently been applied to text annotation tasks from social sciences, equalling or surpassing the performance of human workers at a fraction of the cost.…