Lean benchmark for real-world SWE tasks.
We scrape github for PBTs in hypothesis and use an LLM to transpile them to Lean specs, autoformalizing each function under test along the way.
The website
The benchmark generation pipeline and postproduction tools. Includes unified formalization agent (produces both Impl.lean and Spec.lean), quality assessment, and post-processing (turncount, merge, metrics, grading). Requires ANTHROPIC_API_KEY in .env. Source PBTs are pulled automatically from the GaloisInc/fvspec-pbt dataset on the Hugging Face Hub; to run against a local file instead, drop a JSONL under ./benchmark/data and pass its name via --datafile.
Conducting performance baselines on the benchmark
All you need are uv and elan to work with the pipelines or evals, but npm is required for the website. Tip: run lake build in ./benchmark/lake-template once to prepopulate the .lake dir for performance.
This project is funded by the Advanced Research + Invention Agency (ARIA).
This work is made available under both an MIT license and an Apache 2 license such that users can decide which to utilize.