Olivier Buffet

Chang-Shing Lee

Woan-Tyng Lin

Olivier Teytaud

Optimistic Heuristics for MineSweeper

We present a combination of Upper Confidence Tree (UCT) and domain specific solvers, aimed at improving the behavior of UCT for long term aspects of a problem. Results improve the state of the art, combining top performance on small boards (where UCT is the state of the art) and on big boards (where variants of CSP rule).

Introduction

This sequential decision making research is based on the following requirements on our favorite application:

anytime algorithm (behavior for unknown and possibly small time settings):

we want our algorithm to be able to run in very limited time and provide an approximate solution. For example, Direct Policy Search (DPS) and Upper Confidence Tree (UCT) satisfy this requirement. -asymptotic optimality (behavior for long time settings): many algorithms are fast, but have strong assumptions on the model, so that the real problem is modified in order to match the model requirement; as a consequence, the solution, even if it is optimal on the model, is not optimal on the real problem. For example, UCT satisfies this requirement (in discrete cases, and with some modifications also in continuous domains); many reinforcement learning tools also have this property. DPS, on the other hand, is usually limited by the policy structure. -compatibility with long term effects: many Markov Decision Processes (MDP) have long term effects; you can not make optimal decisions unless you take into account long term consequences of your actions. This requirement is harder to formalize: Direct Policy Search has no problem with this, because it is based on complete simulations of the problem; also, Stochastic Dynamic Programming takes into account long term effects. On the other hand, it is not the case for UCT. Theoretically, UCT will asymptotically find optimal solutions if the horizon is finite; but in real life, only the few initial time steps make sense, the remaining part being left to the pure Monte-Carlo part.

compatibility with high-dimension: many works are dedicated to improving the scalability of MDP-solving algorithms; a great success for this is UCT, with its ability to focus on the relevant parts of the search space.

In this paper, we propose the following principle:

-Using a UCT algorithm for handling the short term combinatorial explosion of the tree of possible futures. -Using, in lieu of the standard pure Monte-Carlo simulator of UCT, a solver known for good performance for long-term behavior.

Section 2 presents some tools useful in the paper. Section 3 presents our algorithm, Optimistic Heuristics. Section 4 presents experimental results. Section 5 concludes.

Tools

In this section, we define the tools on which our algorithm is based: Upper Confidence Trees (Section 2.1), Constraint Satisfaction Problems (Section 2.2).

Upper Confidence Trees

Upper Confidence Trees [START_REF] Kocsis | Bandit based Monte-Carlo planning[END_REF] It is widely reported that choosing a heuristic with high performance does not necessarily lead to high performance of the UCT built on top of it [START_REF] Gelly | Une contribution l'apprendissage par renforcement[END_REF]. However, in the one player case, introducing strong heuristics is seemingly quite efficient [START_REF] Couetoux | Consistent belief state estimation, with application to mines[END_REF][START_REF] Sebag | Combining Myopic Optimization and Tree Search: Application to MineSweeper[END_REF]. This is the principle of [START_REF] Sebag | Combining Myopic Optimization and Tree Search: Application to MineSweeper[END_REF], using a strong heuristic, namely CSP, for improving UCT performance on MineSweeper on small boards.

Constraint Satisfaction Problems + Heuristics

In some problems in which rigorous optimality is unreachable, just optimizing the instantaneous reward might be a good idea. For example, in the MineSweeper problem, choosing the move with lowest probability of immediate loss is efficient. Nonetheless, it is not sufficient for rigorous optimality; as shown by [START_REF] Legendre | Minesweeper: Where to probe?[END_REF], when two locations have the same probability of mine, choosing the one which is as close as possible to the frontier between covered locations and uncovered locations might be a good idea. For examples, if 6 locations a, b, c, d, e, f are uncovered, with probability of mine respectively 50%, 50%, 20%, 20%, 20%, 20%, and distance to the frontier respectively 1, 1, 2, 2, 2, 1, then move (f) should be chosen (at least according to this heuristic), because (i) moves (c), (d), (e) and (f) have lowest probability of mines, and among these locations (f) has smallest distance to frontier. Formally, the frontier is defined as the set of locations which are uncovered and next to at least one mine. This is not formally proved as optimal (and Fig. 2 shows that it is not optimal), but it is on average quite efficient (see results in [START_REF] Legendre | Minesweeper: Where to probe?[END_REF]) as a heuristic for breaking ties between equivalent moves. This heuristic "tie breaking" provides significant improvements. However, as shown by [START_REF] Couetoux | Consistent belief state estimation, with application to mines[END_REF], there are cases where the optimal move is difficult to find among moves with minimum probability of mine. Therefore, CSP variants do not have the asymptotic optimality property discussed in the introduction.

Optimistic Heuristics

We define Optimistic Heuristics (OH), our UCT-based algorithm, as follows:

the main structure of the program is UCT; -we fix the first move at a corner of the board; -we expand only children with minimum probability of mine; -but the Monte-Carlo part is replaced by HCSP (Heuristic CSP), a variant of CSP with improved performance thanks to the heuristic of prefering locations close to the frontier between covered and uncovered locations. [START_REF] Chaslot | Progressive Strategies for Monte-Carlo Tree Search[END_REF]. Before making a decision, the algorithm performs many simulations. Each simulation is typically made of (i) a path in the current tree stored in memory (ii) a construction of one new node added to the tree (iii) a Monte-Carlo simulation from this new node.

The pseudo-code is given in Alg. 2. Describing UCT in details is beyond the scope of this paper; so we refer to http://www.mcts.ai/?q=mcts for a userfriendly introduction. Figure 1 provides a graphical overview.

Experiments

Fig. 2. Situations in which some moves with minimum probability of mine are suboptimal. We are not aware of situations where no move with minimum probability of mine is optimal; so in our program we expand only the parts of the tree corresponding to moves with lowest probability of mine (yet, we have no proof of optimality for this). Top: the top location and the bottom covered locations lead to a probability of winning 2 3 , whereas the middle location leads to a probability of winning 1 3 . Bottom: these three boards are the three possible cases when playing 5x5 GnoMine with 15 mines (up to rotation): they show that under GnoMine rule, playing in the center (for the first move) leads to a 100% winning rate. One can easily see that the success rate when playing any other move is < 100%. So, this case shows that even for the first move, choosing a move with minimal probability of mine is not enough for playing optimally; moreover, corners are not optimal for the GnoMine variant.

The well known MineSweeper game is much more complex than expected at first sight [START_REF] Kaye | Minesweeper is np-complete[END_REF][START_REF] Ben-Ari | Minesweeper as an np-complete problem[END_REF][START_REF] Nakov | Minesweeper, #minesweeper[END_REF], and a good tool for modeling in a clean way some real world problems [START_REF] Hein | Minesweeper for sensor networks-making event detection in sensor networks dependable[END_REF]. The most classical approach for MineSweeper is based on Constraint Satisfaction Problems [START_REF] Studholme | Minesweeper as a constraint satisfaction problem[END_REF], as in Section 2.2: this provides a provably correct estimate of the belief state, and then classically after CSP one plays the covered location with least probability of being a mine. However, [START_REF] Couetoux | Consistent belief state estimation, with application to mines[END_REF] has shown that this approach is suboptimal; there are situations, as in Fig. 2, where some moves with minimum probability of mines are nonetheless suboptimal moves. This fact was used in [START_REF] Legendre | Minesweeper: Where to probe?[END_REF] for designing a version of CSP with better performance, by preferring the locations which are closest to the frontier in case of tie on the probability of mines; [START_REF] Legendre | Minesweeper: Where to probe?[END_REF] got the best performance so far on MineSweeper on many board sizes, under time constraints, in particular big boards.

An alternate approach has been investigated in [START_REF] Couetoux | Consistent belief state estimation, with application to mines[END_REF][START_REF] Sebag | Combining Myopic Optimization and Tree Search: Application to MineSweeper[END_REF]; using UCT, these approaches have asymptotic optimality, and so outperform CSP when given enough time. They got best performance so far on small boards, outperforming CSP, but are too slow for big boards.

[13] and [START_REF] Legendre | Minesweeper: Where to probe?[END_REF] outperformed the state of the art in two different settings; close to optimality on small boards for [START_REF] Sebag | Combining Myopic Optimization and Tree Search: Application to MineSweeper[END_REF] (compliant with any variant of rule), and better than CSP on big boards for [START_REF] Legendre | Minesweeper: Where to probe?[END_REF]; in this paper we combine both approaches, using UCT with the HCSP approach as a heuristic.

MineSweeper is parametrized by the number of mines, the number of rows, the number of columns. Importantly, there are different variants of MineSweeper:

variants in which the mines can be anywhere on the board; -variants in which the mines can not be on the first move (as in most implementations); -variants in which there are no mine in the neighborhood of the first move (e.g. the GnoMine implementation).

The optimal strategies are the same for the first two variants. It is widely believed that moves in the corners are optimal in the two first cases; but, as shown by the example in Fig. 2 (right) this is not the case for the third family of variants.

For the sake of sound comparisons with earlier results, we will present results in the second case, i.e. one can not lose at the first move.

Results are presented in Table 1.

Conclusions

We experimented a combination between UCT and CSP solvers. We got a reasonably fast solver, much faster than the one from [START_REF] Sebag | Combining Myopic Optimization and Tree Search: Application to MineSweeper[END_REF], and benefiting from the heuristic from [START_REF] Legendre | Minesweeper: Where to probe?[END_REF]. Results are at the state of the art on all board sizes. Further work consists in -Pairing simulations: using the same sequence of possible children for all children of a given node. -Using the additional information from HCSP for ordering legal decisions in a given node; for example, we might:

• consider moves in lexicographic orders on x-axis and y-axis;

• consider moves in order of probability of mine, and in case of tie distance to the frontier (this is inspired by [START_REF] Legendre | Minesweeper: Where to probe?[END_REF]); • consider random order (which avoids biases).

-Using progressive widening [START_REF] Chaslot | Progressive Strategies for Monte-Carlo Tree Search[END_REF]4,[START_REF] Lee | The Computational Intelligence of MoGo Revealed in Taiwan's Computer Go Tournaments[END_REF]; testing various coefficients, and maybe non-polynomial rules; or use rules depending on rewards obtained for the already sampled moves; see Fig. 3 for more on this. CSP-PGMS is the PGMS implementation of CSP (http://www.ccs.neu.edu/home/ramsdell/pgms/). HCSP is the implementation of CSP with heuristic breaking ties by playing as close as possible to the frontier between covered locations and uncovered locations [START_REF] Legendre | Minesweeper: Where to probe?[END_REF]; results are averaged over 10 5 games except 16x30 which is averaged over 10 4 games. BSSUCT is the implementation of UCT from [START_REF] Sebag | Combining Myopic Optimization and Tree Search: Application to MineSweeper[END_REF]. OH is our Optimistic Heuristics program. For OH, results are obtained with 10000 simulations per move, except expert mode and intermediate mode (99 mines on 16x30 and 40 mines on 16x16) which use 100 simulations per move. BSSUCT is not documented for cases in which it was too slow for being operational in [START_REF] Sebag | Combining Myopic Optimization and Tree Search: Application to MineSweeper[END_REF].

-Simulate several times for evaluating a node, before starting new simulations from the root. -Using rapid action value estimates [START_REF] Gelly | Combining online and offline knowledge in UCT[END_REF] (either it brings an improvement, or it is an interesting counter-example; see Fig. 4 for a counter-example in the game of Go.).

More specifically for Minesweeper, we don't know if the assumption that the optimal move has minimum probability of mine is safe. We just break ties between various moves with minimum probability of mine, and we did not find any proof that doing otherwise (i.e. considering also moves with non minimal probability of mine) can bring an improvement; but we have no proof. Also we have no proof that always playing in the corner for the first move is a good idea; it is known as a good heuristic, but maybe in some cases there are better moves (with the rule "first move is a 0", it is mathematically proved that the center is a good move in some cases; see [START_REF] Couetoux | Consistent belief state estimation, with application to mines[END_REF]). There are infinitely many possible decisions. Without progressive widening, all moves are tested just once, and the final arm is chosen randomly, whereas a progressive widening as in [START_REF] Wang | Algorithms for infinitely many-armed bandits[END_REF] is mathematically consistent.

Fig. 1 .

 1 Fig. 1. A description of MCTS in one Figure, from[START_REF] Chaslot | Progressive Strategies for Monte-Carlo Tree Search[END_REF]. Before making a decision, the algorithm performs many simulations. Each simulation is typically made of (i) a path in the current tree stored in memory (ii) a construction of one new node added to the tree (iii) a Monte-Carlo simulation from this new node.

Fig. 3 .

 3 Fig. 3. Example in which progressive widening is necessary; each decision leads to a reward which is a Bernoulli random variable with parameter p, uniformly drawn in [0, 1]. There are infinitely many possible decisions. Without progressive widening, all moves are tested just once, and the final arm is chosen randomly, whereas a progressive widening as in[START_REF] Wang | Algorithms for infinitely many-armed bandits[END_REF] is mathematically consistent.

  proceeds as explained in Alg. 1 for making a decision in a state s in time t.

	This algorithm uses the two following formulas:
	Q(s, d) = mean reward of past simulations including decision d in state s
	Q ucb (s, d) = Q(s, d) +	log(2 + n(s)) 1 + n(s, d)
	where n(s, d) is the number of simulations with move d in state s and n(s) =
	d n(s, d).
	Algorithm 1 The UCT algorithm in short.
	Inputs: a state s, a time t.
	Output: a decision.
	while t is not elapsed do
	s ′ = s	// initialization of a simulation
	while s ′ is not a final state	// this loop is a simulation do
	if s ′ has more than 5 simulations then
	Let d be the decision in s' which maximizes Q ucb (s ′ , d)
	else
	Let d be a decision in s' chosen by a heuristic (a.k.a Monte-Carlo part)
	end if
	Let s ′′ be a (possibly stochastic) next state obtained after decision d in s ′ .
	s ′ ← s ′′
	end while
	Update Q ucb values and Q values
	end while
	Return the decision in s ′ with maximum Q(s ′ , d).

  Algorithm 2 Our Optimistic Heuristics algorithm. The two parts in bold involve specialized methods, namely CSP and HCSP. Output: a decision. while t is not elapsed do s ′ = s // initialization of a simulation while s ′ is not a final state // this loop is a simulation do CSP: Let E be the set of moves with minimum probability of mine. if s ′ has more than 5 simulations then Let d be the decision in E which maximizes Q ucb (s ′ , d) else Let d be a decision in E chosen by HCSP. end if Let s ′′ be a (possibly stochastic) next state obtained after decision d in s ′ . s ′ ← s ′′ end while Update Q ucb values and Q values end while Return the decision in s ′ with maximum Q(s ′ , d).

Inputs: a state s, a time t.

Table 1 .

 1 Results of various implementations on the MineSweeper games.

	Format	CSP-PGMS	HCSP	BSSUCT	OH
	4 mines on 4x4	64.7 %	67.0%	70.0% ± 0.9%	67.0% ± 0.5%
	1 mine on 1x3	100 %		100%	100%
	3 mines on 2x5	22.6%	21.0%	25.4%± 1%	23.4% ± 0.5 %
	10 mines on 5x5	8.20%	8.51%	9% (p-value: 0.14)	11.4% ± 0.4 %
	5 mines on 1x10	12.93%	12.7%	18.9% ± 0.2%	17.0% ± 0.4 %
	10 mines on 3x7	4.50%	4.76%	5.96% ± 0.16%	6.1% ± 0.2 %
	15 mines on 5x5	0.63%	0.63%	0.9% ± 0.1%	1.15% ± 0.1 %
	10 mines on 8x8		79.9 %		80.2 ± 0.48
	10 mines on 9x9	80%	90.5%		89.9% ± 0.3%
	40 mines on 16x16	45%	76.4% ± 0.4%		74.4% ± 0.5%
					(100 sims per move)
	99 mines on 16x30	34%	38.1% ± 0.5%		38.7 ± 1.8 %
					(100 sims per move)

Acknowledgements

The authors are grateful to NSC for funding NSC100-2811-E-024-001, to ANR for funding COSINUS program (project EXPLO-RA ANR-08-COSI-004), to the authors of PGMS and PGMS-CSP for making their implementations freely available. We are also grateful to the MASH European project (program FP7) and the the IOMCA (ANR) project.


Dominique Guegan
email: dguegan@univ-paris1.fr

Bertrand K Hassani
email: bertrand.hassani@malix.univ-paris1.fr

Cédric Naud
email: cedric.naud@aon.fr

Dominique Guégan

An efficient threshold choice for operational risk capital computation

Keywords:

Operational risk quantification requires dealing with data sets which often present extreme values which have a tremendous impact on capital computations (VaR). In order to take into account these effects we use extreme value distributions, and propose a two pattern model to characterize loss distribution functions associated to operational risks: a lognormal on the corpus of the severity distribution and a Generalized Pareto Distribution on the right tail. The threshold from which the model switches form a scheme to the other one is obtained using a bootstrap method. We use an extension of the Peak-over-threshold method to fit the GPD and the EM algorithm to estimate the lognormal distribution parameters. Through the VaR, we show the impact of the GPD estimation procedure on the capital requirements.

Besides, our work points out the importance of the building's choice of the information set by practitioners to compute capital requirements and we exhibit some incoherences with the actual rules. Particularly, we highlight a problem arising from the granularity which has recently been mentioned by the Basel Committee for Banking Supervision.

Introduction

The purpose of this paper is operational risks quantification following the Basel Advanced Measurement Approach (AMA) [START_REF] Bis | International convergence of capital measurement and capital standards[END_REF]). This proposal of the Basel committee binds banks to carry out their own models on internal data sets to evaluate amounts of capital necessary to face these risks.

In this paper, we focus on the computation of the loss distribution function (LDF) [START_REF] Frachot | Loss distribution approach for operational risk[END_REF], [START_REF] Guégan | A modified panjer algorithm for operational risk capital computation[END_REF]) which is currently used to evaluate this kind of risks [START_REF] Cruz | Operational Risk Modelling and Analysis[END_REF], [START_REF] Chernobai | Operational Risk: A Guide to Basel II Capital Requirements, Models, and Analysis[END_REF] and [START_REF] Shevchenko | Modelling Operational Risk Using Bayesian Inference[END_REF]). We compute it as a convolution of two distribution functions, one modeling the frequencies of the losses and the other one their severity. Following the literature, we restrict to a Poisson distribution for the frequencies, and in this paper we focus on the estimation of the severity distribution.

The objective of the paper is to model the severities using a class of distributions which take into account the large losses: the Generalized Pareto Distribution (GPD). In order to capture extreme values on the first hand, and on the other hand the multimodality observed in operational risk data sets1 , we propose to model the severities as a mix of two distributions: one characterizing the most important losses denoted cauda using the GPD [START_REF] Pickands | Statistical inference using extreme order statistics[END_REF], [START_REF] Davis | Tail estimates motivated by extreme value theory[END_REF] and [START_REF] Embrechts | Modelling Extremal Events: for Insurance and Finance[END_REF]), and another one on the remaining data corresponding to the central part of the distribution or corpus. A characteristic of the GPD stands in the determination of a threshold denoted u permitting to define the data set on which the distribution will be adjusted. Therefore, the estimation of this threshold is the core of this paper: we highlight the influence of the choice of the threshold on the computation of the capital requirement. Then, once the threshold has been identified we need to estimate the parameters of the two distributions, for instance the lognormal and the GPD. Using several estimation methods, we also exhibit the influence of these ones on the computation of univariate capital requirement.

Finally, considering the obtained results, we discuss the problem of granularity which is the main problem in the construction of operational risk data sets (or Basel matrix).

The paper is organized as follows: Section two introduces the data set, Section three presents the theoretical framework, Section four describes the estimation of the threshold and the construction of the LDF and Section five is devoted to capital charge estimations. A sixth Section concludes.

The Data Set

The data set we use is organized into the Basel Matrix (BIS ( 2001)). In its first level of granularity, this matrix is made up of 56 cases -8 business lines ("b") × 7 event types ("e")2 . Nevertheless, each event type might be decomposed in several elements. For example, the "external fraud" event may be shared in two items -"Theft and Fraud" and "Systems Security" (second level of granularity). In a third level, the element "Theft and Fraud" may be split in several components: "Theft/Robbery", "Forgery" and "Check kiting". After a deep analysis, we observe that the kind of losses expected from a fraud with a credit card does not correspond to losses caused by someone hacking the system for instance; nevertheless they are in the same cell. Therefore, considering the largest level of granularity, we could face multimodal empirical distributions.

Consequently, the methods used to model the losses depend on the granularity level choice. This choice might have a tremendous impact on capital requirement computations. Besides, we face a trade-off between quantity of data and robustness of the estimations: indeed, if the quantity of data is not sufficient, we cannot go lower in the granularity; on the another hand the ensuing empirical distribution is therefore an aggregate of various natures of data and the estimation of this last empirical distribution can be source of unusable or unrealistic results.

The previous paragraph dealt with the multimodality and the granularity problems. These points have a corollary: an extreme value is a relative concept, which require a referent. For example, a card fraud of 50000e is an extreme value compared to an average loss of 300e while a rogue trading of 50000e is not an extreme value when we know that the average loss represents several millions. Furthermore, we do not define an extreme value as an "extremely" rare event.

Therefore, one can use a GPD approach as the one presented below to model the severities.

The theoretical framework

The Loss Distribution Function (LDF) G (whose density is denoted g) is a mixture of two distributions, the frequency distribution p and the severity distribution F (whose density is f ):

G = ∞ γ=0 p(γ)F * γ (x; θ), x > 0, G = 0, x = 0, (3.1)
where * γ is the γ-order operator of convolution, θ a vector of parameters. The density is given by,

g = ∞ γ=0 p(γ)f ⊗γ (x; θ), x > 0. (3.2)
The severity distribution, on which we focus in the current paper, is defined as a mixture of a lognormal distribution on the corpus, and a GPD on the right tail (cauda). The GPD density is:

f GP D (x; u, β, ξ)) =      1 β 1 + ξ x-u β -1-( 1 ξ ) , if x ≥ u, 1 + ξ (x-u) β > 0, β > 0 1 β 1 -x-u β , if x ≥ u, ξ = 0 , ( 3.3)
where u ∈ R * + is the threshold, β ∈ R * is the scale parameter and ξ ∈ R the shape parameter.

Therefore, the severity density in our model is as follows:

f (x; u, β, ξ, µ, σ) =      f (corpus) (x; µ, σ), if x < u f (cauda) = 1 1- u 0 f (corpus) (x;µ,σ)dx × f GP D (x; u, β, ξ)), if x ≥ u , (3.4)
where, µ and σ are the lognormal distribution parameters, and f GP D is the density introduced in (3.3).

Remark 3.1. Modeling both the losses below and above the threshold has two major advantages:

• It enables specifying the threshold regarding a model, i.e. the quantile obtained empirically is different from the quantile we have theoretically.

• It permits creating a whole distribution we will be able to use in a multivariate approach [START_REF] Guégan | n-dimensional copula contributions to multivariate operational risk capital computations[END_REF]).

In order to estimate the parameters of the distribution (3.4), we need first to estimate the threshold u. To do so, we carry out a bootstrap method [START_REF] Hall | Using the bootstrap to estimate mean squared error and select smoothing parameter in nonparametric problems[END_REF], [START_REF] Danielsson | Using a bootstrap method to choose the sample fraction in tail index estimation[END_REF] for which we give practical solutions in the next Section. Once u has been found, ξ and β have to be estimated, therefore we implement a method based on the Anderson-Darling statistics [START_REF] Luceno | Fitting the generalized pareto distribution to data using maximum goodnessof-fit estimators[END_REF]). This method maximizes the following relationship to estimate the parameters:

A 2 n = n ∞ -∞ (F (GP D) (x; u, β, ξ) -S n (x)) 2 F (x; u, β, ξ)(1 -F (GP D) (x; u, β, ξ))) dF (GP D) (x; u, β, ξ), (3.5)
where, F (GP D) (x; u, β, ξ) is the cumulative distribution function of a GPD whose density is

given by (3.3), and n ∈ R + the number of observations. In the fifth Section, we compare this method with other traditional estimators and we show that this approach provides interesting results. Then, as we assumed a lognormal distribution to model the central part of the severity distribution (3.4), we implement an Expectation-Maximization algorithm [START_REF] Dempster | Maximum likelihood from incomplete data via the em algorithm[END_REF], [START_REF] Mclachlan | The EM algorithm and extensions[END_REF]) to estimate the parameters of the truncated distribution. Finally, the λ parameter of the Poisson distribution p(γ; λ) is estimated using maximum likelihood method. As soon as we have estimated the whole set of parameters, we can build the loss distribution function (3.1) using a convolution method based on the modified Monte Carlo Algorithm given in Appendix B [START_REF] Fishman | Monte Carlo[END_REF], [START_REF] Cruz | Modeling, measuring and hedging operational risk[END_REF], [START_REF] Peters | Simulation of the annual loss distribution in operational risk via panjer recursions and volterra integral equations for value at risk and expected shortfall estimation[END_REF] and Shevchenko ( 2010)), and compute a VaR [START_REF] Riskmetrics | Var[END_REF], [START_REF] Artzner | Coherent measures of risk[END_REF]),

V aR (1-α)% = inf(x ∈ R : P (X > x) ≤ (1 -α)), (3.6)
where, X is a random variable characterized by the previous LDF, and α = 0.1.

The Figure 1 illustrates the method introduced in this section through a simulation experiment.

We Remark 3.2. Drawing a parallel between this two-behavior approach with other methods such as using g-and-h distributions [START_REF] Peters | Bayesian inference, monte carlo sampling and operational risk[END_REF], [START_REF] Dutta | A tale of tails: an empirical analysis of loss distribution models for estimating operational risk capital[END_REF] 4 Discussion around the threshold "u" of the GPD

In this section, we focus on the way to determine an efficient threshold u consistent with the specific data set we work with, that is to say operational risks losses. In order to solve this problem, we assume that we observe a data set X = (X 1 , ..., X n ), and we denote X = (X (1) , ..., X (n) )

its order statistics, We first estimate the parameter ξ of the GPD (3.3) with the whole sample using the traditional Hill estimator [START_REF] Hill | A simple general approach to inference about the tail of a distribution[END_REF]):

ξn (k) = 1 k k i=1 log X (n-i+1) -log X (n-k) , (4.1)
k being the number of losses above the threshold. Thus, by the way we introduce a direct relationship between k and u. Indeed, once we have k we have the threshold and vice versa.

We first determine k using the Hill estimate (4.1) and then implement a bootstrap method to obtain u. The different steps are the following:

1. We plot ξn (k) with respect to k, as in Figure 2.

2. As soon as we detect a change in the plot pattern ("break"3 ) as in Figure 2 we build an information subset X 1 (size n 1 ) containing this break and the values above it. For example, in Figure 2 we heuristically determine a break at the value 100 e which corresponds to the initial value of the subsample. Using the values in X 1 we determine the parameter k 1 minimizing the following criterion: 3. In the relation (4.2), the parameter ξ is unknown and we estimate it bootstrapping ξn 1 (k 1 ) as follows. From the set previous X 1 , we draw J (J ∈ N) subsamples with replacement of size n 2 (n 2 < n 1 ), (X

AM SE(k 1 ) := E( ξn 1 (k 1 ) -ξ)
(j) 1 , ..., X (j)
n 2 ), j = 1, ..., J. Their corresponding order statistics are (X

(1) , ..., X

(n 2 ) ) and the corresponding bootstrapped Hill estimate of ξn 1 (k 1 ) from X 1 is equal to,

ξn 2 (k 2 ) = 1 k 2 k 2 i=1 log X (n 2 -i+1) -log X (n 2 -k 2 ) , k 2 = 1, ..., n 2 , (4.3)
where

X l = 1 J J j=1 X (j) (l) , l = 1, ..., n 2 . (4.4)
4. Now, replacing ξ by ξn 2 (k 2 ) in (4.2), we minimize the following criterion with respect to

k 2 . AM SE(k 2 ) := E( ξn 1 (k 1 ) -ξn 2 (k 2 )) 2 .
(4.5) 5. Then, given (k 1 , k 2 ), and following [START_REF] Hall | On some simple estimates of an exponent of regular variation[END_REF][START_REF] Hall | Using the bootstrap to estimate mean squared error and select smoothing parameter in nonparametric problems[END_REF] we estimate 4 the threshold u by,

u = k 2 * n 1 n 2 2 3 . (4.6)
In order to implement the previous methodology, we need to pay attention to the following points:

1. If an obvious pattern change (from erratic to linear for example) is observed in the representation of ξn (k) with respect to k (Step 1), we can directly read u on the graph.

2. In the step 4, k 1 is fixed. In practice, we can hesitate between several k 1 -values, denoted

k 1 1 , ..., k Λ 1 , Λ ∈ N, which means that for each k (j) 1 , j = 1, ..., Λ, we obtain a k 2 -value de- noted k (j) 2 . For each couple (k (j) 1 , k (j)
2 ), we choose the k (j) 2 -value, for which the relationship (4.5) is the "'most stable"', and therefore, we compute the criteria (4.5) for d successive values of k 2 taken around k (j) 2 . In that case the parameter k 2 is obtained minimizing:

φ(k (j) 2 , d) = d i=1 M (j) 1 -M * (j) i 2 , j = 1, ..., Λ, (4.7)
where, M

(j) 1 ≡ AM SE(k (j)
2 ) is obtained from (4.5) for each k

(j)
2 , and M * (j) i is computed using the i value around k (j)

2 , i = 1, ..., d. 4 We are only working on a part of the initial sample, it is necessary to adjust k2 to the whole data set. 3. If we cannot interpret the Hill plot (Step 1), either because the data set is too unstable or too stable, we cannot use the previous algorithm, therefore, we use the whole information set X, and follow the method developed in [START_REF] Danielsson | Using a bootstrap method to choose the sample fraction in tail index estimation[END_REF] to estimate the ξ parameter (this method does not require an a priori value of the threshold). We estimate ξ by:

ξn (k) = 1 k k i=1 (log X (n-i+1) -log X (n-k) ) 2 2 ξn (k) . (4.8)
For a certain 5 n 2 , we bootstrap ξn (k) which appears in relationship (4.8) following the step 3 of the previous algorithm to create ξn 2 (k 2 ), where the parameter k 2 is obtained minimizing,

AM SE(k 2 ) := E( ξn 2 (k 2 ) -ξn 2 (k 2 )) 2 .
(4.9)

Then for a given k 2 , u is equal to:

u = (k 2 ) 2 k 3 (log k 2 ) 2 (2 log n 2 -log k 2 ) 2 log n 2 -log k 2 log n 2 , (4.10)
where k 3 is obtained exactly as k 2 with n 3 = n 2 2 n .

4. [START_REF] Shevchenko | Modeling operational risk data reported above a timevarying threshold[END_REF] suggest the use of a time varying threshold. In the current paper, we use a static methodology, nevertheless it would be interesting to dynamics in the process of estimation. To do so, a possibility would be to use the dynamics of the severity data set given for instance by the incidents' amounts and their occurrence dates. In that case, the results would take into account the behavior changes in the risk faced through time and adjust with the state of nature they are currently in (crises, boom etc.).6

Capital Requirement

We applied the previous methodology to real operational risks data. We use two data sets denoted X (1) and X (2) .

• The set X (1) represents the severity of the business line "Retail Banking" and the event type "Business Disruption & System Failure and Execution" for the year 2007.

• The set X (2) represents the severity of the business line "Payment & Settlement" and the event type "Delivery, Execution and Process Management" for the year 2006.

Their statistics are given in Table 1. We deduce that their corresponding empirical severity distributions are asymmetric (right skewed) and leptokurtic. This statement strengthens our decision to implement a method which cares about extreme values in the distributions.

We provide in Table 2 the estimations of GPDs parameters (with their standard deviation in brackets) obtained for both sets, using these four methods. Then we estimate the parameters of the lognormal distributions for the sets X (1) -X (GP D 1 ) and X (2) X (GP D 2 ) and the results are provided in Table 3. 2: Estimations of the GPD's parameters ξ and β given in (3.3), using four methods respectively for u (1) = 1645.07 and u (2) = 179. We provide in brackets the standard deviations computed by bootstrapping.

Method

X (1) -X (GP D 1 ) X (2) -X (GP D 2 ) µ = 5.702144 σ = 1.103373 µ = 3.593098 σ = 1.510882 (0.07134) (0.03016) (0.04112) (0.02576)
Table 3: Estimations of the parameters of the lognormal distributions fitted on the data sets X (1) -X (GP D 1 ) and X (2) -X (GP D 2 ) . Standard deviation are provided in brackets.

As soon as all the parameters have been estimated, we implement a Monte Carlo algorithm with a million of iterations to build G, and we use it to compute a 99.9% VaR which provides the required amount of capital. Table 4 provides the VaRs of the set X (2) using the four estimation methods to estimate the threshold. We observe miscellanous amounts, varying from 5 725 341 euros to 538 480 990 euros. This last result is obtained from a distribution whose mean is infinite (the parameter ξ is greater than 1). This result points that the choice of the distribution and the estimation procedure are crucial for the VaR computations. The M1 method has the advantage to maximize the goodness-of-fit of the GPD and insures that the distribution cannot be statistically rejected. Therefore, one can argue that the VaR at 15 700 112 euros be a reasonnable value considering the information set we have, and the assumptions done.

We do not provide the VaRs for the set X (1) as the results we obtained imply a simulated VaR multiplied by more than one hundred compared to the historical one. Here again, we can observe that the underlying model has an infinite mean.

Analyzing the results and controlling every step of the method, we concluded that the difficulty to obtain a "correct" and a "robust" model comes from the structure of the data set. Considering that different kinds of data are mixed in a single set it appears difficult to fit an accurate distribution on the severities. In order to analyze the impact of the granularity strategy, it would be interesting to split the data in multiple subsets whether the information sets sizes are large enough. In that latter case the computed VaRs would reflect risks created by specific kinds of risk, and finally aggregating them we could compare the results to the largest level of granularity. 4: VaR estimations for u = 179, µ = 5.681191 and σ = 1.081609 for the data set X (2) .

Estimations have a tremendous impact on the VaRs. In this table, these ones may differ by 9405%.

Finally we want to notice the influence of the threshold on the estimation of the GPD's parameters β and ξ. This effect is due to the fact that the information set changed. We illustrate this point providing estimates for five threshold values, for the set X (1) ( thresholds u for the data set X (2) . Parameters are very sensitive to the threshold value.

Conclusion

In this paper, we focus on the estimation of the LDF used to estimate operational risks. We highlight that the VaR computation depends on the method implemented. Therefore, a sharp analysis of the LDF is essential, and even if the LDF is a convolution of two distinct distributions, the capital requirements seem particularly sensitive to the choice and the estimation of the severity distribution. We present a new method to compute the severity distribution, splitting it in two parts in order to better take into account the large losses. We use a GPD on the right tail for which we provide innovative theoretical and practical solutions, and fit a lognormal distribution on the remaining data. Then, to build the final LDF, we apply a new adapted Monte Carlo algorithm. This method enables capturing at least two distinct behaviors in a severity distribution, and sometimes a bit more if the multimodality is not too strongly marked.

We point out the importance of the Basel matrix construction and the so-called granularity effect.

Second, we underline the fact that once the threshold of the GPD has been found, the method chosen to estimate GPD's parameters tremendously impacts the VaR: it seems that this fact has never been discussed before.

In our applications, we have been confronted to an important problem arising from the data bases construction. Following the regulator, who demands to take into account the right tail of the severity distribution to estimate the LDF, we sometimes obtained unrealistic VaRs (i.e.

equal to half the bank capitalization) due to infinite mean models. On the other hand, if we do not care about the severity tail, we have negligible VaRs. Then, even if it seems reasonable to follow regulator requirements, we point out two important facts: either the Bank are overexposed to these risks or the data sets are badly built. We privilege the last point and ask operational risks managers to pay attention to the large diversity of data origins. The correct question is to propose another way for building the data sets used to compute operational risks taking into account the difference which exists inside the different risk categories. It seems that it has no sense to mix some risks together. In our knowledge, this problem has not yet been discussed and the regulators need to reexamine risk typology and data sets granularity on which are computed operational risk capital requirements.

  exhibit the histogram of the Historical LDF. The black line corresponds to a LDF mixing a Poisson distribution and a lognormal severity. The associated 99.9% VaR is pointed out by ∆. The dashed line represents a LDF mixing a Poisson distribution and a multiple pattern severity distribution (lognormal-GPD given by (3.4)) using the Monte Carlo algorithm described in Appendix B. The corresponding VaR is represented by a +. The right graph focuses on the right tail of the LDFs described in this paragraph. This figure highlights the fact that this method enables thickening up the right tail of the LDF.

Figure 1 :

 1 Figure 1: Method Illustration: This figure presents the histogram (in grey) of the Historical LDF. The black line corresponds to a LDF mixing a Poisson distribution and a lognormal severity. The associated 99.9% VaR is pointed out by ∆. The dashed line represents a LDF mixing a Poisson distribution and a multiple pattern severity (lognormal-GPD given by (3.4)) using the algorithm discribed in Appendix B. The corresponding VaR is represented by a +. The right graph focuses on the right tail of the LDFs described above. This figure highlights the fact that this method enables thickening up the right tail of the LDF.

9Figure 2 :

 2 Figure 2: Using the 610 highest values of the Basel case (Retail Banking; Damage to Physical Assets) of 2007, we represent the Hill estimates considering thresholds varying between 39.2 and 7000 e. The graph becomes roughly stable around the value 180, but even if we are able to identify the zone in which the threshold would stand, we have not yet an exact value, thus to estimate u, we define the set X 1 from the value 100 e, thus X 1 contains 290 data.(Upper and lower dashed lines represents a 95% confidence interval.)

13

  Documents de Travail du Centre d'Economie de la Sorbonne -2010.96 ( Version révisée)

  (2007)), we conclude that it does not exist a method which supplant the others. Trying the gand-h distribution to model some of our data sets, we had most of the time bad fitting results

	or unrealistic capital charges, nevertheless in some particular cases the flexibility offered by this
	distribution could be a reliable solution to model multimodal severity distributions. The method
	presented in this paper, especially when we have enough data above the threshold and as soon as
	the goodness-of-fit test validates the distribution, may be a powerful alternative.

and Degan et al. 6 Documents de Travail du Centre d'Economie de la Sorbonne -2010.96 ( Version révisée)

Table 5 :

 5 Table5). All the estimated values are relevant despite a great instability. Thus the corresponding VaR and capital amount would be different. All steps of the previous methodology: estimation of u, estimation of the parameters ξ and β, methods of estimation play an important role in the computation of the This table presents GPD's parameters estimates and their standard errors for different

	capital requirement.
	Threshold u	β	Standard error β	ξ	Standard error ξ
	1162.12	1110.8538	87.77	0.6026	0.06877
	1608.27	946.6787	94.68	0.7924	0.09329
	1645.07	904.087	92.31	0.827	0.09713
	2021.48	1188.2956	155.48	0.9149	0.1397
	2177.58	1385.5295	199.56	0.8879	0.14

We used data from BPCE on the French Caisse d'Epargne perimeter.

Documents de Travail du Centre d'Economie de la Sorbonne -2010.96 ( Version révisée)

The business lines are corporate finance, trading & sales, retail banking, commercial banking, payment and settlement, agency services, asset management and retail brokerage. The event types are internal fraud, external fraud, employment practices & workplace safety, clients, products & business practices, damage to physical assets, business disruption & system failures and execution, delivery & process management.

The break is determined empirically by finding a change in the slop.

A short algorithm providing the optimal n2 is given in[START_REF] Danielsson | Using a bootstrap method to choose the sample fraction in tail index estimation[END_REF]. 10 Documents de Travail du Centre d'Economie de la Sorbonne -2010.96 ( Version révisée)

Nevertheless in the current paper, this methodology cannot be considered because we do not have the corresponding information set. Besides, in[START_REF] Guégan | A mathematical resurgence of risk management: an extreme modeling of expert opinions[END_REF] we dealt with a dynamic threshold using a extreme distribution[START_REF] Fisher | Limiting forms of frequency distributions of the largest or smallest member of a sample[END_REF]) with another data set.

We do not provide those results as we did not have the corresponding data sets.

 1: First four moments of the two data sets X (1) and X (2) . The third order empirical moment is non null and the fourth order moment is far from 3.

In order to calibrate the appropriate loss distribution function on each data set, we use a Poisson distribution to model the frequency data. In the current paper, we did not challenge the choice of a Poisson distribution to model the frequency as the gain obtained from a continuous approximation or the use of another theoretical distribution has almost negligible impact on capital computation. Therefore, estimating the λ parameters of the Poisson distribution by maximum likelihood method, we get λ (1) = 2653 and λ (2) = 1292 respectively on the sets X (1) and X (2) .

To fit the severities, we tried several usual distributions suggested in the literature, but the Kolmogorov-Smirnov test rejected all (Table 6). Therefore, we continue our exercise and focus on the estimation of the threshold. To estimate the threshold u of the GPDs in the relation (3.4), we define two new sets X

(1) 1

an X

(2)

1 , following the notations introduced in the previous section. Their sizes are respectively n (2) 2 = 97. The resulting thresholds are u (1) = 1645.07 and u (2) = 179. They imply respectively 191 and 315 data above these thresholds.

We denote X (GP D 1 ) and X (GP D 2 ) the two corresponding data sets on which we fit the GPDs.

We estimate the parameters ξ and β of the GPDs defined in (3.4) using the method introduced by (Luceno ( 2006)) given in (3.5), denoting this method M1. We also consider three other alternative estimation methods to estimate these parameters in order to check their impact on VaR computations. These ones are respectively the Pickands method (M2) [START_REF] Pickands | Statistical inference using extreme order statistics[END_REF]), the Hill method (M3) [START_REF] Hill | A simple general approach to inference about the tail of a distribution[END_REF]), and the Maximum Likelihood method (M4).

The method we provide enables to compute capital requirements with respect to Basel accords, so, we strictly stick to them. In this paper we focused on the effectiveness of the proposed method on an operational standpoint, however, other research tracks can extend the results developed in this paper. Even if in this paper we focus on the VaR computation to obtain the corresponding capital requirement, it will be interesting to use other risks measures, for instance the Expected Shortfall (ES) measure, and analyze their impact on the computation of the associated capital requirement. The use of the ES is not required by the regulator but it would be interesting because it is a coherent risk measure [START_REF] Artzner | Coherent measures of risk[END_REF], Extensions are proposed in [START_REF] Guégan | A mathematical resurgence of risk management: an extreme modeling of expert opinions[END_REF]). On the other hand there are alternatives to the Monte Carlo method to calculate the LDF [START_REF] Luo | Computing tails of compound distributions using direct numerical integration[END_REF], [START_REF] Guégan | A modified panjer algorithm for operational risk capital computation[END_REF]) permitting to improve the computation speed that could be investigated. Finally, to take into account the effect of the tail behavior, we focus in this paper on the Generalized Pareto Distribution, nevertheless other alternatives could be considered, e.g. the extreme value distributions defined in the Fisher-Tippett theorem [START_REF] Fisher | Limiting forms of frequency distributions of the largest or smallest member of a sample[END_REF]), the g-and-h distributions, or multivariate methods through the extreme value copulas [START_REF] Gudendorf | Extreme-value copulas[END_REF]). All these subjects will be discussed in companion papers.

A Traditional distributions

X (2)

Table 6: Goodness-of-fit of the presented theoretical distributions to the sets X (1) and X (2) : the parameters have been estimated by maximum likelihood and we have chosen the Kolmogorov-Smirnov statistic. The p-values are all lower than 1%. It's not satisfactory. Considering goodness-of-fit test results, it is not possible to state that a distribution is better than another to model the losses.


François Bobot

Jean-Christophe Filliâtre

Claude Marché

Andrei Paskevich

Why3: Shepherd Your Herd of Provers ⋆

Why3 is the next generation of the Why software verification platform. Why3 clearly separates the purely logical specification part from generation of verification conditions for programs. This article focuses on the former part. Why3 comes with a new enhanced language of logical specification. It features a rich library of proof task transformations that can be chained to produce a suitable input for a large set of theorem provers, including SMT solvers, TPTP provers, as well as interactive proof assistants.

Introduction

Why3 is the next generation of the Why software verification platform. In this article, we present it as an environment for logical specification that targets a multitude of automated and interactive theorem provers. It provides a rich syntax based on first-order language and a highly configurable toolkit to convert specifications into proof obligations in various formats.

The development of Why3 is mainly motivated by the necessity to model the behavior of programs (both purely applicative and imperative) and formally prove their properties. It is commonly admitted that verification of non-trivial programs requires designing a pure logical model of the considered programs. In JML [START_REF] Burdy | An overview of JML tools and applications[END_REF] or Spec# [START_REF] Barnett | The Spec# Programming System: An Overview[END_REF], for instance, such models are described using the pure fragment of the underlying programming language. In the L4.verified project [START_REF] Klein | seL4: Formal verification of an OS kernel[END_REF], the Haskell language is used to model the C code of a micro-kernel. Proof assistants such as Coq [START_REF] Bertot | Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions[END_REF], PVS [START_REF]The PVS system[END_REF], or Isabelle [START_REF]The ISABELLE system[END_REF] also provide rich specification languages that are convenient to model programs.

Why3 distinguishes itself from the aforementioned approaches in that we want to provide as much automation as possible. Instead of being a theorem prover by itself, Why3 intends to provide a front-end to third-party theorem provers. To this end, we propose a common specification language which aims at maximal expressiveness without sacrificing efficiency of automated proof search (Section 2). Another challenge is modular specification. Our proposal is a notion of reusable theories and an associated mechanism of "cloning" (Section 3). As we target a large set of theorem provers whose language and logic range from mono-sorted first-order logic to many-sorted first-order logic modulo theories to the Calculus of Inductive Constructions, we provide an extensible framework to translate the language of Why3 to these various logic languages (Section 4). Finally, we briefly describe the set of tools in the current distribution of Why3 (Section 5).

Logic

The logic of Why3 is a first-order logic with polymorphic types and several extensions: recursive definitions, algebraic data types and inductive predicates.

Types. A type can be non-interpreted, an alias for a type expression or an algebraic data type. For instance, the type of polymorphic binary trees is introduced as follows:

type tree 'a = Leaf | Node (tree 'a) 'a (tree 'a)

A particular case of algebraic types are enumerations.

type answer = Yes | No | MayBe

Built-in types include integers (int), real numbers (real) and polymorphic tuples. The following declaration defines the type answer tree as an alias for a pair: type answer_tree 'a = (tree 'a, answer) Function and Predicate Symbols. Every function or predicate symbol in Why3 has a (polymorphic) type signature. For example, an abstract function that merges two integer trees can be declared as follows: function merge (tree int) (tree int) : tree int Both functions and predicates can be given definitions, possibly mutually recursive. As examples, we can calculate the height of a tree function height (t: tree 'a) : int = match t with | Leaf -> 0 | Node l _ r -> 1 + max (height l) (height r) end or test whether the elements of a tree are both sorted and within given bounds predicate sorted (t: tree int) (min: int) (max: int) = match t with | Leaf -> true | Node l x r -> sorted l min x /\ min <= x <= max /\ sorted r x max end Why3 automatically verifies that recursive definitions are terminating. To do so, it looks for an appropriate lexicographic order of arguments that guarantees a structural descent. Currently, we only support recursion over algebraic types. Other kinds of recursively defined symbols have to be axiomatized. In future versions of Why3, we plan to allow annotating recursive definitions with termination measures. Such definitions would generate proof obligations to ensure termination.

Another extension to first-order language adopted in Why3 is inductive predicates. Such a predicate is the least relation satisfying a set of clauses. For instance, the subsequence relation over finite lists is inductively defined as follows: Standard positivity restrictions apply to ensure the existence of a least fixed point.

Terms and Formulas. First-order language is extended, both in terms and formulas, with pattern matching, let-expressions, and conditional (if-then-else) expressions. We have decided to be faithful to the usual distinction between terms and formulas that is made in the first-order logic. Thus we make a difference between a predicate symbol and a function symbol which returns a bool-typed value, bool being defined with type bool = True | False. However, to facilitate writing, conditional expressions are allowed in terms, as in the following definition of absolute value:

function abs (x: int) : int = if x >= 0 then x else -x
Such a construct is directly accepted by provers not making a distinction between terms and formulas (e.g. provers supporting the SMT-LIB V2 format [START_REF] Barrett | The SMT-LIB Standard: Version 2.0[END_REF]). In order to translate if-then-else constructs to traditional first-order language, Why3 lifts them to the level of formulas and rewrites them as conjunctions of two implications.

Theories

Why3 input is organized as a list of theories. A theory is a list of declarations.

Declarations introduce new types, functions and predicates, state axioms, lemmas and goals. These declarations can be directly written in the theory or taken from existing theories. Figure 1 contains an example of Why3 input text, containing four theories. We start with a theory Order of partial order, declaring an abstract type t and an abstract binary predicate (<=). The next theory, List, declares a new algebraic type of polymorphic lists, list 'a, together with a recursively defined predicate of membership. Now we want to construct a theory SortedList of ordered lists. We want to reuse the definition of polymorphic lists given in theory List, as well as the axioms from Order. The use import List command indicates that this new theory may refer to symbols from theory List. These symbols are accessible in a qualified form, such as List.list or List.Cons. The import qualifier additionally allows us to use them without qualification. Then we clone theory Order. This is pretty much equivalent to copy-pasting every declaration from Order to SortedList. Finally, we introduce an inductive predicate sorted and state as a lemma that the head of a sorted list is smaller or equal to all subsequent elements.

Notice an important difference between use and clone. If we use a theory, say List, twice (directly or indirectly), there is no duplication: there is still only one type of lists and a unique pair of constructors. On the contrary, when we clone a theory, we create a local copy of every cloned declaration, and the newly created symbols, despite having the same names, are different from their originals. Now, we can instantiate theory SortedList to any ordered type, without having to retype the definition of sorted. Let us build a theory SortedIntList for sorted lists of integers. We first import the theory of integers int.Int from Why3's standard library -the prefix int indicates the file in the standard library containing theory Int. The next declaration clones SortedList (i.e. copies its declarations) substituting type int for type O.t of SortedList and the default order on integers for predicate O.(<=). Why3 controls that the result of cloning is well-typed. Notice that, when we instantiate an abstract symbol, its declaration is not copied from the theory being cloned. Thus, we do not create a second declaration of type int in SortedIntList.

Why should we clone theory Order in SortedList if we make no instantiation? Couldn't we write use import Order as O instead? The answer is no. When we use a theory, we mean to share its symbols and declarations with other places where this theory is used. On the other hand, when we clone a theory, we obtain a fresh, local copy of its declarations. Therefore, when cloning a theory, we can only instantiate the symbols declared locally in this theory, not the symbols imported with use. Therefore, we create a local copy of Order in SortedList to be able to instantiate t and (<=) later.

The mechanism of cloning bears some resemblance to modules and functors of ML-like languages. Unlike those languages, Why3 makes no distinction between modules and module signatures, modules and functors. Any Why3 theory can be use'd directly or instantiated in any of its abstract symbols.

Proof Tasks

The principal activity of Why3 can be described as processing of proof tasks. A proof task is basically a sequent: a list of declarations that ends with a goal. A proof task is flat: it does not contains any use or clone anymore. Why3 starts by extracting a set of proof tasks from a given theory. Suppose we want to send a proof task to a particular prover, say Z3 [START_REF] De Moura | Z3, an efficient SMT solver[END_REF]. Not only is the input syntax of Z3 different from Why3's syntax, there are also significant differences in the logic of the two systems. For instance, Z3 does not support polymorphism or inductive predicates. We need to apply a series of transformations that will gradually translate Why3's logic into the prover's logic. This series of transformations is controlled by a configuration file, called a driver, associated to any prover supported by Why3. The task flow from theories to provers is illustrated in Figure 2.

Figure 3 contains a simplified driver for Z3. In the driver, we specify a prettyprinter corresponding to the prover's input format (smtv2 here). We also give regular expressions to interpret the prover output. Next we enumerate the transformations to be applied to a proof task before it can be sent to the pretty-printer. For instance, inline trivial expands "simple" definitions, such as predicate (>=) (x y : t) = y <= x

In the current implementation, we call a definition simple whenever it is nonrecursive, right linear and does not contain variables at depth more than one. This might change in future versions of Why3. Transformation eliminate_ algebraic_smt encodes algebraic data types and pattern-matching expressions in terms of uninterpreted type and function symbols [START_REF] Paskevich | Algebraic types and pattern matching in the logical language of the Why verification platform (version 2)[END_REF]. Finally, encoding smt eliminates polymorphic types from the proof task, converting it to an equivalent monomorphic many-sorted sequent [START_REF] Bobot | Expressing Polymorphic Types in a Many-Sorted Language[END_REF]. For description of other transformations, we refer the reader to Why3's manual [START_REF] Bobot | The Why3 platform[END_REF]. Finally, to take into account built-in theories of Z3, we specify the correspondence between Why3 symbols and Z3 interpreted symbols. For instance, integer addition (defined in theory int.Int) corresponds to the built-in operation + of Z3. Also, we can omit all axioms which are already known to Z3.

printer "smtv2" filename "%f-%t-%g.smt" valid "^unsat" invalid "^sat" unknown "^\\(unknown\\|Fail\\)" "Unknown" time "why3cpulimit time : %s s" transformation "inline_trivial" transformation "eliminate_builtin" transformation "eliminate_definition" transformation "eliminate_inductive" transformation "eliminate_algebraic_smt" transformation "simplify_formula" transformation "discriminate" transformation "encoding_smt" prelude "(set-logic AUFNIRA)" theory BuiltIn syntax type int "Int" syntax type real "Real" syntax predicate (=) "(= %1 %2)" end theory int.Int prelude ";;; this is a prelude for Z3 integer arithmetic" syntax function zero "0" syntax function one "1" syntax function (+) "(+ %1 %2)" syntax function (-) "(-%1 %2)" syntax function (*) "(* %1 %2)" syntax function (-_) "(-%1)" syntax predicate (<=) "(<= %1 %2)" syntax predicate (<) "(< %1 %2)" syntax predicate (>=) "(>= %1 %2)" syntax predicate (>) "(> %1 %2)" Users can develop pretty-printers and transformations of their own, dynamically linked to Why3 as plug-ins. They are registered under unique names, which can be subsequently referred to in drivers. As a consequence, a user can easily add support for a new prover or tweak the interface to an existing one. For example, along with the driver in Figure 3, we provide an alternative driver for Z3 with support for built-in theory of arrays. To avoid writing the same driver rules several times, common parts can be put in separate files and included in drivers.

remove

Architecture

Why3 is implemented as a OCaml programming library. Every functionality (term construction, parsing, proof task transformations, prover calls, etc.) is given in a form of an API. We took a defensive approach in designing this API: Why3 does not allow constructing an ill-formed or ill-typed term, or to use a nondeclared symbol in a theory or a proof task. A special effort is made to share the common sub-terms and sub-tasks, and to memoize the intermediate results of transformations on these sub-tasks. In this way, we avoid a lot of redundant work since, in the most common case where proof tasks originate from the same theory, they share the most of their premises.

The tools we provide in Why3 distribution are built on top of this common library. We anticipate other projects to make use of this library. For instance, integrating automated theorem provers in an interactive proof assistant can be naturally done by linking with Why3 (assuming we trust the prover answers). Another way of using Why3 is to supply new parsers, transformations, or pretty-printers in the form of dynamically loadable plug-ins. As an example, we distribute a parser for the TPTP format, allowing us to test Why3 on a vast collection of theorem proving problems [START_REF] Sutcliffe | The TPTP problem library[END_REF].

We package three main tools with Why3:

a simple command-line interface why3, to launch a selected prover on a set of goals in a given file;

an interactive graphical user-interface why3ide; -a tool why3bench to benchmark different automated provers (or different configurations of the same prover) on large sets of problems. It is also useful to compare axiomatizations or transformations.

A screenshot of the Why3 GUI is shown in Figure 4. On the left side we see the available provers. We can apply some transformations to a proof task before sending it to the prover; for example, split a goal or unfold a definition in it. The goal in theory SortedIntList is quite simple and Alt-Ergo [7] proves it in an instant. The lemma sorted mem in theory SortedList is, on the other hand, more difficult for automated prover since it requires induction. We thus resort to an interactive proof assistant, namely Coq, to discharge this proof task. Using the "Edit" button, the user can launch a Coq IDE to edit a proof script. After the editing session is finished, Why3 GUI rechecks that the saved proof script is accepted by Coq.

Why3 GUI saves the state of a proof session in a database file. A user can modify the initial Why3 file and then return to GUI and replay the previous proof session. For all proof tasks that have not been automatically discharged in this way, the user has to reconstruct the proof. In the future, we plan to extend Why3 GUI to a full-fledged IDE.

Related Work and Perspectives

We presented Why3, a language for specification and a tool to translate it into proof obligations for various interactive and automated theorem provers. Why3 improves upon the former Why 2 platform both in terms of expressiveness, architecture, extensibility (see the manual [START_REF] Bobot | The Why3 platform[END_REF] for an exhaustive list of changes). The Why3 platform can be used by itself, as some kind of standalone "meta" theorem prover, but the main purpose of Why3 is to be used as an intermediate language. For instance, we are currently designing a plug-in for the Coq proof assistant, to extract the first-order part of Coq goals and pass them to automated theorem provers. At the moment, Why3 does not attempt to analyze the output of an automated prover (neither proofs nor counterexamples). A short term perspective would be to translate counterexamples back to Why3 language. This requires not only to parse the output of a particular prover, but also to reverse the effect of various task transformations of Why3. In a long term perspective, we would like to augment the confidence in prover results by producing Coq or Isabelle certificates, in the spirit of Isabelle's Sledgehammer [START_REF] Meng | Automation for interactive proof: first prototype[END_REF].

At the same time, we are re-implementing a verification condition generator for a programming language, WhyML, annotated with Why3 pre/post-conditions. (Interested readers are invited to visit our gallery of verified programs at http: //proval.lri.fr/gallery/why3.en.html.) We also plan to use WhyML as an intermediate language for program verification, in the spirit of the former Why platform [START_REF] Filliâtre | The Why/Krakatoa/Caduceus platform for deductive program verification[END_REF] or Boogie [START_REF] Barnett | Boogie: A Modular Reusable Verifier for Object-Oriented Programs[END_REF]. This is one of the two principal approaches to program verification, where a general-purpose programming language is equipped with a specification language and then possibly translated to the intermediate language of a VCGen. This is the case of VCC [START_REF] Dahlweid | VCC: Contractbased modular verification of concurrent C[END_REF], Spec# [START_REF] Barnett | The Spec# Programming System: An Overview[END_REF], Dafny [START_REF] Leino | Dafny: An Automatic Program Verifier for Functional Correctness[END_REF], Chalice [START_REF] Leino | Verification of concurrent programs with Chalice[END_REF], ESC/Java2 [START_REF] Cok | ESC/Java2: Uniting ESC/Java and JML[END_REF], Krakatoa [START_REF] Marché | The Krakatoa tool for deductive verification of Java programs[END_REF], Frama-C [START_REF]The Frama-C platform for static analysis of C programs[END_REF]. The other principal approach uses a deep embedding of a programming language and its semantics in the logic of a general-purpose proof assistant. This is the case of SunRise [START_REF] Homeier | A mechanically verified verification condition generator[END_REF], KIV [START_REF] Reif | Proving system correctness with KIV 3.0[END_REF], Isabelle/Simpl [START_REF] Schirmer | Verification of Sequential Imperative Programs in Isabelle/HOL[END_REF], KeY [START_REF]Verification of Object-Oriented Software: The KeY Approach[END_REF], Ynot [START_REF] Nanevski | Reasoning with the awkward squad[END_REF], etc.

While the latter approach benefits from rich specification languages, one can argue that these languages are not close enough to the programming language constructs, creating another entry barrier for a new user. Additionally, proofs are typically performed in an interactive way, since underlying environments do not offer as much automation as state-of-the-art theorem provers (although the Sledgehammer effort strives to fill this gap). On the other hand, the former approach, which Why3 belongs to, offers more automation but poorer specification languages. We believe that Why3 features presented in this paper (inductive predicates, algebraic data types, theories) help to alleviate this drawback. We intend to promote these constructions to existing specification languages, such as ACSL [START_REF] Baudin | ACSL: ANSI/ISO C Specification Language, version 1.4[END_REF] or JML [START_REF] Burdy | An overview of JML tools and applications[END_REF].

  inductive sub (list 'a) (list 'a) = | empty: sub (Nil: list 'a) (Nil: list 'a) | cons : forall x: 'a, s1 s2: list 'a. sub s1 s2 -> sub (Cons x s1) (Cons x s2) | dive : forall x: 'a, s1 s2: list 'a. sub s1 s2 -> sub s1 (Cons x s2)

Fig. 1 .

 1 Fig. 1. Example of Why3 text.

2 Fig. 2 .

 22 Fig. 2. Task flow in Why3.

Fig. 3 .

 3 Fig. 3. Driver for Z3.

Fig. 4 .

 4 Fig. 4. Why3 GUI screenshot.

⋆ This work was partly funded by the U3CAT (ANR-08-SEGI-021, http://frama-c. com/u3cat/) and DECERT (ANR-08-DEFI-005, http://decert.gforge.inria. fr/) projects of the French national research organization (ANR), and the Hilite project (http://www.open-do.org/projects/hi-lite/) of the System@tic ICT cluster of Paris-Région Île-de-France.