5 papers · 1 filter
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…
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…