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
saved by
related reading
- A shallow dive into formal verificationvitalik.eth.limo
- A Lean Syntax Primer — overreactedoverreacted.io
- Human Judgment as a Specificationblog.brownplt.org
- Lean Software Scaling Laws · Gwern.netgwern.net
- Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agentsalphaxiv.org
- Formally Verifying the Easy Partbrainflow.substack.com
- lf-lean: The frontier of verified software engineering | Theoremtheorem.dev
- Patterns for Building LLM-based Systems & Productseugeneyan.com
- When AI Writes the World's Software, Who Verifies It? — Leonardo de Mouraleodemoura.github.io
- Automatic Formal Verification for Code Generationlogicalintelligence.com
- Dear Agent: Prove it. • Rijnard van Tonderrijnard.com
- Using LLM-based Verification to Eliminate Bugs in Linux's Network Stackbasis.ai