We introduce `formal methods' of mechanized reasoning from computer science to address two problems in auction design and practice: is a given auction design soundly specified, possessing its intended properties; and, is the design faithfully implemented when actually run? Failure on either front can be hugely costly in large auctions. In the familiar setting of the combinatorial Vickrey auction, we use a mechanized reasoner, Isabelle, to first ensure that the auction has a set of desired properties (e.g. allocating all items at non-negative prices), and to then generate verified executable code directly from the specified design. Having established the expected results in a known context, we intend next to use formal methods to verify new auction designs.

The performance of a learning classifier system is due to its two main components. First, it evolves new structures by generating new rules in a genetic process; second, it adjusts parameters of existing rules, for example rule prediction and accuracy, in an evaluation step, which is not only important for applying the rules, but also for the genetic process. The two components interleave and in the case of XCS drive the pop-ulation toward a minimal, fit, non-overlapping population. In this work we attempt to gain new insights as to the relative contributions of the two components. We find that the genetic component has an additional role when using the train/test approach which is not present in online learning. We compare XCS to a system in which the rule set is restricted to the initial random population (XCS-NGA, that is, XCS No Genetic Algorithm). For small Boolean functions we can give XCS-NGA all possible rules of a particular condition length. In online learning, XCS-NGA can, given sufficiently many rules, achieve a surprisingly high classification accuracy, comparable to that of XCS. In a train/test approach, however, XCS generalises better than XCS-NGA and there seem to be limitations of XCS-NGA which cannot be overcome simply by increasing the population size. This illustrates that the requirements of a function approximator tend to differ between reinforcement learning (which is typically online) and concept learning (which is typically train/test).