Crowdsourcing Formal Decision Making Using Generalized Semantic Games
We are after a Wikipedia for formal scientific knowledge; a crowdsourcing system where the crowd takes positions on interpreted predicate logic statements (a.k.a. claims) and objectively argues the positions through Semantic Games (SGs). SGs are zero-sum, two-person games where players take two contradictory positions on claims and exchange examples and counter-examples to support their positions and dispute their opponent's positions.
SGs provide an attractive basis for solving some key challenges that face crowdsourcing systems. More concretely, 1) the challenge of defining user contributions is to some extent solved by SGs because SG players interact through a formal well-defined protocol. However, an SG is a binary interaction mechanism that needs to be scaled to the crowd. 2) SGs provide a basis for solving the challenges of evaluating users and their contributions because, under certain restrictions, SG winners are more likely to be stronger than their opponents, and the contributions of SG winners are more likely to be true than the contributions of their opponents. However, the system either has to guarantee those restrictions or somehow compensate for their absence. 3) SGs are fun to play, again under certain restrictions, and thus help address the user retention challenge. However, the challenge of combining user contributions is not addressed by SGs. The system should combine the results of several SGs to better evaluate users and their contributions.
Our proposed system can be applied to crowdsource the building of a formal scientific knowledge base, the development of algorithms for solving formally-specified computational problems as well as to educate and evaluate users.
We developed a proof of concept implementation that employs first-order logic to express claims and two algorithms to evaluate users and their contributions. We did not provide a particular Crowd Interaction Mechanism (CIM), instead we provided an architectural principle to organize CIMs that alleviate some of the concerns related to the meaningful evaluation of users. With the help of the committee members, we propose the following contributions: 1) to develop an SG-based Crowd Interaction Mechanism (CIM). 2) to generalize SGs, beyond arguments based on examples and counter-examples alone, to arguments that involve reductions (and other relations between claims). 3) to develop an evaluation algorithm for users and their contributions for generalized SGs.
Due to a funding crisis, our plan is to finish most of the work during the first three months of the summer.
A short description of his work is on the above home page.
Ahmed's PhD thesis topic is on the design and utility of crowdsourcing of formal scientific knowledge. We envison a wikipedia of formal scientific knowledge where the constructive knowledge of a discipline is presented in labs inhabited by scholars. The knowledge is represented as interpreted logic statements. The constructions are algorithms to refute the false statements and to defend the true ones using generalized semantic games.
The proposed dissertation makes significant contributions to how to (1) organize and evaluate scientific activity in formal sciences, (2) improving peer teaching and student interaction and evaluation in (online) courses in formal sciences (3) crowdsource software development for formally-specified problems. For example, any formally-specified computational problem of the crowdsourcing platform can be improved through crowdsourcing, making the approach reflexive.
His thesis work brings together five areas: (1) crowdsourcing (Christo Wilson), (2) programming languages and formal methods (declarative programming for the global brain using generalized semantic games), (3) task-specific social network design, (4) game design (Casper), (5) mining information networks (Yizhou published a book on this topic).
We have three challenges in developing our system. The expertise of committee members is relevant to at least one of these three challenges. Details are described below:
1) The crowd interaction mechanism defines when users can make certain contributions. The main challenge is to design a simple, semantic-game-based mechanism that balances the product (a.k.a. meaning) of our system with the restrictions it puts on users' behavior. This perfectly fits the expertise of Casper and Amy.
2) How to generalize Semantic Games to handle reductions, specializations, and other claim relations? This fits Thomas' expertise in logic and Formal Methods. It also fits Amy's expertise in using different kinds of logic for predicting and influencing crowd behavior.
3) How to meaningfully evaluate users and their contributions (taking positions and supporting actions) especially for generalized semantic games. This fits the expertise of Yizhou.
-- Karl Lieberherr, April 11, 2013.