https://www.linkedin.com/posts/ilyasergey_new-post-on-proofs-and-intuitions-on-the-share-7462518426058625026-9aOv?utm_source=share&utm_medium=member_android&rcm=ACoAACSY17kB8nKeUAs4qK-Xpt5-VQ8o_lo8Y4I
New post on Proofs and Intuitions: "On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications." Formal verification is only as good as the spec you verify a program against, so how do you know the spec itself is right? In this post, we look at whether property-based testing (yes, the 25-year-old QuickCheck idea) can validate LLM-synthesised specifications in Lean. Short answer: yes, surprisingly well. In particular, our approach flagged underspecification in around 10% of the published, human-written specs in widely cited benchmarks for verified program synthesis. https://lnkd.in/gfECw6-c
On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications