2 citations · 2 across the 4 of their papers we have counts for
4 papers
AxDafny: Agentic Verified Code Generation in Dafny
Benjamin Breen, Austin Letson, Borja Requena Pozo +1
We study agentic code generation in Dafny, where a model must generate both executable code and the proof artifacts for verification. We present AxDafny, a verifier-guided repair f…
SorryDB: Can AI Provers Complete Real-World Lean Theorems?
Austin Letson, Leopoldo Sarra, Auguste Poiroux +9
We present SorryDB, a dynamically-updating benchmark of open Lean tasks drawn from 78 real world formalization projects on GitHub. Unlike existing static benchmarks, often composed…
A Minimal Agent for Automated Theorem Proving
Borja Requena, Austin Letson, Krystian Nowakowski +2
We propose a minimal agentic baseline that enables systematic comparison across different AI-based theorem prover architectures. This design implements the core features shared amo…
Reinforcement learning with learned gadgets to tackle hard quantum problems on real hardware
Akash Kundu, Leopoldo Sarra
Quantum computing offers exciting opportunities for simulating complex quantum systems and optimizing large scale combinatorial problems, but its practical use is limited by device…