کشف قضایا در تئوری بازی ها: بازی های دو نفره همراه با بازپرداخت منحصر به فرد تعادل نش خالص

In this paper we provide a logical framework for two-person finite games in strategic form, and use it to design a computer program for discovering some classes of games that have unique pure Nash equilibrium payoffs. The classes of games that we consider are those that can be expressed by a conjunction of two binary clauses, and our program re-discovered Kats and Thisseʼs class of weakly unilaterally competitive two-person games, and came up with several other classes of games that have unique pure Nash equilibrium payoffs. It also came up with new classes of strict games that have unique pure Nash equilibria, where a game is strict if for both player different profiles have different payoffs.

This paper pursues the perspective of Lin [11,12] that many interesting theorems can be automatically discovered by first specifying a class of conjectures in a logical language and then testing them systematically in some small domains. This approach presents at least two challenges. The first concerns how to come up with a set of reasonable conjectures. This raises further issues, such as how to represent these conjectures, what is the yardstick for reasonableness, etc. The second concerns how to prove or refute the conjectures automatically. In general, using computers to discover theorems is a difficult endeavor. Nonetheless there have been various attempts. In one pioneer work, Petkovsek et al. [15] showed that to prove the following theorem, “The angle bisectors of every triangle intersect at one point”, it suffices to verify it in 64 non-isomorphic triangles, which can be automated by computers. In the same spirit, the authors went on to demonstrate that certain forms of theorems concerning the close form of the sum of combinatorial sequences can be completely discovered by computers programs. Langley [5] had briefly summarized the attempts of computer-aided discovery until 1998, ranging from mathematics to physics, chemistry as well as biology. Among those attempts, Lenat’s AM system [6] and Fajtlowicz’s Graffiti [2] are also remarkable progresses on theorem discovery. The AM system aims at finding new concepts and theorems based on existing concepts as well as a large amount of heuristic rules, which require extensive domain knowledge of the designers. Despite the complexity of design, the system managed to rediscover hundreds of common concepts as well as simple theorems. The Graffiti system, on the other hand, is more intuitive in design. First of all, the system itself does not attempt to prove anything. Alternatively, it aims at generating interesting conjectures in graph theory by guessing and testing some invariants, most of which are of forms a  b, a = b, and ai bi , concerning two numerical features in a graph. It is worth some attention that Graffiti maintains the quality of the set of conjectures by filtering those implied by existing ones. In other words, the current set of conjectures are the strongest ones generated so far. This is similar to our approach in game theory, which will be introduced in detail later. Our work here continues the line of work in [11,9]. In both papers, the problem domain is formulated in a symbolic language. Conjectures about the domains are then represented by sentences in the underlying language. A computer program is then used to test through these conjectures to find those that are true in domains up to certain small size. These conjectures are either guaranteed to be true in the general case or checked manually. A parallel work applies the same idea on social-choice theory [10,17], where we prove three of the most important impossibility theorems in a unified computer-aided framework. We also similarly discover several theorems that generalize Arrow’s conditions as well as a new theorem that better interprets Arrow’s IIA condition. Interestingly, this approach has recently been proved effective in finding impossibility theorems in another field of social choice [3]. Similar idea can be found in automated mechanism design [7,8], where they use several parameters as domain language to describe a class of auctions and then search through the language to find the revenue-optimal auctions. In this paper, we will show how the same methodology can be used to discover some interesting theorems about pure Nash equilibria. Traditional equilibrium analysis has been mostly focused on mixed strategy equilibria. Part of the reasons for this bias is that such an equilibrium always exists and algorithms such as the one by Lemke–Howson are guaranteed to find one. Moreover, best response functions in games with mixed strategies are continuous and differentiable, allowing for standard calculus techniques to be applied. However, pure Nash equilibria (PNEs) are also of interest, and there is already much work about them. Examples here include the existence of PNEs in ordinal potential games [13], quasi-supermodular games [20] as well as games with dominant strategies, and uniqueness of PNE payoffs1 in two-person strictly competitive games [14]. As part of our project on using computers to discover theorems in game theory, this paper considers the possibility of using computers to discover new classes of two-person games that have unique PNE payoffs. Here is an overview of our project.• Step 1. We first formulate the notions of games, strictly competitive games and PNEs in first-order logic. Under our formulation, a class of games corresponds to a first-order sentence. • Step 2. We then consider sentences that have similar syntactic form as that of strictly competitive games. • Step 3. We prove that a sentence of this form is a sufficient condition for a game to have a unique PNE payoff iff it is so for all 2×2 games. • Step 4. We then generate all sentences of the form in step 2, and check if any of them is a sufficient condition for a 2×2 game to have unique PNE payoff. • Step 5. Finally, among these sufficient conditions, we collect weakest ones. We did not expect much as these conditions are rather simple, but to our surprise, our program returned a condition that is more general than the strict competitiveness condition. As it turned out, it exactly corresponds to Kats and Thisse’s [4] class of weakly unilaterally competitive two-person games. Our program also returned some other conditions. Two of them capture a class of “unfair” games where one player has advantage over the other. The remaining ones capture games where everyone gets what he wants – each receives his maximum payoff in every equilibrium state, thus there is no real competition among the players. Thus one conclusion that we can draw from this experiment is that among all classes of games that can be expressed by a conjunction of two binary clauses, the class of weakly unilaterally competitive games is the most general class of “competitive” and “fair” games that have unique PNE payoffs. Of course, this does not mean that the other conditions are not worth investigating. For instance, sometimes one may be forced to play an unfair game. For the same set of conditions, we also consider strict two-person games where different profiles have different payoffs for each player. Among the results returned by our program, two of them are exactly the two conjuncts in Kats and Thisse’s weakly unilaterally competitive condition, but the others all turn out to be special cases of games with dominant strategies. Motivated by these results, we consider certain equivalent classes of games, and show that a strict game has a unique PNE iff it is best-response equivalent [16] to a strictly competitive game. This turns out to be a new and interesting result, and has recently been published in Games and Economic Behavior [18]. The rest of the paper is organized as follows. We first review some basic concepts in two-person games in strategic form, and then reformulate them in first-order logic. We then show that for a class of conditions, whether any of them entails the uniqueness of PNE payoff needs only to be checked on games up to certain size. We then describe a computer program based on this result, and report our experimental results.

We have provided a logical framework for computer-aided theorem discovery in two-person game theory, and applied it successfully to the task of discovering classes of two-person games with unique PNE payoffs. Our program returned a condition that is more general than the strict competitiveness condition, namely, the weakly unilaterally competitiveness. Two conditions, which we coin “I-compete-you-cooperate”, capture a class of “unfair” games where one player has advantage over the other. The remaining ones capture games where everyone gets what he wants – each receives his maximum payoff in every equilibrium state, thus there is no real competition among the players. Thus one conclusion that we can draw from this experiment is that among all classes of games that can be expressed by a conjunction of two binary clauses, the class of weakly unilaterally competitive games is the most general class of “competitive” and “fair” games that have unique PNE payoffs. For the same set of conditions, we also consider strict two-person games where different profiles have different payoffs for each player. Among the results returned by our program, two of them are exactly the two conjuncts in Kats and Thisse’s weakly unilaterally competitive condition, but the others all turn out to be special cases of games with dominant strategies; others correspond to games with dominant strategies. Motivated by these results, we consider certain equivalent classes of games, and show that a strict game has a unique PNE iff it is best-response equivalent to a strictly competitive game. There are many directions for future work. An obvious one is to see how interesting theorems can be discovered using Theorem 1 on classes of games that do not have any PNE and games whose PNEs are Pareto optimal. More importantly, we would like to see how this methodology can be applied on classes of game that has at least one PNE. In fact, we recently have found that two such classes, potential games and supermodular games are best response equivalent [18]. Our program also shows there are other classes of games that do not belong to either class but still have at least one PNE. This suggests a new research direction: a characterization of these games. An even more interesting direction is to come up with a language that can effectively represent mix strategy equilibria and then conduct our theorem discovery method on this setting.