Stefan Zetzsche — accepted AI-conference papers

2026

MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification

Mantas Baksys, Sean B Holden, Olivier Bouissou, Stefan Zetzsche

ICML 2026poster

LLMs excel at reasoning, but validating their steps remains challenging. Formal verification offers a solution through mechanically checkable proofs. Interactive theorem provers (ITPs) dominate mathematical reasoning but require detailed low-level proof steps, while auto-active verifiers offer autom…

Cited by 0 Source ↗Scholar ↗

2025

CLEVER: A Curated Benchmark for Formally Verified Code Generation

Amitayush Thakur, Jasper Lee, George Tsoukalas, Meghana Sistla, Matthew Zhao, Stefan Zetzsche +3

NeurIPS 2025poster

We introduce ${\rm C{\small LEVER}}$, a high-quality, manually curated benchmark of 161 problems for end-to-end verified code generation in Lean. Each problem consists of (1) the task of generating a specification that matches a held-out ground-truth specification, and (2) the task of generating a L…

Cited by 0 Source ↗code ↗Scholar ↗