Papers by Auguste Poiroux
RLMEval: Evaluating Research-Level Neural Theorem Proving (2025.findings-emnlp)
Copied to clipboard
| Challenge: | RLMEval evaluates large language models for research-level neural theorem proving and proof autoformalization . the best model achieves only a 10.3% pass rate on existing benchmarks . |
| Approach: | They propose a new evaluation suite for large language models . it evaluates research-level theorems from real-world Lean formalization projects . |
| Outcome: | RLMEval evaluates research-level theorems from real-world Lean formalization projects. |
Reliable Evaluation and Benchmarks for Statement Autoformalization (2025.emnlp-main)
Copied to clipboard
| Challenge: | Existing methods for evaluating statement autoformalization are limited . current methods can achieve up to 45.1% accuracy on undergraduate mathematics . |
| Approach: | They propose a new autoformalization metric that correlates strongly with human judgment . they propose two new auto-formalisation benchmarks: ProofNet# and RLM25 . |
| Outcome: | The proposed methods can achieve up to 45.1% accuracy on undergraduate mathematics but struggle with research-level content without proper context. |
Apertus: Democratizing Open and Compliant LLMs for Global Language Environments (2026.acl-long)
Copied to clipboard
Alejandro Hernández-Cano, Alexander Hägele, Allen Hao Huang, Angelika Romanou, Antoni-Joan Solergibert, Barna Pásztor, Bettina Messmer, Dhia Garbaya, Eduard Frank Ďurech, Ido Hakimi, Juan Garcia Giraldo, Mete Ismayilzada, Negar Foroutan, Skander Moalla, Tiancheng Chen, Vinko Sabolčec, Yixuan Xu, Michael Aerni, Badr AlKhamissi, Inés Altemir Marinas, Mohammad Hossein Amani, Matin Ansaripour, Ilia Badanin, Harold Benoit, Emanuela Boros, Nicholas John Browning, Fabian Bösch, Maximilian Böther, Niklas Canova, Camille Challier, Clément Charmillot, Jonathan Coles, Jan Milan Deriu, Arnout Devos, Lukas Drescher, Daniil Dzenhaliou, Maud Ehrmann, Dongyang Fan, Simin Fan, Silin Gao, Miguel Gila, María Grandury, Diba Hashemi, Alexander Miserlis Hoyle, Jiaming Jiang, Mark Klein, Andrei Kucharavy, Anastasiia Kucherenko, Frederike Lübeck, Roman Machacek, Theofilos Ioannis Manitaras, Andreas Marfurt, Kyle Matoba, Simon Matrenok, Henrique Mendonça, Fawzi Roberto Mohamed, Syrielle Montariol, Luca Mouchel, Sven Najem-Meyer, Jingwei Ni, Gennaro Oliva, Matteo Pagliardini, Elia Palme, Andrei Panferov, Léo Paoletti, Marco Passerini, Ivan Pavlov, Auguste Poiroux, Kaustubh Ponkshe, Nathan Ranchin, Javier Rando, Mathieu Sauser, Jakhongir Saydaliev, Mukhammadali Sayfiddinov, Marian Schneider, Stefano Schuppli, Marco Scialanga, Andrei Semenov, Kumar Shridhar, Raghav Singhal, Anna Sotnikova, Alexander Sternfeld, Ayush Kumar Tarun, Paul Teiletche, Jannis Vamvas, Xiaozhe Yao, Hao Zhao, Alexander Ilic, Ana Klimovic, Andreas Krause, Caglar Gulcehre, David Rosenthal, Elliott Ash, Florian Tramèr, Joost VandeVondele, Livio Veraldi, Martin Rajman, Thomas C. Schulthess, Torsten Hoefler, Antoine Bosselut, Martin Jaggi, Imanol Schlag
| Challenge: | Apertus is a fully open suite of large language models (LLMs) designed to address responsibility shortcomings in today’s open model ecosystem, namely data responsibility and global representation. |
| Approach: | They propose to release a fully open suite of large language models (LLMs) that address data responsibility and global representation shortcomings in today’s open model ecosystem. |
| Outcome: | The proposed model is pretrained on openly available data and suppresses verbatim recall of data while retaining task performance. |