On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications | Proofs and Intuitions
In this post, we show that property-based testing (PBT) is surprisingly effective for validating LLM-synthesised specifications of Lean programs: it is a cheap alternative to symbolic proofs, which helped to detect underspecification in 10% of the specs in state-of-the-art benchmarks for verified code generation.
In this post, we show that property-based testing (PBT) is surprisingly effective for validating LLM-synthesised specifications of Lean programs: it is a cheap alternative to symbolic proofs, which helped to detect underspecification in 10% of the specs in state-of-the-art benchmarks for verified code generation. Getting Program Specifications that are “Just Right” Formal program verification and program synthesis are only as reliable as the specifications used to validate the programs in question. A specification is a mathematical contract between a programmer and a machine: it captures what
Explore this link on the map →saved by
related reading
- A Lean Syntax Primer — overreactedoverreacted.io
- A shallow dive into formal verificationvitalik.eth.limo
- Dear Agent: Prove it. • Rijnard van Tonderrijnard.com
- The sad state of property-based testing librariesstevana.github.io
- Human Judgment as a Specificationblog.brownplt.org
- Catching bugs with fractional proofs | Theoremtheorem.dev
- When AI Writes the World's Software, Who Verifies It? — Leonardo de Mouraleodemoura.github.io
- Introduction to Property Based Testing | by Nicolas Dubien | Criteo Tech Blog | Mediummedium.com
- lf-lean: The frontier of verified software engineering | Theoremtheorem.dev
- Tao on “blue team” vs. “red team” LLMs | Hacker Newsnews.ycombinator.com
- Your AI Product Needs Evals – Hamel's Blog - Hamel Husainhamel.dev
- crawshaw - 2025-01-06crawshaw.io