Mittelmann, Munyque (2022) Logiques pour la représentation et la conception d'enchères. École doctorale Mathématiques, Informatique et Télécommunications (Toulouse).

Preview

Text Download (1MB) | Preview

Abstract

Une enchère est un mécanisme compétitif qui permet d’allouer un ensemble de ressources auprès d’un ensemble d’agents. Ce mécanisme agrège les offres effectuées par les participants à l’enchère dans le but de produire une décision sociale caractérisée en termes d'allocations et de paiements. Les agents automatisés sont largement utilisés sur les marchés basés sur les enchères, mais ils sont généralement conçus pour agir dans un contexte spécifique. Pour passer d'un type de marché à un autre, les agents doivent être capables de "comprendre" les règles de l'enchère et de raisonner sur leurs valuations ainsi que sur les valeurs privées des autres joueurs. De fait, il est nécessaire de définir un langage simple permettant de représenter les règles d'un marché aux enchères, qui permettra ensuite à des joueurs généraux automatiques de raisonner stratégiquement dans différents environnements. Cet aspect stratégique, notion centrale de la théorie des jeux et des systèmes multi-agents, est de première importance dans la caractérisation des mécanismes d’enchères. Un problème de première importance concerne la conception de nouvelles enchères, ou plus généralement, de nouveaux mécanismes. En effet, un des principaux objectifs consiste à agréger les offres individuelles tout en garantissant un résultat socialement souhaitable. La dimension stratégique est donc au cœur de la conception de mécanismes. Alors que les langages logiques ont été largement considérés dans le contexte des Systèmes Multi-Agents (SMA), l'utilisation de méthodes formelles et de raisonnement stratégique pour la Conception Automatique de Mécanismes a été à peine étudiée. Cette thèse explore l'application des logiques pour la description et la conception de mécanismes d’enchères. Ces derniers placent la dimension stratégique en leur cœur et nous proposons l'utilisation de méthodes formelles pour la spécification, la conception et l'évaluation de mécanismes intégrant cette dimension. Dans un premier temps, afin de fournir une fondation pour les joueurs d'enchères généraux et automatisés dans les SMA, nous proposons un formalisme pour représenter les enchères, appelé Auction Description Language (ADL). ADL traite des dimensions importantes des marchés basés sur des enchères et est suffisamment général pour représenter la plupart des contextes d'enchères. Nous montrons qu’en enrichissant ADL avec un opérateur de connaissance et une modalité d'action pour caractériser le comportement rationnel limité des enchérisseurs, les agents enchérisseurs peuvent raisonner sur l'effet des actions ainsi que sur la rationalité des autres agents. Dans un second temps, nous proposons une nouvelle approche pour le raisonnement et la conception de nouvelles enchères basée sur des méthodes formelles. Cette approche vise à générer des mécanismes à partir de leurs spécifications et à les vérifier par rapport à des propriétés économiques objectives. Nous proposons une nouvelle variante de Strategy Logic (SL) avec une sémantique quantitative et des opérateurs épistémiques. Nous montrons comment elle permet d'exprimer des concepts essentiels de la théorie de l'économie, notamment l'équilibre de Nash et la manipulation stratégique, qui sont de première importance lors de la conception de nouvelles enchères et lorsque les agents doivent raisonner sur leurs propriétés. Nous introduisons aussi SL avec des stratégies naturelles, qui permet de raisonner sur les mécanismes en fonction de la complexité des stratégies. L'analyse des mécanismes et des stratégies se résume donc à la vérification de formule en SL dans des modèles représentant des enchères. Enfin nous proposons la reformulation du problème de la conception de mécanismes en termes de synthèse de spécifications logiques. Cette approche permet de générer automatiquement des mécanismes optimaux à partir d'une spécification, qui peut inclure non seulement les règles du jeu mais aussi des exigences sur le comportement stratégique des participants.

An auction is a popular mechanism that aggregates participants' bids into a social decision, usually expressed in terms of allocations and payments. Automated agents are widely used in auction-based markets, but they are usually designed to act on a specific context. Those agents cannot switch between different kinds of markets. For doing so, they should be able to ``understand'' the auction rules and reason about their own valuations and about other players’ private information valuations. This limitation inspires the development of a lightweight logic-based language for representing the rules of an auction market, which will then allow automated general players to reason strategically in different environments. Another important problem is the design of new auctions and, more generally, mechanisms. The challenge here is to aggregate individual preferences, while choosing a socially desirable outcome and reaching an equilibrium even though agents can lie about their preferences. Although logic-based languages have been widely considered in the context of Multi-Agent Systems (MAS), the use of formal methods and strategic reasoning for Automated Mechanism Design (AMD) has not been much explored yet. This thesis investigates an application of logics and strategic reasoning for Game Theory and MAS. In particular, we propose the use of formal methods for the specification, design and evaluation of mechanisms, with focus on auctions. This thesis addresses such challenges by introducing logic-based approaches for representing and designing auction-based markets with strategic players. Firstly, for providing a foundation for general and automated auction playing in MAS, we propose a framework for representing auctions, denoted Auction Description Language (ADL). ADL addresses important dimensions of auction-based markets and is general enough to represent most auction settings. We illustrate the generality of ADL by modeling a number of representative auctions. We extend ADL with knowledge operators and an action modality for characterizing bounded rational behavior of bidders when reasoning about the effect of actions and other agents' rationality. Second, we propose a novel approach for reasoning and designing new auctions (and, in general, preference aggregation mechanisms) based on formal methods. Such approach for AMD aims to automatically generate mechanisms from their specifications and verify them in relation to target economical properties. For verifying mechanisms, we propose a new variant of Strategy Logic (SL) with quantitative semantics and epistemic operators. We demonstrate how it can express key concepts from Economic Theory, including Nash equilibrium, strategyproofness and individual rationality, which are at first importance when designing new auctions and when agents need to reason about their properties. We also introduce a quantitative semantics for SL with natural strategies and imperfect information which enables reasoning about mechanisms based on the complexity of strategies. The analysis of mechanisms and their strategies boils-down to model checking formulas from those SL variants. Finally, we offer a novel perspective on the design of mechanisms by rephrasing the AMD problem in terms of synthesis from specifications in Quantitative SL. This approach enables automatically generating optimal mechanisms from a quantitative logical specification, which may include not only game rules but also requirements over the strategic behavior of participants and quality of the outcome.