Proving incentive (in)compatibility for our auction implementation

[davidrpugh]

The incentive compatibility (or lack thereof) of a particular auction mechanism is a critical property of a particular auction mechanism. Whilst certain classes of mechanisms are provably incentive compatible, in many such cases computing the optimal, incentive compatible allocation is an NP-hard problem. Common "greedy" heuristics that are applied to solve these auction problems in practice often result in allocations that are provably not incentive compatible.

Are there any conditions for which we can guarantee that the approximate result computed using a particular heuristic is incentive compatible? Quoting @bherd-rb from #39 ...

the author of this paper -- are sufficient for truthfulness for both efficient and non-efficient allocations in combinatorial auctions. They might be useful for showing incentive compatibility at some point. The summary below is taken from this report.

• Exactness postulates that a single minded bidder receives exactly the set of goods it
  desires or nothing. In single-item auctions this means that the bidder will get the item it
  bidded for or nothing.
• Participation requests that unsatisfied bidders pay zero and their utility is zero. In other
  words, a non-participating or non-winning bidder neither pays nor receives any money.
• Monotonicity requires that if a bidder increases its bid (decreases in reverse auctions) the
  bidder still wins the auction.
• Criticality claims that each winning bidder pays (receives in reverse auctions) the lowest
  value it could have declared and still be allocated the good it requested.

Formal verification of contracts and algorithms, such as auctions and markets, that process them is of huge practical relevance. The lack of formal verification of contracts developed using Ethereum's Solidity contract language has already led to the theft of millions of dollars and continues to lead to buggy contracts that limit the progress of development of Blockchain-based smart contracting solutions.

@bherd-rb As a long term project goal, could we use formal verification techniques to prove important properties, such as incentive compatibility, of the auction mechanisms that we are developing?

[davidrpugh]

Relevant to actually implementing some kind of formal verification tools on the JVM...

http://babelfish.arc.nasa.gov/trac/jpf/wiki

...unsurprisingly, NASA has developed a formal verification toolkit for the JVM.

[bherd-rb]

@davidrpugh I'm very interested in that! Especially since I'm still collaborating with my former colleagues at King's College in London on the verification of agent-based simulation models (you may remember the Skype presentation that I gave about my research about a year ago).

I think both formal and semi-formal approaches are useful and necessary. Formal verification is definitely crucial in the context of smart contracts. On the other hand, approximate (i.e. simulation-based) verification is great for showing and quantifying the emergence of system-level properties about auctions and marketplaces that are too complex to be analysed formally. The four rules mentioned above seem like a very good starting point. I think they should be expressible in a variant of the temporal-logic specification language that I developed and be answerable using statistical model checking. We could then show that, given a particular simulation model, the auction is incentive-compatible with a certain level of confidence (e.g. 99%) and error rate (e.g. 1%).

Such an approximate verification approach could sit on top of ESL and form part of the overall V&V process. It would be great if we could bring together these two strands of work (ESL and ABM verification).

[davidrpugh]

@bherd-rb I think that we should push on this. Seems to be very interesting research topic as well as a topic that has substantial practically relevance.