8 papers
GitSwarm: Decentralized Compounding Inference
Vedant Shah, Ankur Samanta, Paras Dahal +11
Long-horizon problem solving and scientific research require computation to accumulate across successive attempts. Partial solutions, experimental findings, and unsuccessful approa…
Learning to Discover Interesting Mathematics
Niket Patel, Ahmad Rammal, Amaury Hayat +2
Recently, Large Language Models (LLMs) have been increasingly able to solve advanced mathematical problems, including many that have been open for decades. This opens the door to e…
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 Policy Optimization: Batch-Online Multi-Turn RL via Single-Turn RL
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…