A Foundational Framework for the Specification and Verification of Mechanism Design
Résumé
We introduce mech.v, a new framework for the specification and verification of mechanisms, implemented using the Coq interactive theorem prover and the Mathematical Components library. We provide a general definition of mechanism, a subclass capturing auctions, and a few examples of auctions including three notions of Vickrey-Clarke-Groves (VCG), proving their main incentive properties such as truthfulness with reasonable verification effort. We define and prove some more lemmas and definitions usually found in the mechanism design (MD) literature such as Pareto-optimality, rationality, dominance and Nash equilibria. We also define a mechanism refinement system, which we use to relate the implementation of an efficient version of the VCG mechanism for an online advertisement auction to the general VCG specification, allowing us to transfer the truthfulness property from the generic proof. We hope that our library can be useful as a formally verified, unambiguous reference with applications ranging from verification of deployed mechanism to education, and that this is a first step to gather interesting results and definitions from the MD literature to eventually provide a comprehensive mechanically formalized reference.
Origine : Fichiers produits par l'(les) auteur(s)