PROJECT TITLE: Wikipedia for Formally-Specified Computation/Science

Letter of Intent to NSF (INSPIRE) March 2013: SYNOPSIS

Karl Lieberherr, CCIS, Northeastern

The Wikipedia is a successful crowdsourcing project. We propose to develop a Wikipedia for Formally-Specified Computation and for Formal Science. The connection between the two is that Formal Sciences use formally-specified computations to refute the false claims. Every claim in our system consists of a formal specification of how to refute it, following ideas of Karl Popper.

Formally-specified computations are defined by logical statements (a.k.a. claims) interpreted in a computable structure. Semantic Games (SGs) of claims provide novel answers to crowdsourcing challenges yet with several limitations. We provide a comprehensive analysis of the limitations of SGs when used for crowdsourcing and propose a new concept, called the Contradiction-Agreement Game (CAG), which builds on SGs and has desirable properties for successful crowdsourcing. The list of desirable properties includes a progress property (each CAG improves evaluation of scholars or adds to social welfare), cheating prevention through anonymity and cheating detection and fairness of the CAG payoff function.

We have a proof of concept implementation of a CAG-based crowdsourcing platform for formally-specified computational problems, called the Scientific Community Game (SCG). SCG uses a modular construct, called a lab, to group related claims and to solve labs incrementally through lab relations, which are themselves captured as labs. SCG has the flavor of a "Wikipedia for Formally-Specified Computation/Science" where inventions are explicit and composable.

Our proposed system has significant applications, in addition to crowdsourcing formally-specified computations. (1) The collaborative and self-evaluating nature of SGs provides a peer-based evaluation system for MOOCs on formal science topics. The peer-based evaluation is guaranteed to be fair, and it saves significant time for the teaching staff. (2) SGs provide a lower barrier of entry to making contributions to formal sciences through game play. It is a significant help to scientists to test claims using the crowd. There are many formal sciences: logic, mathematics, theoretical computer science,information theory, systems theory, decision theory, statistics and any domain that has a formal simulation model. SCG in the cloud will help any program officer in any of those fields.


Our SCG (Scientific Community Game) work is about "optimal network design" which tries to make the scholars in a lab optimally productive through careful mechanism design. The sciences we use are: logic, mathematics, algorithms, and psychology.

We have a web page on the SCG which contains a lot of information about the use of our system and its evolution:

The thesis proposal:

contains the best incarnation of SCG so far. SCG has the useful property that SCG can use the crowd to improve any formally specified part of SCG.

Our research on SCG started in 2007 with seed funding from Novartis ($150000). Our research plan is to continue refining our crowdsourcing model based on actual crowdsourcing results with real crowds. When the system is in full use, we envision thousands of labs in the cloud where problems important to society are solved collaboratively and competitively.