Modeling Formal Science for Progress and Learning on the Web

The "Scientific Community Game" work by Ahmed Abdelmeged and Karl Lieberherr defines an approach to model formal science and to define a set-up for social networks for formal science to be used for advancing and teaching formal science. The description below describes our vision, independent of the various applications to crowdsourcing and solving computational problems. For further information, see: SCG-Publications and specifically Thesis Proposal by Ahmed Abdelmeged, Crowdsourcing of Computational Problem Solving, CCIS Technical Report NU-CCIS-2013-10, March 2013.

We describe a generic game, called the Scientific Community Game (SCG), for the Popperian Scientific Method. Popper, one of the most influential philosophers of science of the previous century, promoted in ``Conjectures and Refutations'' the idea that each claim should have a description how to refute the claim. We use relative refutation, not absolute refutation.

SCG is a game designed to encourage constructively-solvable disputes about a predefined set of claims. The reason we want to encourage those constructively-solvable disputes is that they help advance and focus the scientific discourse and learning.

Formal Science and Simulators

We use the following variant of Popper's ideas: We take any science that is sufficiently well understood so that we have efficient simulation software that defines a sufficiently precise computable model. In biology, this is called an ``in-silico'' science. SCG applies to formal sciences. Unlike other sciences, the formal sciences are not concerned with the validity of claims based on observations in the real world, but instead with the properties of formal systems based on definitions and rules. Examples of formal sciences are many: logic, mathematics, theoretical computer science, information theory, systems theory, decision theory, statistics, etc.

We consider a lab that formulates claims about the science. We have several lab users, called scholars, who form their opinions about the claims of the lab. Then they meet in pairs on the web and engage in a scientific discourse to determine who has likely the correct opinion. This determination is done by playing several binary games in which the players assume the position they believe is true.

An example of a domain that is sufficiently well understood is robotics. To program your robot and see it in action you don't need a real robot but the Robot Operating System (ROS) with Gazebo and a some libraries, such as a physics simulation library. See http://www.ros.org/wiki/ and http://gazebosim.org/. ROS and Gazebo provide a framework to use SCG to develop and teach robotics algorithms and the integration of various robotics components.

Contradiction-Agreement Game

In our version of Popperian Science, each claim c has a two-person game CAG(c,s1,s2,p1,p2) attached that defines what is needed by the scholars s1 and s2 to defend their positions p1 and p2 of a claim c in a specific lab. CAG stands for contradiction-agreement game.

The claims are grouped into claim families that we call labs. The purpose of the CAG game is to (1) ask the scholars s1 and s2 to show a personal performance of the skills needed to defend the true claims in the lab (2) evaluate the scholars with respect to their skills relevant to the lab (3) bring at least one of the scholars into a ``personalized'' contradiction. This does not mean that the position of the scholar who got into the contradiction is false. But it is an indication that it might be false casting doubts on the skills of the scholar who took the position. The personalized contradiction has the flavor: you predict an outcome of an experiment connected to the claim and involving the two scholars but when the experiment is carried out the predicted outcome does not happen.

During the game the scholars try to push each other into contradictions and the one who succeeds, gets a point. The winner teaches a lesson to the other scholar because she or he was self-contradictory. We use the points a scholar collects as a first approximation of the strength of the scholar. See our SCG-strength algorithm that gives the details of how we take the strength of the opponents into account. The two scholars p1 and p2 play two roles: p1 takes role r1 and p2 takes role r2, where r1 and r2 are either the verifier or falsifier roles. We take a personalized interpretation of defense and refutation which is with respect to two scholars p1 and p2. p1 and p2 assume the roles verifier or falsifier and then the game determines the winner which gives evidence that the position taken is correct (but it does not prove that the position taken is correct). Special attention is given to the situation when one scholar is forced, e.g., when both scholars want to be verifiers.

Novelty

We provide a new model for formal science that has a much lower barrier of entry. The purpose of SCG is to collect arguments for and against claims and to develop and learn refutation strategies. Scholars don't have to prove their refutation strategies to be correct. A key novelty is that scholars are evaluated by CAGs independent of the ``correctness'' of scholar contributions. CAG-based evaluation can objectively judge one contribution to be better than the other.

Scholar Contributions

During playing a CAG, scholars make two kinds of contributions to the science: positions and supporting actions. Furthermore, they contribute by improving their play based on the feedback through the supporting actions. Because scholars need to follow the protocol behind CAG, scholars may produce an avatar to act on their behalf. The software in the avatar is another contribution.

Evaluating Scholars

CAGs provide an objective and self-sufficient approach to assess the relative strength of users.

Which CAGs to play?

SCG must decide which CAGs to play. A useful way to organize this is to use algorithms to match claims with scholars based on preferences of scholars and SCG and Lab owner. SCG has several CONCERNS it needs to balance. See Ahmed's thesis proposal for the definition of the 10 CONCERNS.

The Social Network and Its Purpose

Scholars all over the world join the labs of their choice and engage in the scientific dialogs implied by the CAGs being played in each lab. The purpose of SCG is to estimate the likelihood that a given claim is true. We achieve this in two steps: we first determine the strength of the scholars and use this information to estimate the likelihood that each claim is true. The strongest scholars in a lab will have the best skills for defending the true claims (and refuting the false ones).

Progress Property

CAGs ensure that progress is taking place for individuals or for the community. This property is stated as: There is a win/loss or there is a meaningful contribution. In the first case, the winner gives targeted feedback and in the second case, the community benefits from the meaningful contribution.

Level the Boats

To further help with progress, it is advisable to "level the boats" from time to time and make all knowledge about winning strategies public. Then the competitions can start again and hopefully reach a higher level.

As a word of caution, SCG is very useful and broadly applicable, but it is not a panacea: SCG has the garbage-in garbage-out property. When the scholars in SCG are not giving their best, they will create a knowledge base of claims which has a minimal value. But it takes only one strong scholar to significantly improve the quality of the knowledge base.

Science is modeled by labs and lab relations. Lab relations are the tool to modularize labs and break them down into components. Labs are based on a computable model (structure). Each lab contains a family of related claims that are closed under negation. Central is a Contradiction-Agreement Game abbreviated CAG. Each claim c has a game CAG(c,s1,s2,p1,p2) associated with it that involves two scholars s1 and s2 and their positions p1 and p2. p1 and p2 are either verifier or falsifier. If s1 believes the claim is true, s1 will choose verifier as s1's position and if s2 believes that c is false, s2 will choose falsifier as s2's position. CAG(c,s1,s2,

Properties of CAGs

CAG encourages innovation because forced scholars can score while their adversary cannot. This provides an incentive for forced players to win even though they are forced to take positions that are often contradictory to their own intuition as well as to the predominant beliefs.

CAGs ensure that some form of progress is taking place either as an update to the player scores or that a potentially correct contribution has been made. In the first case, the loser is receiving targeted feedback and in the second case, the community benefits from the potentially correct contribution.

We define: !verifier = falsifier, !falsifier = verifier. p, p1, p2 are variables that are of type position = (verifier,falsifier).

CAG(c,s1,s2,p1,p2) returns a pair: (payoff(s1),payoff(s2)) if p1!=p2. The scholar with the higher payoff is the winner. If p1=p2, CAG returns two pairs. CAG(c,s1,s2,p1,p1)= CAG(c,s1,s2,p1,!p1) followed by CAG(c,s1,s2,!p1,p1).

The CAG has several interesting properties. We assume that s1 and s2 play the same moves on both games. CAG(c,s1,s2,p1,p2)=CAG(!c,s2,s1,!p1,!p2).

Game CAG(c,s1,s2,p,!p) must have the following property: If both scholars could freely choose their position: Game CAG(c,s1,s2,p,!p)=(1,0) means that s1 has pushed s2 into a contradiction and s1 gets a point. Game CAG(c,s1,s2,p,!p)=(0,1) means that s2 has pushed s1 into a contradiction and s2 gets a point. The situation is different when the second scholar is forced.

SG(c,s1,s2,p,!p(forced))=(0,0). The justification is that the forced scholar is not penalized for losing a lost position.

SG(c,s1,s2,p,!p(forced))=(,0,1).

s1 defends claim c against s2: SG(c,s1,s2,verifier,falsifier)=(s1,1,0).

s1 refutes claim c against s2: SG(c,s1,s2,falsifier,verifier)=(1,0).

Defending a claim c = refuting !c: SG(c,s1,s2,p,!p)=(1,0) iff SG(!c,s1,s2,!p,p)=(1,0).

In summary, it is enough to consider the following three kinds of games: SG(c,s1,s2,p,!p) and SG(c,s1,s2,p,!p(forced)) and CAG(c,s1,s2,p,p). What is important is whether the scholars assume different roles or not and whether a player is forced.

Are there interesting CAGs?

Details about the CAG have been left open intentionally. SCG applies to Formal Science where claims are expressed in some logic. We choose logics that have the concept of a semantic game attached. For example, predicate logic or its generalization, called Independence-Friendly logic. Using those semantic games gives CAG(c,s1,s2,p,!p) a precise meaning based on the structure of c. But this is beyond the topic of this web page. See Ahmed Abdelmeged's thesis proposal and the related papers.

Page edited by Ahmed Abdelmeged and Karl Lieberherr.