Theorem
Most testing strategies miss rare edge cases until customers find them in production. We’ve developed a system that automatically generates targeted unit tests for rare bugs, including the one that would have caught Anthropic’s recent approximate top-K bug.
Fractional proof decomposition fuses partial evaluation and property-based testing to scale testing compute logarithmically with bug rarity, instead of linearly. Introduction Most large projects have a limited compute budget for testing, lest it slows down the CI pipeline. This means missing rare edge cases until customers find them in production. I love formal verification! And I want to bring the power of reasoning about program structure to testing. In this blog post, I will briefly introduce fractional proof decomposition, our new technique that makes testing compute scale logarithmically
saved by
related reading
- Defeating Nondeterminism in LLM Inference - Thinking Machines Labthinkingmachines.ai
- A shallow dive into formal verificationvitalik.eth.limo
- Transformer Inference Arithmetic | kipply's blogkipp.ly
- Formally Verifying the Easy Partbrainflow.substack.com
- On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications | Proofs and Intuitionsproofsandintuitions.net
- lf-lean: The frontier of verified software engineering | Theoremtheorem.dev
- Software Testing as a Multi-Armed Bandit Problemocram575.substack.com
- FLT: Anthropic has beaten me to itxenaproject.wordpress.com
- Formalizing Fermat's Last Theoremanthropic.com
- Antithesisantithesis.com
- Finding Miscompiles for Fun, Not Profit - by Justin Lebarnewsletter.semianalysis.com
- Earn $200K by fuzzing for a weekend: Part 1 | secret clubsecret.club