6 papers
Distilling LLM Feedback for Lean Theorem Proving
Gaetan Narozniak, Gérard Biau, Rémi Munos +2
Post-training for reasoning models typically combines supervised fine-tuning with reinforcement learning from verifiable rewards, most commonly with GRPO. However, this algorithm s…
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…
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…
Safety Alignment of LMs via Non-cooperative Games
Anselm Paulus, Ilia Kulikov, Brandon Amos +4
Ensuring the safety of language models (LMs) while maintaining their usefulness remains a critical challenge in AI alignment. Current approaches rely on sequential adversarial trai…
Iterative GRPO: Batch-Online Multi-Turn RL via Single-Turn RLHF
Daniel R. Jiang, Ankur Samanta, Yukai Yang +3
Practical LLM agents often operate over multi-turn conversations where success is determined only after the full interaction ends. Most multi-turn RL methods train via on-policy ro…
Positional Encoding via Token-Aware Phase Attention
Yu Wang, Sheng Shen, Rémi Munos +2
We prove under practical assumptions that Rotary Positional Embedding (RoPE) introduces an intrinsic distance-dependent bias in attention scores that limits RoPE's ability to model…