Inferring Loop Invariants through Gamification
summary
A puzzle game shows runtime traces and asks players to enter arithmetic and Boolean expressions; the backend uses counterexample pruning to filter and combine those expressions into inductive loop invariants. The system runs as a crowdsourcing experiment with 67 Mechanical Turk players, achieving human-derived invariants that let verification tools solve 10 of 14 benchmarks that state-of-the-art invariant generators could not, and players rate the game about 4.36/5 while some solutions require stitching different players’ suggestions.
AI-written summary · about
chapters (9)
- 0:00Introduction to loop invariants
- 1:52Game demo and overview
- 3:37Challenges in loop invariants
- 6:02Game design and player interaction
- 9:08Evaluation and results
- 12:00Player effectiveness analysis
- 13:26Key findings and implications
- 15:13Summary and future work
- 15:57Q&A session
related talks
40mPuzzles, Problems, and Programs
23mBeyond Tests What to Verify in AI Generated Code
30mExploring the Verifiability of Code Generated by GitHub Copilot
11mThe Benchmarks Game: Why It's Rigged and How You Can (Really) Win
43mSoftware Design: Humans vs AI
39mThe Boringly Simple Loop Powering GenAI Apps
50mIdentifying and fixing Issues in Code using AI based tools
26mInteractive Theorem Provers for Proof Education