Abstract VCG: Tie-breaking rules in VCG mechanism design
summary
Computer-checked solutions resolve how VCG handles equal bids in sponsored search by parameterizing argmax tie-breaking functions and proving incentive compatibility inside mech.v built on MathComp and the Rocq proof assistant. The work shows the sorting-based implementation used in practice (bubble sort) corresponds to a general VCG with chosen tie-breakers, formalizes winner, price and utility definitions, publishes a GitHub repo Mongi, and provides reusable tactics and mechanized proofs rather than informal arguments.
AI-written summary · about
chapters (7)
- 0:00VCG verification introduction
- 2:09Auction theory motivation
- 4:58Sponsored search auctions
- 7:47General vs sponsored VCG
- 8:54Tie-breaking formalization
- 10:40Key contributions
- 11:22Q&A
related talks
17mSecure Vickrey Auctions for Online Advertising
11mExpanding the VOQC Toolkit
03h 50mSpotlight Talks
13mInteractive Bit Vector Reasoning using Verified Bitblasting
52mGame-Theoretically Secure Protocols Inspired by Blockchains
24mVerifying Almost-Sure Termination for Randomized Distributed Algorithms
24mInformation is the New Money
34mConsensus with Adaptive Adversaries in the Synchronous and Partially Synchronous Models...