% This is lnicst.tex the demonstration file of the LaTeX macro package for % Lecture Notes of the Institute for Computer Sciences, Social-Informatics % and Telecommunications Engineering series from Springer-Verlag. % It serves as a template for authors as well. % version 1.0 for LaTeX2e % \documentclass[lnicst]{svmultln} % \usepackage{makeidx} % allows for indexgeneration \usepackage{amsfonts} \usepackage{color,amsmath,times,url,xspace} \newcommand{\period}[1]{#1\xspace} \newcommand\demj{DemeterJ} \newcommand\robot{\period{agent}} \newcommand\Robot{\period{Agent}} \newcommand\robotp{\period{agent}} \newcommand\robots{\period{agents}} \newcommand\robotsp{\period{agents}} %\newcommand\SDG{Specker Derivative Game\ } \newcommand\SDG{\period{Specker Challenge Game}} \newcommand\SCG{\period{Specker Challenge Game}} %\newcommand\SDGp{Specker Derivative Game} \newcommand\SDGp{Specker Challenge Game} \newcommand\SCGp{Specker Challenge Game} %<<<<<<< .mine %\newcommand\Scholarp{Scholar} %\newcommand\scholarp{scholar} %\newcommand\scholar{scholar\ } %\newcommand\scholarsp{scholars} %\newcommand\Scholars{Scholars\ } %\newcommand\scholars{scholars\ } %\newcommand\SCGAvatarp{SCG/Avatar} %\newcommand\SCGAvatar{SCG/Avatar\ } %\newcommand\SCGBoardp{SCG/Board} %\newcommand\SCGBoard{SCG/Board\ } %======= \newcommand\Scholarp{\period{Scholar}} \newcommand\scholarp{\period{scholar}} \newcommand\scholar{\period{scholar}} \newcommand\scholarsp{\period{scholars}} \newcommand\Scholars{\period{Scholars}} \newcommand\scholars{\period{scholars}} \newcommand\SCGAvatarp{\period{SCG/Avatar}} \newcommand\SCGAvatar{\period{SCG/Avatar}} \newcommand\SCGBoardp{\period{SCG/Board}} \newcommand\SCGBoard{\period{SCG/Board}} %>>>>>>> .r148 \newcommand\WolframAlphap{WolframAlpha} \newcommand\etc{{\it etc.}} \newcommand\eg{{\it e.g.}, } \newcommand\ie{{\it i.e.}, } \newcommand\wrap[1]{\langle #1\rangle} \newcommand\mathsc[1]{\text{\sc #1}} \newcommand\gap{\;\;} \newcommand\pubsec[1]{\langle#1\rangle} \newcommand\op[1]{\mathit{#1}} \begin{document} \mainmatter \title{The \SCGp \ for Education and Innovation in Constructive Domains} \titlerunning{\SCGp} \author{Karl Lieberherr \and Ahmed Abdelmeged \and Bryan Chadwick} \authorrunning{Lieberherr et al.} % abbreviated author list (for running head) % %%%% list of authors for the TOC (use if author list has to be modified) \tocauthor{Karl Lieberherr, Ahmed Abdelmeged, Bryan Chadwick} \institute{ College of Computer \& Information Science\\ Northeastern University, 360 Huntington Avenue \\ Boston, MA, 02115 USA.\\ \email{{lieber,mohsen,chadwick}@ccs.neu.edu} } \maketitle {\em Dedicated to Ernst Specker to celebrate his 90th birthday.} %\begin{abstract} % \keywords{} %\end{abstract} % RawMaterial -> ChallengeInstance % FinishedProduct -> Solution \section{Introduction} We have the following vision: To teach a constructive domain (e.g., domains in computer science, mathematics, engineering, etc.), we design a domain-specific game where the winning students demonstrate superior domain knowledge. The game is simple: the students make constructive claims about the domain we want to teach and refute each others' claims. The students who are the most successful in defending their claims and in refuting the claims of others win the game. Some benefits of the game are: (1) the students give each other constructive feedback about their claims. Students who lose points gain knowledge to improve their game in the future. (2) Although the students are egoistic, maximizing their points, they create a common good: knowledge. The claims that have not been successfully opposed are candidates for truth. (3) The game is fun and adjusts to the skill levels of the students. It can be played productively by undergraduates as well as by world-class researchers to push the state-of-the-art in a domain. The game also serves as a useful, and novel software development process to develop software for computational problems. %introduce claims, refutation protocol \section{Claims and Refutation Protocols} At the heart of the game are two major concepts, those of \textit{claims} and a corresponding \textit{refutation protocol}. Claims are made by one student, Alice. Alice is then engaged with another student, Bob, in an instance of a refutation protocol to determine if Alice would be able to successfully support her claim. Or if Bob would be able to successfully refute Alice's claim. Or if both Alice and Bob will tie. \subsection{Claims in a Nutshell} We distinguish between mathematical and non-mathematical claims. \begin{itemize} \item{Mathematical.} Those claims can be written as a mathematical statement that is either true or false. For example, $\exists (c,n_0)\ s.t.\ \forall n\geq n_0\ :\ n^{1/2} \leq c * (log(n))^{10}$. For those claims we can determine in principle in advance that we have a winning strategy for supporting or refuting them. \item{Non-Mathematical.} Those claims take the form of ``I can construct a problem, knowing a very good solution for it that you cannot beat''. or ``If you construct a problem, knowing a very good solution for it, I can beat your solution". For those claims we cannot guarantee logically that we will win. We must play out the game and the refutation protocol will decide. An example of a non-mathematical claim is the claim for the Maximum Independent Set problem shown below or the claims in the renaissance game. \end{itemize} % For % a slightly more concrete discussion, imagine that we have two % students, Alice and Bob, who argue about a statement in some % domain. Alice thinks the statement, or claim, is true, and Bob % believes it is false. The claim is defined by an instantiation of a % generic refutation protocol: \subsection{Refutation Protocol in a Nutshell} The refutation protocol involves a message exchange between both students, Alice and Bob, and a trusted third party called the administrator. The administrator serves as a mediator for messages; Alice and Bob communicate only to the administrator and the administrator forwards their messages to the other party. The administrator also serves as a referee that decides who succeeds in the protocol. The exact sequence of messages exchanged messages depends on the claim. We assume that all three parties have agreed on a claim made by Alice. If the claim was of the form $\exists x \in X\ s.t. \forall y \in Y(x): predicate(x,y)$. Then Alice has to provide an $x \in X$ such that Bob cannot find a $y \in Y(x)$ that makes $predicate(x,y)$ false. On the other hand, if the claim was of the form $\forall x \in X\ \exists y \in Y(x): predicate(x,y)$, then Bob has to provide an $x \in X$ such that Alice cannot find a $y \in Y(x)$ that makes $predicate(x,y)$ true. In general, a pair of messages needs to be exchanged per every pair of alternating qualifiers in the claim. To handle non-mathematical claims, $x$ may be extended to have an optional secret part that is used to hold the secret solution. The administrator does not pass the secret along to the other party, instead it stores it locally and uses it later in deciding on a winner. Note that Alice is not required to prove her claim, neither is Bob required to disprove Alice's claim (unless the refutation protocol explicitly requires them to exchange proofs). Claims are supported or refuted via examples and counter examples. Therefore, if Alice successfully supports her claim (Alice wins), it does not mean that her claim is true. It could be that Bob made a mistake. If Bob successfully refuted Alice's claim (Bob wins), it does not mean that the claim is false. It could be that Alice made a mistake. However, we can state the following properties of the game: If Alice is perfect and Bob wins, the claim is false. If Bob is perfect and Alice wins, the claim is true. By "perfect" we mean making the best decisions to win the game. % When the admin $x=\pubsec{\op{public}(x), % \op{secret}(x)}$ % % A portion (\eg round) of the game essentially proceeds as follows. % Alice produces message, consisting of a \textit{public} and % \textit{secret} part, $\pubsec{\op{public}(x), \op{secret}(x)}$, with % $x$ drown from some domain $X$. She sends $\op{public}(x)$ to Bob and % sets $\op{secret}(x)$ aside. Bob looks at $\op{public}(x)$ and % produces a corresponding message, $y(\op{public}(x))$, drawn from some % domain $Y$. Once Bob produces $y(\op{public}(x))$, then Alice reveals % $\op{secret}(x)$ to Bob, and the winner is determined by a predicate % $\op{refute}$ such that if $\op{refute}(x, y(\op{public}(x)))$ holds % then Bob wins, otherwise Alice wins. The refutation protocol may more % complex consisting of several moves. In each move, a piece of $x$, % say $x_1$, and a piece of $y$, say $y_1(x_1)$ are produced. In some % refutation protocols the order may be reversed, so Bob produces $x$ % and Alice produces $y$. % % The refutation protocol is parameterized by sets $X, Y, % \op{Public}(X)$, $\op{Secret}(X)$, and a $\op{refute}$ function. A % claim is a tuple % $(x,\,y,\,\op{public}(x),\,\op{secret}(x),\,\op{refute})$ used to % instantiate the refutation protocol with an additional confidence % factor in $[0,1]$. % % The meaning of the interaction is that Alice claims that she can % create an $x$ such that regardless of the $y$ Bob creates, % $\op{refute}(x,y(\op{public}(x)))$ will be false. Before Bob % challenges Alice on her claim, he must carefully study the refutation % protocol and the claim to decide whether it is worth while (\ie % profitable) to challenge Alice. Only if he sees a winning strategy % should he try to challenge the claim. The game is fair as long as % Alice and Bob have a clearly defined protocol to determine the % refutation of the claim. \subsection{Claim Design} Claim design must follow a few principles. Mathematical claims that come from interesting theorems with an even number of alternating quantifiers are good candidates for claims. This is folklore knowledge. The claims must have the property that it is "challenging" for Alice to produce her $x$ and for Bob to produce his $y$ (knowing $x$). It must be "challenging" for Alice to produce claims that cannot be refuted. It must be "challenging" for Bob to analyze a claim to reach the refute decision. Another issue in claim design is privacy. The information that is exchanged between the players should not reveal too many secrets. Otherwise, the players are less motivated to develop new ideas. Claim design for educational purposes may have an indirect flavor. For some simple claims, a significant amount of material needs to be mastered that is not at all mentioned in the claim formulation. \subsection{Examples} \subsubsection{O Notation} How can we engage our students in a constructive discussion about the big O notation. The instructor prepares for them a set of claims to choose from and Alice chooses the following claim: $n^{1/2} = O((log(n))^{10})$. The parameters to the refutation protocol are: $X=\mathbb{R}^+ \otimes \mathbb{R}^+$, where $\mathbb{R}^+$ is the set of positive real numbers, and $Y=\mathbb{R}^+$. There are no secrets in this case. The refute function is $\op{refute}((C,n_0),n) = (n < n_0) \lor (n^{1/2} > C \cdot ((log(n))^{10}))$. The refutation protocol is: Alice finds $x = (C, n_0)$ and Bob finds $n \geq n_0$ so that refute returns true. After playing this game a few times, Bob starts to refute consistently and they start looking for a reason. They remember a theorem from calculus: $\op{log}(n) \in O(n^x )$ for every $x>0$. \subsubsection{Highest Safe Rung Problem} How can we engage our students in a constructive discussion about search, from linear search to binary search and what is between? Along the way, we want to teach them about binary decision trees and attempting to minimize the longest root-to-leaf path in such trees. More importantly, they learn about deriving and solving equations and analyzing the asymptotic behavior of functions. We do this by engaging the students in the following game between Alice and Bob. The game is based on the following problem from \cite{Kleinberg:1051910}: You are doing some stress-testing on various models of glass jars to determine the height from which they can be dropped and still not break. The setup for this experiment, on a particular type of jar, is as follows. You have a ladder with $n$ rungs, and you want to find the highest rung from which you can drop a copy of the jar and not have it break. We call this the highest safe rung. You have a fixed ``budget'' of $k \geq 1$ jars. By $\op{HSR}(n,k)= q$ we summarize Alice' claim that she can determine the highest safe rung for a ladder on $n$ rungs and a budget of $k$ jars with at most $q$ experiments. The parameters to the refutation protocol are: $X$ is the set of sequences of questions to Bob of the form $\op{breaks}(j)$: Does the jar break at rung $j$? $Y$ is the set of sequences of answers from Bob of the form true or false. The answers must be consistent: if $\op{breaks}(j_1)$ is true then $\op{breaks}(j_2)$ holds for all $j_2 > j_1 $ and if $\op{breaks}(j_1)$ is false then $\op{breaks}(j_2)$ does not hold for all $j_2 < j_1 $. The refutation function for $\op{HSR}(n,k)=q$ is $\op{refute}(n,k,q, x,y)$ returns true if ($y$ is not consistent with $x$) or ($y$ contains more than $k$ true answers) or ($x$ contains more than $q$ questions) or the highest safe rung is not uniquely determined. We give the following claims to choose from: $\op{HSR}(9,2)=6, \op{HSR}(9,2)=5, \op{HSR}(9,2)=4, \op{HSR}(9,2)=3.$ Alice chooses claim $\op{HSR}(9,2)=4$ after finding a decision tree whose longest root to leaf path is 4. Bob also tries to find a decision tree of depth 4 but he cannot. Therefore Bob decides to refute Alice' claim. However, Alice successfully defends her claim. Bob tries to improve his decision tree construction based on the input he got from Alice through the game and he now also succeeds to find a decision tree for $\op{HSR}(9,2)=4$. \subsubsection{Maximum Independent Set} An independent set in a graph is a set of mutually nonadjacent vertices. The problem of finding a maximum independent set in a graph, IndSet, is one of most fundamental combinatorial NP-hard problems. The refutation protocol is: Alice constructs a graph $G$ with at most $n$ nodes and deposits her secret independent set $I_1$. Alice gives $G$ as well as the size of $I_1$ to Bob. In other words, $I_1$ is a secret for now. Bob has 10 minutes to construct his independent set $I_2$ which he gives to Alice and she checks it. Alice reveals her secret set $I_1$ and Bob checks it. Bob wins iff $\op{size}(I_2) \geq \op{size}(I_1)*0.9$. A few of the topics that students learn while playing the game: The difference between checking and searching algorithms; How to hide secrets; How to search for secrets; Approximation Algorithms. \subsubsection{Min-Max} Calculus is a constructive domain that can be covered with the game using modern tools like \WolframAlphap. We choose claims of the form: $\forall {x \in X} \exists {y \in Y}: f(x,y) \geq c$. The claim is of the form $\forall \exists$, therefore the refutation protocol is (Alice claims, Bob tries to refute): Bob chooses $x_0$. Alice chooses $y_0$. Bob wins iff $f(x_0,y_0) < c$. Example: Claim $\op{GoldenRatio}(c)$: $\op{min}_{x \in [0,1]} \op{max}_{y \in [0,1]} (x*y + (1-x)(1-y^2)) \geq c $, where $c$ in $[0,1]$. If the players are perfect, claim $\op{GoldenRatio}(0.62)$ is refutable while claim $\op{GoldenRatio}(0.61)$ is not. To find out why, calculus knowledge is needed. For mathematical claims like this, it makes sense to close them under negation and also allow: \noindent Claim $\op{NegGoldenRatio}(c)$: $ \exists x \in X \forall y \in Y: f(x,y) < c $. When Bob refutes claim $\op{GoldenRatio}(c)$ successfully, he claims a new claim $\op{NegGoldenRatio}(c)$ to find out whether his refutation was accidental. \subsubsection{Renaissance Games} Consider yourself moved back a few hundred years to the time of the Renaissance in Italy. The mathematicians challenged each other regarding the best algorithms to solve problems. Tartaglia played the role of Alice and Fior the role of Bob in a game about cubic equations. Tartaglia won because he had discovered a technique to solve Fior's equations while Fior could not solve the ones posed by Tartaglia. They used the following adapted refutation protocol: $x$ and $y$ were delivered simultaneously, i.e., $y$ does not depend on $x$. Alice solves Bob's equations and Bob solves Alice' equations. $X = Y$ = sets of cubic equations. $x$ = thirty cubic equations from Alice. $y$ = thirty cubic equations from Bob. $\op{refute}(x,y)=$ Alice solves fewer equations in $y$ from Bob than Bob solves in $x$ from Alice within two hours. Note that those renaissance claims are not mathematical claims in the sense of the Highest Safe Rung claims or the Min-Max claims. Tartaglia could not be 100\% sure that he would win. But he thought that Fior had not discovered the solution technique that he had and this gave Tartaglia a significant edge. But the game is interesting and the winner demonstrates that he/she has better algorithms. \section{The Specker Challenge Game} The Specker Challenge Game (SCG) is a \emph{mechanism} for encouraging a number of players to engage in the refutation protocol described above. The game revolves around one central pool of claims. Players are encouraged to add claims to the pool by either proposing new claims or strengthening existing claims. Players are also encouraged to test claims already existing in the pool through the refutation protocol described above. Players are evaluated based on their contribution to the pool of claims. A contribution is either a non-refuted claim (i.e., a claim that has been successfully defended) or a refutation of existing claims. \subsection{Game Benefits} % what does the game achieve? The game motivates players to participate in a well defined dialog about a specific domain. This is important for educational purposes where students learn about the domain through the dialog. Stirring up the communication between geographically dispersed students in online education environments is a desirable feature. Players are engaged because they will either win the game or win constructive feedback. If Alice loses, she can study the $y$ she got from Bob that made her lose. Maybe the $y$ has a structure that gives a hint at Bob's clever technique for producing $y$. If Bob loses, he can study the $x$ that Alice created. Also, the structured, domain-centered communication between scholars helps stirring up the innovation in a specific domain. A second benefit of the game is the accumulation of knowledge in a structured manner. The central pool of undisputed claims is also a useful byproduct of the game. It represents the state of the art knowledge about the domain. Note that players, scholars in this case, can still keep important pieces of information to themselves. Consider claims of the following algorithmic form: Alice claims she has an algorithm that solves any problem $x$ in $X$ with a solution $y(x)$ in $Y(x)$ that has quality $q(Y(x))$. The refutation protocol is: Bob constructs a hard problem instance $x_0$ in $X$ and Alice must find a solution $y$ of the claimed quality. If she cannot, Bob wins. Note that Alice can keep her algorithm for solving problems in domain $X$ secret and Bob can keep his algorithm for generating hard problems in domain $X$ secret. Yet a central pool of hard problems and some good solutions for them is populated. Games of this kind drive the \scholars towards a common good, although they are egoistic: to find the best algorithm and to pose the hardest problems. The \scholars create social welfare through their egoistic behavior thanks to the mechanism design the game uses. % invites proofs for mathematical claims It is important to notice %\section{Examples} % examples: Bob statically determines winning strategy; focus on those % examples: Bob dynamically determines winning strategy, use meta info about Alice % choices: HSR, O notation, MAX CSP % variations of the game and special cases \subsection{Game Versions} %The above game family describes the core of the \SCGp. \subsubsection{Intensional Vs. Extensional Set of Claims} Before playing the game all three parties need to agree on a how claims are expressed. A domain expert is expected to provide such specification. In the intentional version, the expert defines a language to express a usually huge set of claims that may be proposed. %such as %first order logic or a subset thereof defined through a predicate on the %its syntax. In the extensional version, the expert enumerates the universe of all possible claims that may be proposed. \subsubsection{Board Vs. Avatar} \SCGBoard is the informal version of the game where two students challenge each other and together check the rules of the game. \SCGBoard Extensional is a convenient combination because of its low overhead. The students can control their educational experience by choosing claims in a domain they want to explore further. The universe of possible claims is usually enumerated by the instructor. % \subsection{\SCG Intensional} % For the full version, we use the core game to create a world of scholars % who propose and oppose claims. There is a language of claims defined % by the game designer that permits a huge number of claims % intensionally, rather than extensionally. % % % \subsection{\SCG Extensional} % For some applications of the \SCGp, it is better to formulate a heterogeneous market % of claims from which the scholars must take the claims they propose. % Instead of defining the allowed claims intensionally through a predicate, % they are defined extensionally by enumerating them. % The market of claims is defined by the game designer. % % SCG is also an acronym for Scientific Community Game. % Indeed the scholars compete for reputation and they build, % if the claims are mathematical, % a knowledge base of unopposed claims. % \subsection{\SCGBoard} \subsection{\SCGAvatarp, a Web Application} The main attraction of \SCGAvatar is that players get the opportunity to create their ``organism'' that needs to fend for itself in a real virtual world inhabited by organisms created by other players. %\paragraph This version of the game works well when the domain is sufficiently simple so that the task of proposing and opposing can be easily programmed. \SCGAvatar brings to the game a strong software development component and a very fun competitive/collaborative environment. The avatars live somewhere on the web, written in your programming language of choice, and compete with each other in a full round-robin or Swiss style tournament. We have observed that students during the running game changed their avatar to improve its performance against the avatars of their peers. When they come to class, they get a simple baby avatar that can walk and talk (it can briefly survive on the web) but does not have much intelligence. Then they add intelligence that is hopefully better than the intelligence that their peers add. The game creates a ranking of the avatars that gives feedback to the students about their algorithm and software development skills. The Highest Safe Rung and Min-Max games could be easily played using \SCGAvatar by teaching the avatars enough calculus so that they propose strong claims and successfully refute weak claims. We used a more complex version version of \SCGAvatar based on the Constraint Satisfaction Domain. \subsection{The Scientific Community Game Mechanism} SCG is also an acronym for Scientific Community Game in which \scholars compete for reputation gained by proposing hard to refute claims or refuting existing claims. The game proceeds according to the following rules: \begin{itemize} \item The game is a two player game. \item The game consists of a fixed number of turns. A turn can only take a fixed amount of time. \item \Scholars start with a fixed and equal amount of reputation. \item The sum of reputations remains constant throughout the game. \item There is only one central pool of claims. Initially, the pool is empty. \item Claims contain a real numbered field in the range $[0..1]$ referred to as strength. Claims also contain another real numbered field in the range $[0..1]$ referred to as confidence. \item The credibility of a claim is the result of multiplying their confidence field by the reputation of their proposing \scholar at the time the claim is proposed. \item In each turn except the final turn, every \scholar with a positive reputation must either: \begin{itemize} \item propose at least one new claim to be added to the central pool of claims. \item strengthen at least one claim from the central pool. Strengthening is not possible in the first turn and is not allowed in the final turn. \end{itemize} \item \Scholars can also refute existing claims. \item \Scholars strengthen claims by increasing their strength fields from $s_i$ to $s_t$. When they do so, they gain $(s_t - s_i)$ multiplied by the credibility of the claim. \item \Scholars refute claims by engaging in an instance of the refutation protocol mentioned above. The result is a recognition factor $[-1..1]$. The opposed \scholar reputation gain is the recognition factor multiplied by the credibility of the claim. \end{itemize} Below, we give an explanation/rationale for some of the less obvious game rules: It is important to keep the game a two-player game so that a player can regain its reputation lost when its claims are strengthened by opponents. In a multi-player version, players that come after weak players have the advantage of being able to gain reputation by strengthening and refuting claims made by those weak players. Furthermore, in a multi-player version, players can form coalitions in which one player loses reputation for another player. These kind of coalitions are non-productive from the point of view of the game purpose. The two player requirement is not a limitation though, as a multi-player version can be derived from this two player version via a tournament made up of multiple rounds (such as the Swiss-style tournament used in the FIFA world cups). Confidence is a real number in $[0,1]$ that indicates how confident the proposer is in the claim. The confidence should reflect the amount of effort that has been put into the claim. Confidence $1$ means that we believe that the claim cannot be opposed (i.e. strengthened or refuted). For example, one could use confidence $1$ for a claim for which the \scholar has a proof. Strength is a real number in $[0,1]$ that indicates the strength of the claim. For example, in the min-max domain mentioned earlier, the claim $\forall {x \in X} \exists {y \in Y}: f(x,y) \geq 0.62$ is stronger than the claim $\forall {x \in X} \exists {y \in Y}: f(x,y) \geq 0.61$. In some domains, there is no inherent notion of the strength of the claim, or there is an inherent notion of strength that cannot be expressed by a real number in the range $[0,1]$. The O-notation domain is an example of such domains. In this case, strength is set to $1$ and it is no longer possible to strengthen claims. Claims also have a credibility that is proportional to both it's proposing \scholarp's ``confidence'' in the claim and it's proposing \scholarp's reputation at the time of proposing the claim. Since the sum of reputations is preserved and the initial reputation sum is positive, we are guaranteed to have at least one \scholar with a positive reputation. Scholars with positive reputation are required to be active so that the game is guaranteed to produce an accumulation of claims. \Scholars with positive reputation stay active by either proposing at least one new claim or strengthening at least one existing claim. \Scholars can also try to refute existing claims for a possible reputation gain that will help them win the game. Strengthening a claim is a sort of opposing an existing claim and proposing a new (stronger) claim at the same time. That's why strengthening qualifies both as a proposition and as an opposition at the same time. It is meaningless to propose new claims at the final turn as the players do not gain reputation by proposing new claims they get reputation by successfully supporting their proposed claims. Since there are no more turns for their opponent to try to refute their claims, it becomes meaningless to propose new claims in the final turn. Strengthening is not allowed in the final turn as it makes it possible for a player to get away with reputation gained by over-strengthening an existing claim. It is also essential for \scholars to get the chance to refute the strengthening of their claims made by opponents as they lose reputation when their claims are strengthened by other \scholars. This also enhances the quality of the final set of claims in the central pool as they are less likely to contain overly strong claims. \Scholars with negative reputation cannot propose any new claims or strengthen any existing claims, as their new claims would have negative credibility leading to opponents losing reputation when they strengthen or successfully refute these claims. \Scholars with negative reputation can only try to refute existing claims in order to increase their reputation. The refuting protocol recognizes claims by a recognition factor in $[-1,1]$ A recognition factor of $1$ means that the other \scholar has completely failed to refute that claim. A recognition factor of $-1$ means that the other \scholar has completely succeeded to refute that claim. \Scholarp's final reputation is the sum of the \scholarp's initial reputation plus the reputation gains and losses; thus reflecting the past performance of the \scholarp. The \scholar with the highest final reputation wins the game. There is an issue with the axioms as they are currently formulated: When a \scholar with low reputation refutes the claim of a \scholar with high reputation, the low reputation \scholar will significantly increase its reputation. But when the low reputation \scholar loses, it will also lose a high amount of reputation. This might discourage \scholars with low reputation from ``testing'' claims made by \scholars with high reputation. % The \scholars are encouraged to give their "true" confidence in % a claim. If not, they will be penalized. % The following axioms must be followed by any game mechanism. % They are about how reputation is gained. % \begin{enumerate} % \item % \Scholars gain reputation either by opposing other \scholarsp' claims % or by having their claims recognized by other scholars (when the other % \scholars fail to oppose). % \Scholarp's gain from their claim is proportional to both % the credibility of their claim and the recognition of the claim % after the refuting protocol. % Note: the payoff for strengthening comes after the strengthened claim % is recognized (successfully defended or never opposed). % % \item % One \scholarp's reputation gain is another % \scholar's reputation loss. The sum of all \scholarsp's reputation is preserved. % % % The claim's confidence reflects the amount of effort % made by the \scholar behind the claim to prove the claim (i.e., turning it into a theorem % or finding other supporting evidence). % % \end{enumerate} % % Those axioms define a family of mechanisms that can be used % to implement the game. %We would like to prove theorems like: If an agent Perfect has the perfect %algorithms for challenges C1 ,..., Cn and the other agents do not, %Perfect will win the game if C1 ,..., Cn are offered. % applications contributions \subsection{Equilibrium} SCG has a natural equilibrium state. When all players are perfect, they propose claims that can neither be refuted nor strengthened. The other players will recognize those claims as ``optimal''. Everybody will keep their initial reputation and the game is a tie. In real games with imperfect players, there is a lot of refuting and strengthening happening. \section{Applications} \subsection{Education} The \SCG works very well to create a productive interaction between students of constructive domains, like STEM fields. The \SCG focuses the student interaction on a specific domain and gives the students valuable hands-on experience when they propose and oppose. \subsubsection{Software Development} We have used \SCGAvatar successfully in software development courses. Implementations of $\mathit{SCG}(\mathit{CSP})$ have been used at Northeastern University to teach several semesters of a senior level course on software development~\cite{sdsp09,sdf09}. Throughout the course students learn not only about the rigors of software organization and evolution, but about some details of SAT/CSP algorithms. The feedback from both course staff and regular competitions keeps students involved, putting their best ideas into the avatars. The course invites students to master a wide variety of CS topics ranging from Theory of Computation, Discrete Structures (combinations, permutations, simple combinatorics), Calculus (maximizing and minimizing multi-variable rational functions) to Object-Oriented design and Software Engineering. An important part of teaching is to evaluate whether the students understand the computational processes and whether they can effectively use them in practice. A round-robin contest is the perfect tool to give the students quick feedback how well they do compared to the other students. Furthermore, the agents help each other with testing. When students come to the course, they get a baby agent that must be equipped with intelligence to win. We got reports in Spring 2009 that students were so immersed into the game that they ignored other courses and put all their effort into winning. We used the rule that after two weeks of contests, the source code had to be revealed. This on one hand lead to rapid improvements to the agents but it also contributed to the competitive nature of the game. We plan to further develop our use of the \SCG for teaching Software Development. There is significant value in giving the students a baby agent that they have to nurture into an ``intelligent adult'' using state-of-the-art software development technology. \subsubsection{Algorithms} We have also used SCG successfully in two undergraduate algorithms courses \cite{algf10}. Here we used the ``board'' version of the game (\SCGBoardp) where the two participating students jointly check the game rules. We use the game to help the students to create ideas about how to solve textbook problems. We see value in having students defend claims that are true and refute claims that are false. A successful defense of a claim maybe a baby step towards a proof of the claim. \subsection{Innovation} We believe that the small innovation steps we have observed in undergraduate competitions can be achieved on a larger scale when world-class researchers participate (e.g., PhD students in algorithms) both for \SCGAvatar and \SCGBoardp. \subsubsection{Optimization Problems} How can we drive innovation towards better algorithms for NP optimization problems? NPO is the class of all NP optimization problems. The ingredients to an optimization problem are the set of input instances or problems, the set of feasible solutions, and the measure defined for a feasible solution. In a nutshell, NPO problems are optimization problems whose feasible solutions are short and easy to recognize. For optimization problems, the game proceeds as follows. Alice claims that she has an algorithm to solve a family of optimization problems within a given resource bound and a given solution quality. The refutation protocol: Bob gives Alice a problem $(x)$ in the family and if Alice cannot produce a solution $(y)$ %<<<<<<< .mine %within the given resource bound or the promised quality, Alice loses. %======= within the given resource bound or the promised quality, Alice loses. Solution quality and resource consumption usually manifest in the game in the form of claim strength. %>>>>>>> .r148 Using \SCGAvatarp, we design a virtual scientific community that through the avatar game improves its knowledge. The game is designed in such a way that the winning avatars have the best approximation algorithms for the NPO problems under discussion. \SCGAvatar offers a new way to evaluate algorithms without resorting to an asymptotic analysis. Good asymptotic behavior is important but games are won also by clever implementations that use small constant factors. The problem instances allowed to appear in the game are all bounded by a large constant. \subsection{Better Software Development Process for Computational Problems} Developing software for computational problems is an important ongoing activity. The claims are of the form: $\op{Claim}(X,Q,R)$: I have a program that solves instances in $X$ with quality $Q$ and resource bound $R$. \SCGAvatar provides a new software development process for such software that is based on both collaboration and competition. For example, instead of having 4 people working as one team, we use 2 people to develop Alice and 2 to develop Bob and the competitions between Alice and Bob will improve them. The process works better when more avatars are involved. The benefits of the process are: \begin{itemize} \item{Engages Software Developers.} Nobody wants to see their avatar suffer and being beaten by their peers. The competitions typically run over several hours and we saw software developers stay up at night and improve their avatar between rounds in the same competition. \item{Meaningful Measurement.} The tournament ranking provides an objective evaluation of the avatars and the teams behind them with respect to software development and algorithm skills. The game is designed in such a way that the winning avatar must demonstrate better algorithms and their correct implementation. \item{Encourages Good Software Engineering Properties.} There is a lot of pressure between the competitions to update the avatar's code quickly. This can only be done if the code has good software engineering properties such as modularity. \item{Encourages Good Algorithms.} Winning avatars often have superior algorithmic knowledge that they exploit in the game. \item{Testing.} The avatars are thoroughly tested through the opposing activity. \end{itemize} \subsection{Hiring} Companies can benefit from \SCGAvatar by screening potential employees with the game. When a company seeks algorithmic/implementation skills in a given algorithmic problem solving domain, they define a game for this domain and let potential employees participate. The potential employees might create useful knowledge for which they are compensated. For example, the potential employee competition might create an algorithm that beats the algorithm that was created in-house. \section{Evaluation of the \SCG/ Disadvantages} The \SCGp, because its very flexible refutation protocol, covers a broad area. Because of this coverage, the effort of learning the game can be quickly amortized. But one disadvantage of the game is that students and software developers need to learn the game mechanics of a scientific community. The Avatar version requires a very well functioning game engine to work well. The administrator needs to painstakingly check all avatars whether they follow the rules. The Avatar version requires a software tool to quickly generate baby avatars. We hope to make this parameterized engine freely available but we are not there yet. We found \SCGAvatar to be addictive. Students identified with their avatars and did not want to see them suffer. We had to advise the students to balance their efforts with other courses. %What we hope to prove about the \SCG? \section{Origins of the \SCG} Initially, we used the domain of Boolean CSP: Boolean constraint satisfaction problems, motivated by our joint work with Ernst Specker \cite{jacm-81}. Specifically, our problem domain $X$ was the set of CSP {\it formulas}, where a formula is a sequence of constraints, each over a set of variables. For a given CSP formula $x\in X$ we use $V(x)$ to represent the set of all variables used in its constraints. Feasible solutions, $S(x)$, are assignments to a formula's variables, defined as all maps whose domain is $V(x)$, and range is boolean values, $\{\op{true},\,\op{false}\}$. For CSP, the easiest way to define a sub-domain for a claim (\ie $X'$) is to do so intensionally by giving a set of {\it relations} that can be used to create legal constraints. The function $\op{fsat}(x,s)$, which calculates the fraction of satisfied constraints in $x$ using assignment $s$, is used for predicate descriptions. A \scholar might offer a claim using the relation {\sc 1-in-3}, which is {\it true} when exactly one of its three variables is assigned {\it true}. The claim proposed could be: Alice claims: There exists a CSP formula using only the {\sc 1-in-3} relation so that for all assignments to the formula at most the fraction $0.4$ will be satisfied. $$\wrap{\wrap{\{\mathsc{1-in-3}\},\,Q},\,0.4}\quad\text{with}\;\;\;Q(x,\,s)= (\mathit{fsat}(x,\,s) \le 0.4)$$ \noindent %which represents the claim that solutions to a specific CSP %instance (to be provided) using only the {\sc 1-in-3} relation will %not have a fraction of satisfied constraints greater than $2/5$. If refuted by Bob, the offering \scholar Alice would need to provide a CSP instance using the {\sc 1-in-3} relation, {\it e.g.}: $$x \;\equiv\; \wrap{\,(\mathsc{1-in-3}\;\{a,\,b,\,c\}),\;(\mathsc{1-in-3}\;\{a,\,b,\,d\}),\;(\mathsc{1-in-3}\;\{b,\,c,\,d\})\,}$$ We can quickly see that with the defined predicate, $Q$, it is rather easy to refute the claim given this problem instance. Though not all assignments provide a good fraction of satisfied constraints (\eg the all {\it false} assignment does not satisfy any), there are multiple assignments that do. Two possible solutions and their satisfied fractions are: $$\begin{array}{l} \mathit{fsat}(x,\,\{\,a\mapsto\mathit{false},\,b\mapsto\mathit{true},\,c\mapsto\mathit{false},\,d\mapsto \mathit{false}\,\}) \;=\; 1\;\text{\;\;and}\\ \mathit{fsat}(x,\,\{\,a\mapsto\mathit{true},\,b\mapsto\mathit{false},\,c\mapsto\mathit{false},\,d\mapsto \mathit{false}\,\}) \;=\; 2/3 \end{array}$$ For formulas made only of this relation, {\sc 1-in-3}, there always exists an assignment that will satisfy at least $4/9$ of all constraints. This is known as a {\it P-optimal} threshold for this specific CSP problem~\cite{JA-82}: we can satisfy this fraction quickly (in polynomial time), but to do better than $4/9+\epsilon$ for $\epsilon>0$ makes the problem NP-hard. We get this value by maximizing the polynomial: $3\cdot p \cdot(1-p)^2$, which we derive from the truth table of {\sc 1-in-3}, eventually obtaining the maximum value at $p = 1/3$. \section{Related Work} TopCoder \cite{TopCoder} has connections to \SCGAvatarp. TopCoder offers algorithm competitions where you need to defend your own program and try to find bugs in programs of others. But there are big differences: \SCG has claims which can be flexibly defined while in TopCoder they have a fixed form: I have an algorithm that solves the problem correctly. If you want to refute my claim you must provide a test-input where the code fails. Also in \SCGAvatar the avatars must create claims which is absent in TopCoder. The \SCG is patterned after a real scientific community: This related work is quite old. Scientists are encouraged to offer results that are not easily improved. They must offer results that they can successfully support. They strengthen results, if possible. They must stay active and publish new results or oppose current results. They want to become famous! How to turn predicate calculus statements with an even number of alternating quantifiers into a game is well-known folklore. \cite{1296179} provides excellent background information on SCG. However, the idea of defining games with claims/refutation protocols is not touched. The chapter on Evolutionary Game Theory (chapter 29) is most relevant to SCG, although traditional evolutionary game theory works with infinitely many players. In this world, the players are organisms that meet other organisms from which they buy products and to which they offer products. The 2 organisms play a fixed, 2 player game. % Bench-mark-based competitions %http://www.cs.cornell.edu/courses/cs280/2005fa/quantifiers.pdf %http://www.cs.cornell.edu/courses/cs280/2005fa/boolean.pdf %InnoCentive and similar Open Innovation websites %http://cs-www.cs.yale.edu/homes/jf/econsecurity.html %An Economic Approach To Security %Combinatorial optimization games: http://portal.acm.org/citation.cfm?id=314428 \cite{scghome} gives further information on the \SCGp. \cite{Schell:1252688} provides a good introduction to game design. \cite{Becker:2007:SGC:1292428.1292436} promotes the use of serious games in computer science programs but from a different angle than this paper. %\cite{doi:10.2200/S00108ED1V01Y200802AIM003} %http://www.topcoder.com/wiki/display/tc/Algorithm+Overview \section*{Acknowledgements} We would like to thank Novartis/NIBR for partially supporting the development of the \SCGp. Alex Dubreuil was the teaching assistant for several courses where the \SCG was used and he gave us valuable feedback and encouragement. We would like to thank Pete Manolios for his feedback on the game and to Shriram Krishnamurthi for the Renaissance Game connection. \bibliographystyle{abbrv} \bibliography{references} %\begin{thebibliography}{10} % %\bibitem{Becker:2007:SGC:1292428.1292436} %K.~Becker and J.~R. Parker. %\newblock {"Serious Games + Computer Science = Serious CS"}. %\newblock {\em J. Comput. Small Coll.}, 23:40--46, December 2007. % %\bibitem{Kleinberg:1051910} %J.~Kleinberg and E.~Tardos. %\newblock {\em Algorithm Design}. %\newblock Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2005. % %\bibitem{sdf09} %K.~Lieberherr. %\newblock {Software Development: CSU 670 Fall 2009}. %\newblock Website, 2009. %\newblock \url{ % http://www.ccs.neu.edu/home/lieber/courses/cs4500/f09/cs4500-f09.html }. % %\bibitem{sdsp09} %K.~Lieberherr. %\newblock {Software Development: CSU 670 Spring 2009}. %\newblock Website, 2009. %\newblock % \url{http://www.ccs.neu.edu/~lieber/courses/csu670/sp09/csu670-sp09.html}. % %\bibitem{scghome} %K.~Lieberherr. %\newblock {The Specker Challenge Game}. %\newblock Website, 2009. %\newblock \url{http://www.ccs.neu.edu/~lieber/evergreen/specker/scg-home.html}. % %\bibitem{algf10} %K.~Lieberherr. %\newblock {Algorithms and Data CS 4800, Fall 2010}. %\newblock Website, 2010. %\newblock \url{ % http://www.ccs.neu.edu/home/lieber/courses/algorithms/cs4800/f10/course-desc% %ription.html }. % %\bibitem{JA-82} %K.~J. Lieberherr. %\newblock Algorithmic extremal problems in combinatorial optimization. %\newblock {\em Journal of Algorithms}, 3(3):225--244, 1982. %\newblock % \url{http://www.ccs.neu.edu/~lieber/p-optimal/karl-algo-extremal.pdf}\gap. % %\bibitem{jacm-81} %K.~J. Lieberherr and E.~Specker. %\newblock Complexity of partial satisfaction. %\newblock {\em Journal of the ACM}, 28(2):411--421, 1981. %\newblock \url{http://www.ccs.neu.edu/~lieber/p-optimal/JACM1981.pdf}\gap. % %\bibitem{Schell:1252688} %J.~Schell. %\newblock {\em The Art of Game Design: A Book of Lenses; electronic version}. %\newblock Elsevier, Burlington, MA, 2008. % %\bibitem{TopCoder} %TopCoder. %\newblock {The TopCoder Community}. %\newblock Website, 2009. %\newblock \url{ http://www.topcoder.com/ }. % %\end{thebibliography} \end{document}