Proof Games
Motivation
In today’s modern world, bugs in software systems incur significant costs. One promising approach to improve software quality is to prove that the software is correct. There has been tremendous progress in the past 20 years on techniques for performing proofs about programs, specifically through a research area called program verification. However, despite these advances, even state-of-the-art automated techniques have limitations, and there are cases where fully automated verification fails, thereby requiring some form of human intervention for the verification to complete. As a result, proofs of correctness about programs often still require some amount of manual effort, whether it’s in the form of annotations, pre-post conditions, loop invariants, or other guidance.
The broad goal of this project is to crowdsource proofs about programs using gamification, the way Foldit crowdsourced protein folding. In other words, we want to turn each proof about a program into a level inside a game, and let people play the game.
Chapter I: A game for Natural Deduction Proofs
Let’s be honest: our long-term goal is a daunting and ambitious one. And so to get things going we started by looking at a narrower research question: can we turn proofs into a game? Not necessarily proofs about programs, but just any kind of proof. This exploration lead to our first result in this area: Polymorphic Blocks. You can find out more about Polymorphic Blocks by clicking on the link (which also includes our CHI 2015 paper on the topic), but the summary for our purpose here: we developed a visual puzzle game in which solving a puzzle is equivalent to finding a proof in natural deduction. Players solved visual puzzles without ever being exposed to the mathematical symbols.
Although players of our game were able to build simple natural deduction proofs, the real question for us was: how can we move towards our ultimate goal, which is to reason about programs using gamification? If we want to move beyond simple proofs, one of the main challenges is that formulas get larger, and it’s not clear that our Polymorphic Blocks visual representation of formulas scales. Also, in Polymorphic Blocks, users have to do every single step of the proof, which gets really tedious. But there are automated tools that can do many of the tedious steps, so we might want to use those tools to help players. So we decided to try a new approach.
Chapter II: A Game for Loop Invariants
Our new approach is rooted in two decisions that put us at a different point in the design space than our previous game. First, we decided to expose the symbols to the user. It turns out, people have a lot of intuition of about numbers, addition, subtraction, and exposing these symbols will allow us to leverage this. Second, instead of focusing on mundane proof details, we decided to focus specifically on coming up with loop invariants, which is one of the hardest parts of program verification.
In particular, we developed a new puzzle game called InvGame where players find loop invariants without being aware of it. Our game displays rows of numbers, and players must find patterns in these numbers. Without players knowing it, the rows in the game correspond to values of variables at each iteration of a loop in a program. Therefore, unbeknown to the player, finding patterns in these numbers corresponds to finding candidate loop invariants. As a result, by simply playing the game, players provide us with candidate loop invariants, without being aware of it, and without program verification expertise. InvGame then checks these candidates with a solver to determine which are indeed loop invariants. We have shown show through an experiment with Mechanical Turk users that players enjoy the game, and are able to solve verification tasks that automated state-of-the-art tools cannot. More details can be found in our CHI 2018 paper below.
Videos
1) hour-long talk about the entire project
2) 30-second clip about our CHI 2015 paper
3) 30-second clip about our CHI 2018 paper
Papers
Polymorphic Blocks: Formalism-Inspired UI for Structured Connectors (CHI 2015)
with Stephen R. Foster and William G. Griswold
Inferring Loop Invariants through Gamification (CHI 2018)
with Dimitar Bounov, Anthony DeRossi, Massimiliano Menarini, William G. Griswold
Artifacts (Code, Games)
For Polymorphic Blocks, the game and code can be found on the Polymorphic Blocks page.
For the invariant game, the code can be found here, and a live version of the game is here.