Computer-aided Verification in Mechanism Design

Abstract : In mechanism design, the gold standard solution concepts are dominant strategy incentive compatibility, and Bayesian incentive compatibility. These simple solution concepts relieve the (possibly unsophisticated) bidders from the need to engage in complicated strategizing. This is a clean story when the mechanism is " obviously " incentive compatible, as with a simple second price auction. However, when the proof of incentive compatibility is complex, unsophisticated agents may strategize in unpredictable ways if they are not convinced of the incentive properties. In practice, this concern may limit the mechanism designer to mechanisms where the incentive properties are obvious to all agents. To alleviate this problem, we propose to use techniques from computer-aided verification to construct formal proofs of incentive properties. Because formal proofs can be automatically checked, agents do not need to manually verify or even understand complicated paper proofs. To confirm the viability of this approach, we present the verification of one sophisticated mechanism: the generic reduction from Bayesian incentive compatible mechanism design to algorithm design given by Hartline, Kleinberg, and Malekian [17]. This mechanism presents new challenges for formal verification, including essential use of randomness from both the execution of the mechanism and from prior type distributions. As a by-product, we also verify the entire family of mechanisms derived via this reduction.
Liste complète des métadonnées

Littérature citée [48 références]  Voir  Masquer  Télécharger

https://hal-mines-paristech.archives-ouvertes.fr/hal-01260071
Contributeur : Claire Medrala <>
Soumis le : jeudi 21 janvier 2016 - 14:44:00
Dernière modification le : lundi 12 novembre 2018 - 11:00:58
Document(s) archivé(s) le : vendredi 11 novembre 2016 - 14:20:15

Fichier

A-636.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, et al.. Computer-aided Verification in Mechanism Design. [Research Report] MINES ParisTech. 2015. ⟨hal-01260071⟩

Partager

Métriques

Consultations de la notice

195

Téléchargements de fichiers

212