Despite the science of modern formal reasoning being more than a century old,
mechanized formal reasoning is nowhere near what expert human reasoners (formal and
informal) can achieve. Meanwhile, there is a steadily increasing need for automated theorem
proving in various fields of science and engineering. Proof discovery and verification in
science and mathematics [
We present initial results from a project on augmenting automated theorem provers with crowdsourced theorem proving through games. The project was started based on the following two seemingly unrelated observations:
Observation 1 (Observation 1) Non-trivial formal theorem proving requires insight into the structure of the problem being solved. (This insight is provided by the problem domain’s experts.)
What do we mean by insight? While it is hard to quantify this, a rough characterization follows. For instance, say we are modelling a domain (e.g. standard arithmetic over N or biological processes) with a set of axioms A and we are interested in a conjecture G. Assume A can derive G, that is G is a theorem of A. Also, assume that the smallest proof of G from A is of length L via a standard proof calculus r, that is A `rL G.
One form of insight might be through possession of a library of lemmas by experts. Definition 1 (Insight via Lemmas). An expert in the domain might possess insight in the form of a set of lemmas L (such that 8f 2 L : A ` f), that enables the expert to derive G from A [ L using a proof of length L0 with L0 L.
Of course, experts could also possess insight not just through lemmas but also
through common patterns of reasoning that can be reused across problems.
? Note: While this submission draws partly from the first author’s dissertation [
might possess insight in the form of an extended proof calculus r0 that is sound (that is forall F and y, if F `r0 f then F r0 f).
This proof calculus enables the expert to derive G from A through r0 using a proof of length L0 with L0
L, that is A `rL00 G.
Insight through lemmas is usually domain and problem dependent, and insight through extened proof calculi usually transfers between domains and problems.
Unless such insight is provided to a theorem prover in some form, such problems
can be very hard to solve fully automatically. In practice, help is provided by human
experts via lemmas [
Observation 2 (Observation 2) Lay gamesa (such as chess or sudoku) which require the player to think logically or deeply are in fact formal reasoning schemes in disguise. a A lay game is simply any game which does not require extensive formal training on the order of what is required for someone to prove formal theorems in logic.
For example, even if we rename all the pieces in chess (or any similar game), it is not wrong to assume that players with some acclimatization will revert to their skills levels in unmodified chess in a short duration compared with the time they took to learn chess from scratch.
The two observations lead us to the question of whether hard formal problems can be cast into a form, for example a natural game like chess, which would remove the need for domain knowledge by completely abstracting away from the original domain. Ideally, such a game should be able to exploit a human player’s insight into the structure of the game. This insight should then be automatically transferrable into solving the problem.
We present initial promising results from the Uncomputable Games project (first
proposed in [
While [
Proof Discovery in Mathematics and
Science Software and Hardware Verification Fig. 1: The Uncomputable Games Project Architecture. The abstract architecture for Figurcero1w.1d:soTurhceedUtnhecoormempuptraobvilnegG.GamameesrsParroejencott vAisricbhleitteoctthuereth.eTorheemabpsrtorvacint garucsheirtsecatnudre for crgoawmdesorsurdcoednothtekonroewm apbroovuitntgh.e Gpraombelersmasrethneoytavriesisbollevtiongth.e users and gamers do not know about the problems they are solving. machinery of first-order logic (FOL) to specify the games, the games themselves are
neither designed to capture FOL nor to be used in crowd-sourced theorem proving.
the propositional level and cannot capture theoremhood in FOL. Tiling problems [
choices that results in an accepting state sa. 3
Given that we want to have games for crowdsourcing theorem proving, we present some general criteria to aid in the design of games that might help us in this goal. If we are lax with our requirements, we end up with trivial games that are not useful for us. One such game could just present a logic problem “G f?” directly as a game. Another such ` game could present to the player a non-deterministic Turing machine that would accept the string hG; fi only if G ` f. At any stage of the computation, a non-deterministic Turing machine has one or more choices.3 A game could then challenge the player to select choices which result in an accepting state given some input! It is obvious that approaches such as these would not help us.
The overarching requirement that players with no knowledge of formal logic be able to prove theorems by playing games helps us derive some general criteria such games should satisfy. We need a few simple definitions to make our criteria more clear. 3.1
We need a simple vocabulary to help us talk clearly about the aspects of games we are interested in. Some straightforward definitions are given below:
Game Objects Game objects are all the objects that a player can interact with and manipulate in the game. The universe of all game objects is denoted by G. Note that each game object on its own contains enough information to assemble the game at any point in time when combined with all other game objects. The game state at any point in time is a function of the game objects.
Game State The game state at any point of time is just a set of game objects. But not all sets of game objects might correspond to a meaningful configuration of the game. A game state is any valid set of game objects.
Game A game G is a quadruple hG; g G 2G; I; F i composed of the universe of all game objects G, an operation g specifying valid operations with the game objects, the initial game states I 2G and the final states F 2G.
Game Instance The initial game states are also called game instances.
Game Size The game size jgj of a game instance g is simply the number of game objects in that game instance.
Game Play A terminating game play for a game instance g1 is sequence of game states g1; g2; : : : ; gn such that gi+1 = gi fugi g [ n(ugi ) where ugi is some game object in gi and n(ugi ) is a set of game objects such that g(ugi ; n(ugi )) holds. Game play proceeds by replacing game objects with one or more other game objects.
Captures FOL A game captures FOL or theorem-proving in a proof calculus r in FOL iff every problem G ` g is isomorphic with exactly one game instance gG`g and every proof for the problem is isomorphic with every terminating game play for the instance. gG`g is called the game instance for G ` g. 3.2
Any game designed that seeks to help us should satisfy the following criteria: 1. Independently Incentivized: The games themselves should be captivating and engaging enough that users play the games of their own accord without the incentive of good theorems being proved. This sets us apart from games such as FoldIt where players 3 A non-deterministic Turing machine m is said to accept an input string s if there is a sequence of choices that results in an accepting state sa.
deal with the problem domain directly. An incentive structure is usually superimposed on the domain. 2. No Knowledge Needed: In order to play the games, the players need not have any knowledge of first-order logic and the capturing of first-order theorem proving in the game. To play, users need to know only the rules of the game. 3. Non Linguistic: Games that are linguistic in nature generally have a smaller user base.
This is a vague criterion which will be sharpened through the course of this project.
The general idea is that a player should not have to understand, for example, how
Turing machines work in order to play the game. One way to sharpen this criterion
is to stipulate that g has physical correlates or interpretations in na¨ıve physics (e.g.
dropping objects, spatially locking objects etc.).
4. Readable Proof: If a game play instance shows us that a theorem f can be proved
from premises G, the game play instance should also provide us with a readable proof
r. This rules out tiling problems [
The Catabot Rescue Games were designed with the above five criteria in mind. The
games capture first-order logic with binary resolution and natural deduction. The games
are set in a world populated by entities called catabots, which resemble robotic
caterpillars or bugs that consume objects in the game for fuel and can reproduce with other
catabots. Most of the operations in the game have natural physical correlates, such as
dropping objects, dissolving objects, breaking up catabots, etc. No elements of the
underlying logic problem are directly shown in the game. A record of the game play can
be directly translated into a proof in either binary resolution or natural deduction. The
basic design metaphors used in these games could also be utilized to invent and design
other games which satisfy the criteria. We present only the propositional subset of one
of the games. The full set of games can be found in [
There are several sound and complete proof calculi for propositional logic with different
advantages and strengths. Resolution invented by Robinson [
Given two conjunctive normal form clauses p1 _ : : : _ pi _ : : : _ pn and q1 _ : : : _ q j _ : : : _ qm, such that pi r and q j :r, where r is a propositional variable, the binary resolution rule produces:
p1 _ : : : _ pi 1 _ pi+1 _ : : : _ pn _ q1 _ : : : _ q j 1 _ q j+1 _ : : : _ qm
A proof of G ` f is obtained via resolution when there is a series of binary resolution steps resulting in the empty clause denoting false using only the clausal form (disjunctive normal form) of sentences in G [ f:fg and any sentence that was generated by applications of the rule. We now present the Catabot Rescue Game designed to capture propositional resolution. 6
TheCatabot Rescue Game 0, CRG0, captures propositional resolution. The catabots in the game are isomorphic with clauses in a propositional language and the game process is isomorphic with the steps in a resolution proof. The game satisfies the criteria defined above and adheres to the formalization presented. We start with a description of the game world. The backstory for the game is given below (A similar story is presented to the user along with a figure similar to Figure 4.):
There are a bunch of catabots imprisoned in a room by a horrible blob. The room has a small door to the outside. None of the catabots are small enough to use the door. Only a body-less catabot with just the head can go through the door! Catabots can reproduce and download their minds to any child’s body (or any other catabot). Reproduction has certain rules. Help them escape by mating them in a fashion so as to produce a body-less catabot.
Each catabot has a head and a body composed of zero or more blocks. The blocks have a certain number of limbs or legs of either positive or negative polarity such as those shown in Figure 2.
Visual Representation
Alternate Representation
The catabots represent clauses and the blocks on the body represent different atoms.
Let us assume the supply of propositional variables fP1; : : : ; Pkg. Then, e.g., Pn would have n limbs with a positive polarity and :Pn would have n limbs with a negative polarity. Figure 2 shows literals P3 and :P2.
With this process it is easier to visualize the process of binary resolution operating on two clauses. Two simple examples are shown in Figure 3.
With this process it is easier to visualize the process of binary resolution operating on two clauses. Two simple examples are shown in Figure 4.2.
child side of the parents. The children have all the blocks from the parents, save for the pair of blocks which were mated in the parents.
6.1
Catabot mating rules are very simple and correspond to propositional binary resolution.
MachTihneerruylestfoor rceatparbeosterenptrodfiurcsttio-onradreegrivaentobmeloswc:onsists of a fuel setup on top of the blocks. ThMeacteadtPaabirostCsacncoenlsTuhmeueserbcranicckhososfeoarnyftuweolc.ataBbortiscfkorsmaatrieng.dTrwoopcpateadbotisnctaon minatteerconnected if and only if they have the same number of limbs with differing polarities. Such a pair is tanks of watecralloednatmoapted patihr.e blocks. Tanks may be placed on top of the bricks. A tank of
Child Catabot The child is a catabot with all the blocks the same, except for the mated blocks represents a vainrtihaebplaerenatns.d multiple instantiations of the same variable are represented by
Same Blocks Merge If two blocks on different parents are visually the same, they merge into a network of cooneninn ethcetcehdildt.anks. Simple examples are show in Figure 4.3. More complex examples are shown in the next section. Three simple catabots are shown below in Figure 4.4.
An initial industrial-strength implementation of a subset of the operations in CRG0 has The color of the bricks and their shape but not their relative sizes. For been implemented in a game for iPads and the mWeabt.t4ers,
Figure 4 shows a screenshot of the game. ease of presentation here, we sometimes use letters in the bricks to help distinguish the
This initial version has 50 levels out of which 44 were generated automatically (in colors betteadr.ditBiorni ctokfisrsctasnix cleovemlsbwinhiechwariethcoonstihdeerredbrtuitcokrisaltloevfeolsr).mThmegoerneeractoiomnpprloecxessbricks in the 4 The wTeMb version is available at http://compete.catabotrescue.com and the iPad version is availmanner of Lego blocks (Christiansen 2013). One such combination is show below in able at https://itunes.apple.com/us/app/catabot-rescue-lite/id645249674?ls=1&mt=8. Please note that the iPad version is not compatible with more recent versions of the iPad. We sugFigure 4.5. Figure 4.6 shows an ontology of the different objects in the CRG world. gest that reviewers use the web version.
Fig. 4: Catabot Rescue Game . A screenshot of Catabot Rescue Game 0 Beginner of the problems is as follows. We randomly generate a certain number of clauses each having a minimum number min and a maximum number max of literals. Given that we want n clauses, we sample n times the discrete uniform distribution [min; max] to generate the size of each clause. Then for each clause we uniformly select from the set of all possible literals. We consider only the literals:
fp1; p2; p3; p4; :p1; :p2; :p3; :p4; g
Most of the clauses generated in this fashion do not result in a contradiction. The
Prover9 automated theorem prover [
Prover9 also reports the depth of the resolution proof tree. Problems with proofs less than four levels deep were removed. This process produces quite complex problems.
Though the problems are quite complex and hard, users without any formal training in logic found the levels engaging and were able to solve them. The scoring mechanism for the overall game is in terms of dollar rewards for the user. Upon completion of a level n with k operations, the total reward for the user becomes $(n + 100 1=k). 8
We conducted two experiments with the game. In the first experiment, we released the game to the public and got game play results from mostly players untrained in logic. While we don’t have exact numbers on the fraction of the players that were trained in logic, this experiment is supposed to mirror conditions that we might face eventually if the games are to be used on a large scale. In the second experiment, we held a contest in an introductory logic class. The students participating in the class were trained in propositional logic but had no knowledge of resolution. 8.1
Over the course of a few days (less than ten days) since the release of the iPad version of the game, the game was download around 60 times. This resulted in 400 terminating game plays collected from around 15 players. The total number of players is not accurate as users generally hand over played levels to other players and sometimes reset levels to try again and get a better score. We are not interested in metrics which dictate that we have an accurate count of the number of users. Ultimately, when we want to solve very a hard theorem through games, we only need one single player/team to solve the corresponding game instance. Among all the players, only four players were able to solve all the levels. Among these four, we were able to verify that at least two did not have any training in formal logic. Of these two players, one was able to produce smaller proofs than Prover9 for all the 44 levels, save for one. The other players who completed all the levels also produced proofs smaller than Prover9 for some of the levels. 8.2
Over the course of a week we had 1766 terminating game plays from around 80 users. Of all these users, 22 completed all the levels.
which it is easy to see how humans performed better than the ATP. The level we illustrate is Level 7 in the game. The logic problem represented is given below: ( :P1 _ :P3; P4 _ P3; P2 _ :P4; :P3 _ :P2; )
P2 _ P4; P3 _ :P4; P3 _ :P1 _ :P2; :P3 _ P1
Figures 6, 7, 8, and 9 show one possible proof of only four steps. Prover9 was unable to find any proofs with less than six binary resolution steps. Though Prover9’s configuration for the maximum number of proofs to search for was set at 50, Prover9 generated only two proofs. The two proofs are shown in Figure 10.
Child
We also ran the SNARK [
Child
Parent 1 Parent 2
(a) Proof 1 (b) Proof 2 ============================== end of pro=o=f====================================================== end of proof ===================== Fig=.=1=0==:=P=r=o=v=e=r=9=’=s=t=w==o=p==r=o=o=f=s=f=o=r==LePvReOlO7F: =P=r=o=v=e=r=9=’s==tw==o==p=r=o=o=f=s=f=o=r=L==e=v=e=l=7==a=re= longer
than the shortest proof found by humans. % -------- Comments from original proof -------% Proof 2 at 0.00 (+ 0.00) seconds. % Length of proof is 10. % Level of proof is 4. % Maximum clause weight is 2.000. % Given clauses 9. 3 P4 | P3. [assumption]. 4 P2 | -P4. [assumption]. 5 -P3 | -P2. [assumption]. 6 P2 | P4. [assumption]. 7 P3 | -P4. [assumption].
10 -P2 | P4. [resolve(5,a,3,b)].
While nowhere close to a full validation of our goal, these initial results provide us
with some promise that such games could enable crowds of untrained humans to help
machines when it comes to solving hard problems. It is quite notable that humans
without much formal training in logic can produce proofs shorter than those produced by
machine in a calculus specialized for machine reasoning. This is remarkable, because,
in addition to propositional theorem proving being hard, many associated problems in
propositional logic are hard. For example, determining whether there is a proof of a
certain length for a tautology, determining the length of the shortest proof for a given
tautology, and finding the shortest proof given the length of the shortest proof are all
believed to be quite hard [
1. The data from Experiment 2 can be download from here: https://s3.amazonaws.
com/www.catabotrescue.com/data/AnonoynmizedLevelCompletion.json. 2. The cross platform source code for the game is available here: https://github.com/ naveensundarg/catabotrescue-unity 3. The game can be played here: http://compete.catabotrescue.com