3 citations · 10 across the 18 of their papers we have counts for
7 papers · 1 filter
ProofCouncil: An LLM Agent for Solving Open Mathematical Problems
Johannes Schmitt, Tim Gehrunger, Jasper Dekoninck +4
Large language models (LLMs) have shown increasing promise in solving open problems in mathematics. However, their performance can be further improved through agentic workflows tai…
Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness
Ivo Petrov, Jasper Dekoninck, Dimitar I. Dimitrov +1
Large language models (LLMs) have become capable mathematical problem-solvers, often producing correct proofs for challenging problems. However, correctness alone is not sufficient…
Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean
Kári Rögnvaldsson, Chenhao Sun, Jasper Dekoninck +1
Large language models (LLMs) are increasingly used in workflows for generating formal proofs in Lean. These workflows often decompose problems into smaller lemmas, sample many proo…
Learning from Saturated Data: Signals Beyond Correctness for LLM Training
Hanno Hiss, Jasper Dekoninck, Martin Vechev
The growing capabilities of large language models (LLMs) have led to the saturation of many benchmarks and training datasets used to improve them. Motivated by this, we investigate…
Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs
Jasper Dekoninck, Nikola Jovanović, Tim Gehrunger +4
Large language models (LLMs) are becoming increasingly capable mathematical collaborators, but static benchmarks are no longer sufficient for evaluating progress: they are often na…
Delay, Plateau, or Collapse: Evaluating the Impact of Systematic Verification Error on RLVR
Kazuki Egashira, Mark Vero, Jasper Dekoninck +3
Reinforcement Learning with Verifiable Rewards (RLVR) has become a powerful approach for improving the reasoning capabilities of large language models (LLMs). While RLVR is designe…
QED-Nano: Teaching a Tiny Model to Prove Hard Theorems
LM-Provers, Yuxiao Qu, Amrith Setlur +6
Proprietary AI systems have recently demonstrated impressive capabilities on complex proof-based problems, with gold-level performance reported at the 2025 International Mathematic…