Igor Konnov
email: igor.konnov@inria.fr

Josef Widder
email: widder@forsyte.at

ByMC: Byzantine Model Checker

, we have introduced a technique for automatic verification of threshold-guarded distributed algorithms that have the following features: (1) up to t of processes may crash or behave Byzantine; (2) the correct processes count messages and progress when they receive sufficiently many messages, e.g., at least t + 1; (3) the number n of processes in the system is a parameter, as well as t; (4) and the parameters are restricted by a resilience condition, e.g., n > 3t.

In this paper, we present Byzantine Model Checker that implements the above-mentioned technique. It takes two kinds of inputs, namely, (i) threshold automata (the framework of our verification techniques) or (ii) Parametric Promela (which is similar to the way in which the distributed algorithms were described in the literature). We introduce a parallel extension of the tool, which exploits the parallelism enabled by our technique on an MPI cluster. We compare performance of the original technique and of the extensions by verifying 10 benchmarks that model fault-tolerant distributed algorithms from the literature. For each benchmark algorithm we check two encodings: a manual encoding in threshold automata vs. a Promela encoding.

Introduction

In recent work [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF][START_REF] Konnov | SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms[END_REF][START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF] we applied bounded model checking to verify reachability properties of threshold-based fault-tolerant distributed algorithms (FTDA), which are parameterized in the number of processes n and the fraction of faults t. FTDAs typically work only under arithmetic resilience conditions such as n > 3t. Our methods allow us to do parameterized verification of sophisticated FTDAs [START_REF] Mostéfaoui | Evaluating the conditionbased approach to solve consensus[END_REF][START_REF] Raynal | A case study of agreement problems in distributed systems: Nonblocking atomic commitment[END_REF][START_REF] Guerraoui | Non-blocking atomic commit in asynchronous distributed systems with failure detectors[END_REF][START_REF] Song | Bosco: One-step Byzantine asynchronous consensus[END_REF][START_REF] Brasileiro | Consensus in one communication step[END_REF][START_REF] Dobre | One-step consensus with zero-degradation[END_REF] that have not been automatically verified before. Our bounded model checking technique produces a number of queries to a Satisfiability Modulo Theories solver (SMT). These queries correspond to different execution patterns.

// n processes follow the code: input ui ∈ {0, 1}; send ui to all; wait until some value vi ∈ {0, 1} is received n+1 2 times; decide on vj; In [START_REF] Konnov | SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms[END_REF], we conjectured that, by design, this technique allows many SMT queries to be checked in parallel. In this paper, we present a parallel extension of ByMC that executes SMT queries in a computer cluster.

The contributions of this paper are as follows: 1. We present the tool ByMC 2.4.1 that implements sequential and parallel verification [START_REF] Konnov | SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms[END_REF][START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF]. The parallel verification is implemented with MPI (Message Passing Interface). 2. We introduce the details of the parallel extension of the technique and perform experimental evaluation, both for the sequential and parallel versions of the tool. 3. We report the experimental results both for the abstractions that are automatically constructed from Promela code (as in [START_REF] Konnov | SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms[END_REF][START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF]) and for manual abstractions in terms of threshold automata, which we use as a direct input for the first time. Our experiments show that explicit modeling of faulttolerant distributed algorithms with threshold automata leads to a dramatic speed up in most cases.

Distributed algorithm example: Naïve Voting

In order to describe what kind of distributed algorithms our tool ByMC is designed for, we start with a simple threshold-guarded algorithm. In this section, we take the point of view of an algorithm designer and apply the arguments that can be found in the distributed algorithms literature [START_REF] Attiya | Distributed Computing[END_REF][START_REF] Lynch | Distributed Algorithms[END_REF]. Consider a distributed system of n processes, whose goal is to unanimously decide on a binary value v ∈ {0, 1}. We would like to design a distributed algorithm that satisfies the following three properties3 : -Agreement. No two correct processes decide on different values (0 and 1).

-Validity. If a correct process decides on a value v ∈ {0, 1}, then there is a process i, whose initial value u i equals v. -Termination. All correct processes eventually decide.

Figure 1 shows a naïve attempt to solve this problem by majority voting. As usual in the distributed algorithms literature, we give a solution in pseudocode, which is supposed to work as follows. Each process starts with a binary value u i ∈ {0, 1} and sends u i to all processes, including itself. When a process receives a value v ∈ {0, 1} from a majority of processes, it decides on v.

Does Naïve Voting satisfy agreement, validity, and termination? Unfortunately, the pseudo-code does not provide us with sufficient detail to answer the question: Assumptions about the process scheduler, message-delivery, possible faults, etc. are missing. For instance, if messages can be lost, a process may never receive sufficiently many messages to get over the guard in line 4. Thus we have to specify systems assumptions. Let us consider an asynchronous model [START_REF] Attiya | Distributed Computing[END_REF][START_REF] Lynch | Distributed Algorithms[END_REF] with crashes and Byzantine faults [START_REF] Pease | Reaching agreement in the presence of faults[END_REF]:

-Asynchronous computations. Every correct process is scheduled infinitely often, and there are no assumptions on the relative processor speeds. The process steps are interleaved. -Reliable communication. The processes communicate via message passing.

Every message sent by a correct process is eventually delivered, although there are no timing or ordering assumptions about message delivery. -Faults. A fraction f of processes may fail. For instance, they can crash or behave Byzantine -the faulty processes do not follow the algorithm. There is an upper bound t ≥ f on the number of faults. We assume n > 3t for the Byzantine faults, and n > 2t for the crash faults.

Manual proofs. Below, we manually reason about the algorithm's correctness. Such proofs are common in the distributed algorithms literature, cf. [START_REF] Srikanth | Simulating authenticated broadcasts to derive simple faulttolerant algorithms[END_REF][START_REF] Song | Bosco: One-step Byzantine asynchronous consensus[END_REF][START_REF] Tseng | Voting in the presence of byzantine faults[END_REF].

Validity We consider the Byzantine case here, which is more complicated. In order to decide on a value v in line 6, a correct process has to receive n+1 2 messages carrying v. By the assumption on the number of faults (n > 3t and t ≥ f ), we have f < n+1

2

, and if a process decides on v in 6, there is at least one correct process that has sent the value v in line 3. Thus, the algorithm satisfies "Validity". Agreement Whether the algorithm satisfies "Agreement" depends on the considered fault model:

-No faults or crash faults. By line 4, a process has to receive the same value from n+1 2 distinct processes. Since 2• n+1

2

> n, and each process sends only one value (line 3), no two processes i, j : 1 ≤ i < j ≤ n can reach line 6 with different values v i = v j . Thus, the processes cannot decide differently, and agreement is satisfied.

-Byzantine faults. When f > 0, the Byzantine processes can send value 0 to a process i and value 1 to a process j : j = i. If the initial states of the correct processes are split into two equal sets, that is, n -f = 2 • |{k ∈ {1 . . . n} : k is correct and u k = 0}|, then the processes i and j reach line 6 with the values v i = 0 and v j = 1. As a result, agreement can be violated, and a verification tool must produce a counterexample. Termination Assume that there are no faults (f = 0) and the initial states are equally partitioned, that is, n = 2 • |{k ∈ {1 . . . n} : k is correct and u k = 0}|.

No process can pass beyond line 4, as none of the initial value sets form a majority. Therefore, Naïve Voting violates liveness, namely, "Termination".

This subtle bug renders the algorithm useless! A tool should thus not only check invariants, but also find counterexamples to liveness specifications. The manual proofs are tricky, as they combine several kinds of reasoning: temporal reasoning, local reasoning about process code, global reasoning about the number of messages, correct and faulty processes, etc. Our tool ByMC automatically proves temporal properties (or finds counterexamples) of distributed algorithms that (i) communicate by sending to all, and (ii) contain actions that are guarded by comparison of the number of received messages against a linear combination of parameter values (e.g., for a majority).

Inputs: Parametric Promela & Threshold Automata

The algorithm in Figure 1 looks quite simple. However, as one can see from the assumptions on, e.g., faults and communication in Section 2, many details (that are often deemed "non-essential" by algorithm designers) are missing in the pseudo code. Our tool addresses this challenge by supporting two formal languages that are tailored for modeling of threshold-guarded distributed algorithms and the system assumptions: parametric Promela [START_REF] John | Towards modeling and model checking fault-tolerant distributed algorithms[END_REF][START_REF] John | Parameterized model checking of fault-tolerant distributed algorithms by abstraction[END_REF] and threshold automata [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF]. Parametric Promela offers modeling that closely mimicks the behavior of the pseudo code statements, whereas threshold automata are an abstraction that allows for efficient model checking techniques [START_REF] Konnov | SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms[END_REF][START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF]. When given code in parametric Promela, ByMC internally applies data abstraction to construct a threshold automaton, as explained in [START_REF] Konnov | What you always wanted to know about model checking of fault-tolerant distributed algorithms[END_REF]. However, the automatically computed threshold automata are usually much larger than those constructed manually by a distributed algorithms expert. For this reason, the user can directly give a threshold automaton as the input to the tool.

Parametric Promela

Promela is the input language of the Spin model checker [START_REF] Holzmann | The SPIN Model Checker[END_REF]. As it is designed to specify concurrent systems, several features are suitable for capturing distributed algorithms. However, Spin is a finite state model checker, and so Promela only allows us to specify finite state systems. We have thus extended Promela in order to have a parametric number of processes and faults, etc. In the following we will discuss some of our extensions.

Figure 3 shows a model of the Naïve Voting algorithm from Figure 1. This example contains all the essential features of parametric Promela. In line 2, we declare parameters: the number of processes n, the number of Byzantine processes f , and the minimal size of a majority set, that is, n+1 2 . In line 3, we declare two shared integer variables nsnt0 and nsnt1 that store the number of zeroes and ones sent by the correct processes. The expressions assume(...) in lines 4-5 restrict the choice of parameter values.

The behavior of the n -f correct processes is modeled in lines 6-32. To describe a process state, we introduce the following local variables: } od; // next step } // atomic propositions atomic ex D0 = some(Proc:pc == D0); atomic ex D1 = some(Proc:pc == D1); atomic all decide = all(Proc:pc == D0 || Proc:pc == D1); atomic ex V0 = some(Proc:pc == V0); atomic ex V1 = some(Proc:pc == V1); atomic in transit0 = some(Proc:nrcvd0 < nsnt0); atomic in transit1 = some(Proc:nrcvd1 < nsnt1); pc to store the algorithm's control state, that is, whether a process is initialized with values 0 and 1 (i.e., pc=V0 and pc=V1 resp.), sent a message (pc=SE), decided on values 0 and 1 (i.e., pc=D0 and pc=D1 resp.) -nrcvd0 and nrcvd1 to store the number of zeroes and ones received from the correct and Byzantine processes; and next-state variables next pc, next nrcvd0, and next nrcvd1 that are used to perform a process step. An initial process state is chosen non-deterministically in lines 12-13.

#define V0 0 // likewise, V1 is 1, SE is 2, D0 is 3, D1 is 4 symbolic int n / *
// LTL formulae ltl agreement { [](!ex D0 || !ex D1) } ltl termination { (<>[](!in transit0 && !in transit1)) -> <>all decide } ltl validity0 { <>(ex D0) -> ex V0 } ltl validity1 { <>(ex D1) -> ex V1 }
A single process step is encoded as an atomic block in lines 14-31, which corresponds to an indivisible receive-compute-send step. In lines 15-18, a process possibly receives new messages: by invoking havoc(x), we forget the contents of a variable x, and by writing assume(e), we restrict the variable values to those that satisfy a logical expression e. Note that the statements havoc and assume do not belong to the standard Promela; they belong to parametric Promela and are inspired by the similar statements in Boogie [START_REF] Barnett | Boogie: A modular reusable verifier for object-oriented programs[END_REF]. Lines 20-27 encode the computations that can be found in pseudo-code in Figure 1. Like in Promela, a process non-deterministically picks an option of the form ":: guard -> actions", if guard evaluates to true, and executes actions.

To specify temporal properties, we first define atomic propositions in lines 34-38. The keywords some and all correspond to existential and universal quantification over the processes; they belong to parametric Promela. In lines 40-43, define LTL formulas that capture the properties of consensus (cf. Section 2).

Promela code in Figure 3 models the informal pseudo code of Naïve Voting. Note that the manual translation from pseudo code is straightforward, except for one thing: It may seem more honest to maintain sets of sent and received messages, instead of storing only integer message counters such as nrcvd0 and nsnt0. It has been proven that modeling with sets is equivalent (bisimilar) to modeling with message counters [START_REF] Konnov | Accuracy of message counting abstraction in fault-tolerant distributed algorithms[END_REF]. Obviously, modeling with message counters produces smaller transition systems (cf. [START_REF] John | Towards modeling and model checking fault-tolerant distributed algorithms[END_REF]).

Threshold Automata

Our code in parametric Promela has several features: (i) each atomic step is encoded as an imperative sequence of statements, (ii) and the processes explicitly store the number of received messages in local variables such as nrcvd0 and nrcvd1. One can argue that this level of detail is not necessary, and it makes the verification problem harder. Threshold automata are a more abstract model for threshold-guarded fault-tolerant distributed algorithms [START_REF] Konnov | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability[END_REF], as they enable guarded transitions as soon as sufficiently many messages have been sent. Intuitively, the reception variables nrcvd0 and nrcvd1 are bypassed by such modeling. In this section, we introduce threshold automata in a way that explains how automata capture local transitions of individual processes. The semantics of threshold automata are then defined via counter systems in Section 4 that model runs of collections of processes, that is, distributed computations.

We model Naïve Voting with the threshold automaton shown in Figure 2. Its code in the .ta input format of ByMC is shown in 4. A threshold automaton for Naïve Voting in the .ta format n -f instances of the threshold automaton; each instance is modelling a correct process. The automata operate on shared variables such as nsnt 0 and nsnt 1 , which can be only incremented. A threshold automaton resides in a local state from a finite set L, e.g., in our example, L = {V0, V1, SE, D0, D1}. A rule (corresponding to an edge in Figure 2) can move an automaton from one local state to another, provided that the shared variables in the current global state satisfy the rule's threshold guard, e.g., 2•(nsnt 0 +f ) ≥ n+1. If a rule is labeled with an increment of a shared variable, e.g., nsnt 0 ++, then the shared variable is updated accordingly.

<>[](locV0 == 0 && locV1 == 0 && (2 * nsnt0 < N + 1 || locSE == 0) && (2 * nsnt1 < N + 1 || locSE == 0)) -> <>(locD0 != 0 || locD1 != 0); } } / * Proc * / Fig.

Theoretical Background

System

We assume fixed three finite sets: the set L contains the local states, the set Γ contains the shared variables that range over non-negative integers, and the set Π contains the parameters that range over non-negative integers.

Configurations Σ and I. A configuration is a vector σ = (κ, g, p), where σ.κ is a vector of counter values, σ.g is a vector of shared variable values, and σ.p = p is a vector of parameter values. In σ.κ we store for each local state , how many processes are in this state. All values are non-negative integers. In every initial configuration global variables have value zero, and all "modelled" processes are in initial locations. If specifications do not limit the behavior of faulty processes (which is typically the case with Byzantine faults), we only model the correct processes explicitly, while the impact of faulty processes is modelled as nondeterminism in the environment.

Threshold Guards are defined according to the following grammar: A transition is a pair t = (rule, factor ) of a rule of the TA and a non-negative integer called the acceleration factor, or just factor for short. If the factor is always 1, this corresponds that at each step exactly one processes takes a step, that is, interleaving semantics. Having factors greater than 1 permits a specific form of acceleration where an arbitrary number of processes that are ready to execute a rule can do that at the same time.

Transition t is applicable (or enabled) in configuration σ, if the guard of t.rule evaluates to true, and σ.κ[t.from] ≥ t.factor . Configuration σ is the result of applying the enabled transition t to σ, and write σ = t(σ), if σ .g = σ.g + t.factor • t.u and σ .p = σ.p if t.from = t.to then Finally, the transition relation R ⊆ Σ × Σ of the counter system is defined as follows: (σ, σ ) ∈ R iff there is a rule r ∈ R and a factor k ∈ N 0 such that σ = t(σ) for t = (r, k).

ψ ::= pform | G ψ | F ψ | ψ ∧ ψ pform ::= cform | gform ∨ cform cform ::= ∈Locs κ[ ] = 0 | ∈Locs κ[ ] = 0 | cform ∧ cform gform ::= guard | ¬gform | gform ∧
Observe that configurations, transitions, guard, etc. can be encoded in linear integer arithmetic.

Safety and liveness specifications

Using counter systems, we can also easily express the temporal properties, e.g., those of Naïve Voting. To this end, for every local state ∈ L, we introduce a proposition "κ = 0", which tests that there are no processes in . Since threshold automata do not explicitly track received messages, the assumption of reliable communication is modeled as a fairness assumption over local states and actions. The following formula captures the required fairness, that is, (i) eventually all processes leave their initial state V0 or V1, and (ii) if threshold guards become true, then eventually all processes fire the corresponding rules and thus evacuate the local state SE (the latter implication is written as disjunction):

F G κ V0 = 0 ∧ κ V1 = 0 ∧ (2 • nsnt 0 < n + 1 ∨ κ SE = 0) ∧ (2 • nsnt 1 < n + 1 ∨ κ SE = 0) (RC)
Agreement (A), Validity (V), and Termination (T) can be written as follows:

G (κ D0 = 0 ∨ κ D1 = 0) (A) F (κ D0 = 0) → κ V0 = 0 ∧ F (κ D1 = 0) → κ V1 = 0 (V) RC → F (κ V0 = 0 ∧ κ V1 = 0 ∧ κ SE = 0) (T)
In [START_REF] Konnov | SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms[END_REF], we have introduced a bounded model checking technique with SMT that checks reachability in counter systems of threshold automata for all combinations of the parameters. We proved that if a configuration is reachable, then there is a short schedule that reaches this configuration. As a result, bounded model checking is a complete method for reachability checking in our case. In [START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF], this technique was extended to ELTL FT -a fragment of ELTL(F, G), which allows us to verify safety and liveness of counter systems of threshold automata. The syntax of ELTL FT is given in Table 1. We use this logic to express counterexamples, that is, negations of the safety and liveness specifications from above.

For instance, the negation of agreement and termination in Equations (A) and (T) fit into ELTL FT , and can be written as follows:

F (κ D0 = 0 ∧ κ D1 = 0) (NA) RC ∧ G (κ V0 = 0 ∨ κ V1 = 0 ∨ κ SE = 0) (NT)
Technically, the negation of the formula for validity given in Equation (V) does not belong to the fragment ELTL FT . However, it can be easily rewritten as two formulas, for the values of i equal to 0 and 1:

F (κ Di = 0) ∧ κ Vi = 0 (NV i )

Parameterized model checking by schema enumeration

Our verification technique consists of the following steps: From the ELTL FT specifications, our tool enumerates all shapes counterexamples can have. Each of these shapes is encoded as an SMT query, and using SMT solvers, our tool checks for each shape, whether there exists a run of the system that has this shape. Such a run would then be a witness to the violation of a specification. Consider the agreement property (A) of Naïve Voting. A counterexample is a run of the system that starts in an initial state and satisfies its negation:

F (κ D0 = 0 ∧ κ D1 = 0)
Each counterexample thus (i) satisfies the constraints for initial states, and (ii) is a sequence of applicable transitions, that (iii) end up in a state where (κ D0 = 0 ∧ κ D1 = 0) holds. Indeed checking (A) boils down to checking reachability of a state that satisfies (κ D0 = 0 ∧ κ D1 = 0). Our technique from [START_REF] Konnov | SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms[END_REF] enumerates all shapes of such counterexamples.

The central notion is a simple schema:

{pre}r * 1 , . . . , r * k {post}
where pre, post ⊆ are contraints that encode evaluation of guards, and constraints on the counters (e.g., κ D0 = 0). Thus, the schema captures that pre holds, then some transitions with rules r * 1 , . . . , r * k are ececuted to reach a state where post holds. We denote a simple schema by S. A schema is then a concatenation of simple schemas S 1 , S 2 , . . . S k , for some k.

For our example, the technique from [START_REF] Konnov | SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms[END_REF] would generate among others, a schema like the following

S 1 , S 2 , S 3 = {κ V0 + κ V1 = n}r * 1 , . . . , r * 4 {2 • (nsnt 0 + f ) ≥ n + 1}r * 1 , . . . , r * 4 {(2 • (nsnt 0 + f ) ≥ n + 1), ( 2
• (nsnt 1 + f ) ≥ n + 1)}r * 1 , . . . , r * 4 {(2 • (nsnt 0 + f ) ≥ n + 1), ( 2
• (nsnt 1 + f ) ≥ n + 1), (κ D0 = 0 ∧ κ D1 = 0)}
that is, initially, all of the n processes are in the initial locations V0 and V1, then after application of some rules one of the threshold guards becomes true, then after another application of some rules both guards are true and finally a bad state is reached. The SMT solver now has to find whether an executions exists that has that form. This is done by replacing each Kleene star by a distinct variable that encodes how often a rule r is applied.

A different schema can be obtained by changing the order in which the two threshold guards become true. In general each possible order generates a different schema. The number of different schemas to be checked is factorial in the number of guards [START_REF] Konnov | SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms[END_REF]. As our benchmarks have only a small number of guards, the number of calls to the SMT solver is still practical.

Checking a single lasso schema with SMT

In [START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF] we prove that for our counter systems, a counterexample to a liveness specification has lasso shape, that is:

S 1 . . . S k (S k+1 . . . S k+m ) ω
In this way we obtain a finite representation of an infinite execution, which again can be checked with an SMT solver.

Thus, our tool generates multiple schemas: for each safety or liveness specification, a different schema is obtained by changing the order in which the threshold guards become true. A detailed algorithm for constructing schemas is presented in [START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF][Fig. 10]. In a nutshell, the algorithm constructs a graph that represents the partial order on when propositions and threshold guards evaluate to true in an execution, e.g., the one in Figure 5. Each linear extension of this partial order then defines a sequence on which propositions and guards become true. Two neighboring elements in the sequence are the pre and post of a simple schema; the concatenation of all these simple schemas is the schema our tool checks for satisfiability.

Our tool encodes each schema in SMT and then calls a back-end solver in order to check whether the schema generates a counterexample. In [START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF], we explained the SMT encoding. As the schemas are independent, these checks can be done in parallel. We have implemented and exploited this feature in [START_REF] Lazic | Synthesis of distributed algorithms with parameterized threshold guards[END_REF]. As [START_REF] Lazic | Synthesis of distributed algorithms with parameterized threshold guards[END_REF] was concerned with synthesis, we did not discuss the effects of parallelization there. In the following we discuss and compare the sequential and the parallel approaches.

} else { receive WITNESS<w> from master if w = rank { send CEX<SMT model> to master } // I am the witness } // finish and clean up stale MPI messages on exit

Benchmarks and Experiments

Byzantine model checker is written in OCaml. Its source code and the virtual machines are available from the tool web page 4 . For the experiments conducted in this paper, we used Z3 4.6.0 [START_REF] De Moura | Z3: An efficient SMT solver[END_REF] as a back-end SMT solver, which was linked to ByMC via Z3 OCaml bindings.

In earlier work [START_REF] John | Towards modeling and model checking fault-tolerant distributed algorithms[END_REF], we encoded our benchmarks in Parametric Promela, using a shared variable to record the number of processes that have sent a message, and using for each process a local variable that records how many messages a process received. For this modeling we presented a data abstraction and counter abstraction in [START_REF] John | Parameterized model checking of fault-tolerant distributed algorithms by abstraction[END_REF]. To compare later verification techniques with these initial results, we kept that encoding, although the newer techniques rest on a more abstract model of threshold automata, which have finitely many local states.

The threshold automata constructed by data abstraction are significantly larger than threshold automata constructed by a human expert. To see the influence of these modeling decisions on the verification results, we manually encoded our benchmarks as threshold automata. These benchmarks are available from our benchmark repository 5 . Table 2 compares the size of the threshold automata that are: (1) produced automatically by abstraction and (2) hand-coded. The essential features of the automata are: the number of local states |L|, the number of rules |R|, and the numbers of the guards |Φ rise | and |Φ fall |, that is, the guards of the form x ≥ . . . and x < . . . respectively. Moreover, due to data abstraction, we had to consider several cases that differ in the order between the thresholds. They are mentioned in the column "Case".

Table 2 shows the verification results for benchmarks in Promela as well as threshold automata. We ran the sequential schema enumeration (SEQ, [START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF]) and the parallel schema checking technique (MPI) that is presented in this paper. The parallel experiments were run at Vienna Scientific Cluster using 256 CPU cores. For each benchmark, we picked the most challenging specifications -many of them are liveness properties -and show experimental results for them. (Needless to say, we did not run the MPI technique on the benchmarks that could be enumerated with the sequential technique in seconds.) Two columns show the essential features of the enumerated schemas: "number" displays the total number of explored schemas, and "length avg" displays the average length of schemas. For both techniques, we report the computation times and maximal memory usage during a run. For the MPI experiments, we report the average time per CPU core (column "MPI avg") as well as the maximum time per CPU core (column "MPI max"). The deviation from the average case is negligible. As expected, the hand-coded benchmarks are usually verified much faster. Interestingly, the manually constructed threshold automaton for one-step consensus (c1cs [START_REF] Brasileiro | Consensus in one communication step[END_REF]) has more threshold guards than the abstract one: We had to more accurately encode algorithm's decisions, crash faults, and fairness. The sequential technique times out on this benchmark. The parallel technique takes about seven times longer than with the automatic abstraction.

The parallel technique benefits from running on multiple cores, though the actual gains from parallelism depend on the benchmark. As in our experiments the verification times of a single schema negligibly deviate from the average case, the uniform distribution of schemas among the nodes seems sufficient. However, one can construct threshold automata that produce schemas whose verification times significantly vary from each other. We conjecture that an implementation with a dynamic balancer would make better use of cluster resources.

Conclusions

We presented our tool ByMC, and compared its sequential verification implementation to its parallel one. Moreover, by experimental evaluation we showed that manual abstractions give us threshold automata that can be verified significantly faster than those that result from automatic abstraction.

We observe that the sizes of the manually constructed threshold automata are not significantly larger than the (manually crafted) models of round-based distributed consensus presented in [START_REF] Marić | Cutoff Bounds for Consensus Algorithms[END_REF]. In their theory, threshold-guarded expressions also play a central role. Our gains in efficiency in this paper-due to manual encodings-show that the discrepancy was a result of automatic abstraction and not of the technique that uses threshold automata as its input.

We needed from one to three hours per benchmark to specify and debug a threshold automaton, while it usually took us less than 30 minutes to specify the same benchmark in Parametric Promela. The most difficult part of the encoding with threshold automata was to faithfully express fairness constraints over shared variables and process counters. In case of Parametric Promela, fairness constraints were much easier to write, as one could refer to the shared and local variables, which count the number of sent and received messages respectively.

Fig. 1 . 2 • 1 Fig. 2 .

 1212 Fig. 1. Naïve Voting algorithm

  nr. of correct * /, f / * nr. of faulty * /, majority; // majority size int nsnt0, nsnt1; // counters for 0s and 1s sent by the correct processes assume(n > 1 && n > 3 * f); // the resilience condition restricts faults assume(n + 2 == 2 * majority || n + 1 == 2 * majority); // majority = n+1 2 active[nf] proctype Proc() { // run n -f correct processes // control state: initialized with 0 (V0), initialized with 1 (V1), // sent the value (SE), decided on 0 (D0), decided on 1 (D1) byte pc = V0, next pc = V0; // counters for received 0s and 1s int nrcvd0 = 0, nrcvd1 = 0, next nrcvd0 = 0, next nrcvd1 = 0; if :: pc = V0; // non-deterministically initialize with 0 or 1 :: pc = V1; fi; do :: atomic { // a single indivisible step havoc(next nrcvd0); havoc(next nrcvd1); // forget variable values // update message counters (up to f messages from the Byzantine processes) assume(nrcvd0 <= next nrcvd0 && next nrcvd0 <= nsnt0 + f); assume(nrcvd1 <= next nrcvd1 && next nrcvd1 <= nsnt1 + f); // compute the new state and send messages, if needed if :: pc == V0 -> next pc = SE; nsnt0++; // send 0 :: pc == V1 -> next pc = SE; nsnt1++; // send 1 :: pc == SE && next nrcvd0 >= majority -> next pc = D0; // decide on 0 :: pc == SE && next nrcvd1 >= majority -> next pc = D1; // decide on 1 :: pc == SE && next nrcvd0 < majority && next nrcvd1 < majority -> next pc = SE; // wait for more messages :: pc == D0 || pc == D1 -> next pc = pc; // self-loop fi; // update local variables pc = next pc; nrcvd0 = next nrcvd0; nrcvd1 = next nrcvd1; next pc = 0; next nrcvd0 = 0; next nrcvd1 = 0;

Fig. 3 .

 3 Fig. 3. Modeling Naïve Voting in Parametric Promela

Figure 4 .

 4 We are running thresholdAutomaton Proc { local pc; / * control locations: in V0 and V1, initialized with 0 and 1 resp., in D0 and D1, decided on 0 and 1 resp., in SE, sent the initial value * / shared nsnt0, nsnt1; / * the number of 0s and 1s sent by the correct processes * / parameters N, T, F; / * parameter variables * / assumptions (0) { N > 3 * T; T >= F; T >= 1; } / * resilience condition * / locations (0) { locV0: [0]; locV1: [1]; locSE: [2]; locD0: [3]; locD1: [4];}// local states inits (0) { / * initial constraints * / (locV0 + locV1) == N -F; locSE == 0; locD0 == 0; locD1 == 0; nsnt0 == 0; nsnt1 == 0; } rules (0) { / * a set of rules * / / * send message 0 (resp. 1) when initialized with value 1 (resp. 1) * / 0: locV0 -> locSE when (true) do { nsnt0' == nsnt0 + 1; nsnt1' == nsnt1; }; 1: locV1 -> locSE when (true) do { nsnt0' == nsnt0; nsnt1' == nsnt1 + 1; }; 2: locSE -> locD0 / * decide on value 0 * / when (2 * (nsnt0 + F) >= N + 1) do { unchanged(nsnt0, nsnt1); }; 3: locSE -> locD1 / * decide on value 1 * / when (2 * (nsnt1 + F) >= N + 1) do { unchanged(nsnt0, nsnt1); }; / * self loops * / 4: locSE -> locSE when (true) do { unchanged(nsnt0, nsnt1); }; 5: locD0 -> locD0 when (true) do { unchanged(nsnt0, nsnt1); }; 6: locD1 -> locD1 when (true) do { unchanged(nsnt0, nsnt1); }; } specifications (0) { / * LTL formulas * / agreement: [](locD0 == 0 || locD1 == 0); validity0: <>(locD0 != 0) -> locV0 != 0; validity1: <>(locD1 != 0) -> locV1 != 0; termination:

  Guard ::= Int • Shared ≥ LinForm | Int • Shared < LinForm LinForm ::= Int | Int • Param | Int • Param + LinForm Shared ::= a variable from Γ Param ::= a variable from Π Int ::= an integer Transition relation R.

Table 1 .

 1 gform The syntax of ELTL FT -formulas[START_REF] Konnov | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms[END_REF]: pform defines propositional formulas, and ψ defines temporal formulas. We assume that Locs ⊆ L and guard ∈ Φ rise ∪ Φ fall .

• σ .κ[t.from] = σ.κ[t.from] -t.factor , • σ .κ[t.to] = σ.κ[t.to] + t.factor , and • ∀ ∈ L \ {t.from, t.to} it holds that σ .κ[ ] = σ.κ[ ] if t.from = t.to then σ .κ = σ.κ

Table 2 .

 2 The experiments with the sequential (SEQ) and parallel (MPI) techniques on two kinds of inputs: Promela (white rows) and threshold automata (gray rows). The sequential experiments were run with GNU parallel[START_REF] Tange | Gnu parallel-the command-line power tool[END_REF] at AMD Opteron R 6272, 32 cores, 192 GB. The MPI benchmarks were run at Vienna Scientific Cluster 3 using 16 nodes × 16 cores (256 processes). The symbol " " indicates timeout of 24 hours.

	# Input			Case		Threshold		Schemas		Time, seconds Mem, GB
						Automaton		length SEQ	MPI	SEQ MPI
	FTDA (if more than one) |L| |R| |Φ rise | |Φ fall | number avg		avg max	avg
	1 frb			-	7	14	1	0	5	34	1	-	-0.1	-
	2 frb		hand-coded TA	4	9	1	1	70	38	1	-	-0.1	-
	3 strb			-	7	21	3	0	18	72	1	-	-0.1	-
	4 strb		hand-coded TA	4	8	2	0	38	22	1	-	-0.1	-
	5 nbacg			-	24	64	4	0	90	243	6	-	-0.1	-
	6 nbacg		hand-coded TA	8	16	0	1	5	54	1	-	-0.1	-
	7 nbacr			-	77 1031	6	0	517 2489	523	-	-0.7	-
	8 nbacr		hand-coded TA	7	16	0	1	18	63	1	-	-0.1	-
	9 aba		n+t 2	= 2t + 1	37 202	6	0	1172	850	659	12	13 1.0 0.2
	10 aba		n+t 2	> 2t + 1	61 425	8	0	5204 2112 53992 1440 1442 7.2 0.6
	11 aba		hand-coded TA	5	10	2	2	542	57	14	-	-0.1	-
	12 cbc	n 2	< n -t ∧ f = 0 164 2064	0	0	2 8168 1603 290 290 9.3 0.2
	13 cbc	n 2	= n -t ∧ f = 0 73 470	0	0	2 1790	27	9	9 0.6 0.1
	14 cbc	n 2	< n -t ∧ f > 0 165 2072	0	1	4 10213 10024 4943 4943 18.8 0.5
	15 cbc	n 2	= n -t ∧ f > 0 74 476	0	1	4 2258	273	47	47 1.5 0.1
	16 cbc		hand-coded TA	7	14	0	1	5	56	1	-	-0.1	-
	17 cf1s		f = 0	41 280	4	0	90	770	45	5	8 0.2 0.1
	18 cf1s		f = 1	41 280	4	1	523	787	257	6	6 0.4 0.1
	19 cf1s		f > 1	68 696	6	1	3429 2132 10346	29	29 3.8 0.2
	20 cf1s		hand-coded TA	9	26	3	3	13700	122	687	6	8 2.1 0.1
	21 c1cs		f = 0	101 1285	8	0	251	460	331	38	38 0.8 0.1
	22 c1cs		f = 1	70 650	6	1	448	303	239	11	11 0.4 0.1
	23 c1cs		f > 1	101 1333	8	1	2100	404 1865	89	89 1.3 0.4
	24 c1cs		hand-coded TA	9	30	7	3	3.2 • 10 6 ≈ 400		979 981 17.3 1.6
	25 bosco	n+3t 2	+ 1 = n -t 28 152	6	0	20	423	4	3	4 0.1 0.1
	26 bosco	n+3t 2	+ 1 > n -t 40 242	8	0	70 1038	29	6	6 0.2 0.1
	27 bosco	n+3t 2	+ 1 < n -t 32 188	6	0	20	476	4	4	4 0.1 0.1
	28 bosco		n > 5t ∧ f = 0	82 1372 12	0	3431	27	265	35	35 0.3 0.4
	29 bosco		n > 7t	90 1744 12	0	3431	179 1325	52	52 1.0 0.6
	30 bosco		hand-coded TA	8	20	3	4	3429	43	82	4	4 0.2 0.1

Agreement, validity, and termination are typical properties of consensus[START_REF] Attiya | Distributed Computing[END_REF][START_REF] Lynch | Distributed Algorithms[END_REF].

http://forsyte.at/software/bymc

https://github.com/konnov/fault-tolerant-benchmarks/tree/master/isola18

Acknowledgments. We are grateful to our past and present collaborators Annu Gmeiner, Marijana Lazić, Ulrich Schmid, and Helmut Veith, who contributed to many of the described ideas that are now implemented in ByMC.

Supported by: the Vienna Science and Technology Fund (WWTF) grant APALACHE (ICT15-103); and the Austrian Science Fund (FWF) through the National Research Network RiSE (S11403 and S11405), and project PRAVDA (P27722). The computational results presented have been achieved [in part] using the Vienna Scientific Cluster (VSC).

Fig. 5. The graph constructed from the automata guards and formula (NV0) Sequential schema enumeration. In the sequential mode, the schemas are simply checked one-by-one until either a counterexample is found, or all schemas have been enumerated and no counterexample has been found. (Detailed pseudo-code of the function check one order can be found in Figure 10 Parallel schema enumeration. In the MPI mode, the tool runs as a system of N processes, one per CPU; the physical arrangement of the CPUs depends on the cluster configuration. Every process is assigned a unique value rank from 0 to N -1: The process with rank = 0 is the master, whereas the other processes are the workers. Every process is enumerating the schemas as in the sequential mode but checks a schema only if the schema's sequence number i matches the rule: (i mod N ) = rank . In order to terminate quickly when one process has found a bug, the workers asynchronously communicate with the master. After leaving the loop, the workers communicate with the master to deliver a counterexample, if one was found. For presentation, we assume that the master can send to and receive messages from itself.


Maxime Bucher

Stéphane Herbin

Frédéric Jurie

Semantic bottleneck for computer vision tasks

This paper introduces a novel method for the representation of images that is semantic by nature, addressing the question of computation intelligibility in computer vision tasks. More specifically, our proposition is to introduce what we call a semantic bottleneck in the processing pipeline, which is a crossing point in which the representation of the image is entirely expressed with natural language, while retaining the efficiency of numerical representations. We show that our approach is able to generate semantic representations that give state-of-theart results on semantic content-based image retrieval and also perform very well on image classification tasks. Intelligibility is evaluated through user centered experiments for failure detection.

Introduction

Image-to-text tasks have made tremendous progress since the advent of deep learning approaches (see e.g., [START_REF] Das | Visual dialog[END_REF]). The work presented in this paper builds on these new types of image-to-text functions to evaluate the capacity of textual representations to semantically and fully encode the visual content of images for demanding applications, in order to allow the prediction function to host a semantic bottleneck somewhere in its processing pipeline (Fig. 1). The main objective of a semantic bottleneck is to play the role of an explanation of the prediction process since it offers the opportunity to examine meaningfully on what ground will further predictions be made, and potentially decide to reject them either using human common sense knowledge and experience, or automatically through dedicated algorithms. Such an explainable semantic bottleneck instantiates a good tradeoff between prediction accuracy and interpretability [START_REF] Gilpin | Explaining explanations: An approach to evaluating interpretability of ml[END_REF].

Reliably evaluating the quality of an explanation is not straightforward [START_REF] Doshi-Velez | A roadmap for a rigorous science of interpretability[END_REF][START_REF] Biran | Explanation and justification in ml: A survey[END_REF][START_REF] Gilpin | Explaining explanations: An approach to evaluating interpretability of ml[END_REF][START_REF] Ras | Explanation methods in deep learning: Users, values, concerns and challenges[END_REF]. In this work, we propose to evaluate the explainability power of the semantic bottleneck by measuring its capacity to detect failure of the prediction function, either through an automated detector as [START_REF] Zhang | Predicting failures of vision systems[END_REF], or through human judgment. Our proposal to generate the surrogate semantic representation is to associate a global and generic textual image description (caption) and a visual quiz in the form of a small list of questions and answers that are expected to refine contextually the generic caption. The production of this representation is adapted to the vision task and learned from annotated data.

The main contributions of this paper are: (i) The design of two processing chains for content-based image retrieval and multi-label classification hosting a semantic bottleneck; (ii) An original scheme to select sequentially a list of questions and answers to form a semantic visual quiz; (iii) A global fusion approach jointly exploiting the various components of the semantic representation for image retrieval or multi-label

Retrieval

Fig. 1: Semantic bottleneck approach: images are replaced by purely but rich textual representations, for tasks such as multi-label classification or image retrieval.

classification; (iv) A complete evaluation on the MS-COCO database exploiting Visual Dialog annotations [START_REF] Das | Visual dialog[END_REF] showing that it is possible to enforce a semantic bottleneck with only 5% of performance loss on multi-label classification, but a 10% performance gain for image retrieval, when compared to image feature-based approaches; (v) An evaluation of the semantic bottleneck explanation capacity as a way to detect failure in the prediction process and improve its accuracy by rejection.

Related works

Extracting semantic information from images. The representation of images with semantic attributes has received a lot of attention in the recent literature. However, with the exception of the DAP model [START_REF] Lampert | Attribute-based classification for zero-shot visual object categorization[END_REF], which is not performing very well, such models produce vector representations that are not intelligible at all. In contrast, image captioning [START_REF] Vinyals | Show and tell: Lessons learned from the 2015 mscoco image captioning challenge[END_REF][START_REF] Lu | Knowing When to Look: Adaptive Attention via a Visual Sentinel for Image Captioning[END_REF] is by nature producing intelligible representations and can be used to index images. As an illustration, Gordo et al. [START_REF] Gordo | Beyond instance-level image retrieval: Leveraging captions to learn a global visual representation for semantic retrieval[END_REF] addressed the task of retrieving images that share the same semantics as the query image using captions. Despite the success of such recent methods, it has been observed [START_REF] Dai | Towards Diverse and Natural Image Descriptions via a Conditional GAN[END_REF] that such approaches produce captions that are similar when they contain one common object, despite their differences in other aspects. Addressing this issue, [START_REF] Dai | Contrastive Learning for Image Captioning[END_REF] proposed a contrastive learning method for image captioning encouraging distinctiveness, while maintaining the overall quality of the generated captions. Another way to enrich the caption is to generate a set of questions/answers such as proposed in the Visual Dialog framework [START_REF] Das | Visual dialog[END_REF][START_REF] Seo | Visual reference resolution using attention memory for visual dialog[END_REF][START_REF] Lu | Best of both worlds: Transferring knowledge from discriminative learning to a generative visual dialog model[END_REF]. This is what we propose to do by learning how to build dialogs complementary to image captions.

Transferring information from other domains. Producing semantic description of images in natural languages is barely possible without transferring semantic information -expressed as semantic attributes, natural language expressions, dictionaries, etc.from auxiliary datasets containing such information to novel images. This is exactly what Visual Question Answering models can do, the VQA challenge offering important resources, in the form of semantic images, questions, or possible answers. Research on VQA has been very active during the last two years. [START_REF] Malinowski | Ask your neurons: A neural-based approach to answering questions about images[END_REF] proposed an approach relying on Recurrent Neural Network using Long Short Term Memory (LSTM). In their approach, both the image (CNN features) and the question are fed into the LSTM to answer a question about an image. Once the question is encoded, the answers can be generated by the LSTM. [START_REF] Lin | Leveraging visual question answering for image-caption ranking[END_REF] study the problem of using VQA knowledge to improve image-caption ranking. [START_REF] Zhu | Visual7w: Grounded question answering in images[END_REF], motivated by the goal of developing a model based on grounded regions, introduces a novel dataset that extends previous approaches and proposes an attention-based model to perform this task. On their side, [START_REF] Jabri | Revisiting vqa baselines[END_REF] proposed a model receiving the answers as input and predicts whether or not an image-questionanswer triplet is correct. Finally, [START_REF] Wu | Ask me anything: Free-form visual question answering based on knowledge from external sources[END_REF] proposes another VQA method combining an internal representation of the image content with the information extracted from general knowledge bases, trying to make the answering of more complex questions possible.

Producing intelligible representations. The ubiquitousness of deep neural networks in modern processing chains, their structural complexity and their opacity have motivated the need of bringing some kind of intelligibility in the prediction process to better understand and control its behavior. The vocabulary and concepts connected to intelligibility issues are not clearly settled. (explanation, justification, transparency, etc.) Several recent papers have tried to clarify those expressions [START_REF] Lipton | The mythos of model interpretability[END_REF][START_REF] Doshi-Velez | A roadmap for a rigorous science of interpretability[END_REF][START_REF] Doran | What does explainable ai really mean? a new conceptualization of perspectives[END_REF][START_REF] Biran | Explanation and justification in ml: A survey[END_REF][START_REF] Hohman | Visual analytics in deep learning: An interrogative survey for the next frontiers[END_REF][START_REF] Gilpin | Explaining explanations: An approach to evaluating interpretability of ml[END_REF][START_REF] Guidotti | A survey of methods for explaining black box models[END_REF][START_REF] Ras | Explanation methods in deep learning: Users, values, concerns and challenges[END_REF] and separate the various approaches in two goals: build interpretable models and/or provide justification of the prediction. [START_REF] Zhang | Interpreting cnns via decision trees[END_REF] for instance, described an interpretable proxy (a decision tree) able to explain the logic of each prediction of a pretrained convolutional neural networks. The generation of explanations as an auxiliary justification has been addressed in the form of a visual representation of informative features in the input space, usually heat maps or saliency maps [START_REF] Selvaraju | Grad-cam: Visual explanations from deep networks via gradient-based localization[END_REF][START_REF] Rajani | Using explanations to improve ensembling of visual question answering systems[END_REF][START_REF] Montavon | Methods for interpreting and understanding deep neural networks[END_REF], as textual descriptions [START_REF] Hendricks | Generating visual explanations[END_REF], or both [START_REF] Park | Multimodal explanations: Justifying decisions and pointing to the evidence[END_REF]. A large body of studies [START_REF] Mahendran | Understanding deep image representations by inverting them[END_REF][START_REF] Zeiler | Visualizing and understanding convolutional networks[END_REF][START_REF] Dosovitskiy | Inverting visual representations with convolutional networks[END_REF][START_REF] Olah | The building blocks of interpretability[END_REF] have been interested in visually revealing the role of deep network layers or units. Our semantic bottleneck approach fuses those two trends: it provides a directly interpretable representation, which can be used as a justification of the prediction, and it forces the prediction process itself to be interpretable in some way, since it causally relies on an intermediate semantic representation.

Evaluating explanations. The question of clearly evaluating the quality or usability of explanations remains an active problem. [START_REF] Selvaraju | Grad-cam: Visual explanations from deep networks via gradient-based localization[END_REF] described a human-centered experimental evaluation assessing the predictive capacity of the visual explanation. [START_REF] Montavon | Methods for interpreting and understanding deep neural networks[END_REF] proposed to quantify explanation quality by measuring two desirable features: continuity and selectivity of the input dimensions involved in the explanation representation. [START_REF] Zhang | Interpreting cnn knowledge via an explanatory graph[END_REF] and [START_REF] Bau | Network dissection: Quantifying interpretability of deep visual representations[END_REF] described geometric metrics to assess the quality of the visual explanation with respect to landmarks or objects in the image. [START_REF] Kindermans | The (un) reliability of saliency methods[END_REF] questioned the stability of saliency based visual explanations by showing that a simple constant shift may lead to uninterpretable representations. In our work, we take a dual approach: rather than evaluating the capacity of the explanation to be used as a surrogate or a justification of an ideal predictive process, we evaluate its quality as an ability of detecting bad behavior, i.e. detect potential wrong predictions.

Generating distinctive questions. If the generation of questions about text corpora has been extensively studied (see e.g., [START_REF] Serban | Generating factoid questions with recurrent neural networks: The 30m factoid questionanswer corpus[END_REF]), the generation of questions about images has driven less attention. We can, however, mention the interesting work of [START_REF] Li | Learning to disambiguate by asking discriminative questions[END_REF] where discriminative questions are produced to disambiguate pairs of images, or [START_REF] Mostafazadeh | Generating natural questions about an image[END_REF] which introduced the novel task (and dataset) of visual question generation. We can also mention the recent work of Das et al. [START_REF] Das | Learning cooperative visual dialog agents with deep reinforcement learning[END_REF] which bears similarity with our approach but differs in the separation between the question generator and semantic representation encoder, and is not applied to the same tasks. Our work builds on the observation made by [START_REF] Ganju | What's in a question: Using visual questions as a form of supervision[END_REF][START_REF] Zhu | Knowledge acquisition for visual question answering via iterative querying[END_REF] -questions that are asked about an image provide information regarding the image and can help to acquire relevant information about an image -and proposes to use automatically generated discriminative questions as cues for representing images.

Approach

This paper proposes a method allowing to turn raw images into rich semantic representations -a semantic bottleneck -which can be used alone (without using the image itself) to compare images or classify them. At the heart of this image encoder is a process for generating an ordered set of questions related to the image content, which are used, jointly with the answers to these questions, as an image substitute. Questions are generated sequentially, each question (as well as its answer) inducing the next questions to be asked. Such a set of questions/answers should semantically represent the visual information of images and be useful for disambiguating image representations in retrieval and classification task. Answering the question is done with a VQA model, used as an oracle, playing the role of a fine-grained information extractor. Furthermore, this sequence of Q/A is designed to be complementary to an image caption which is also automatically generated. We can use the analogy of human reasoning, starting with the image caption as a starting point and asking question to an oracle to get iteratively more information on the image. The proposed visual dialog allows to enrich image caption representations and leads to a stronger semantic representation. Finally, captions and visual dialogs are combined and turned into a compact representation that can be used easily to compare images (for retrieval task) or to infer class labels (classification tasks). Consequently, our model is composed of two main components: i) a discriminative visual question generator ii) an encoding block taking Q/A and captions as inputs and producing an image representation. These two blocks, trained end-to-end, rely on two oracles: i) an image caption generator which visually describes images with natural language sentences. ii) a visual question answering model capable of answering freefrom questions related to images. We call these last 2 parts of the model oracles as they are trained independently of the main tasks and used as external knowledge base.

Vector space embedding, encoders, decoders

The core objective of our approach is to generate semantic expressions in natural language (questions, answers or captions) that could represent images compactly and informatively. We define the various natural language elements as sequences of words from a fixed vocabulary of words and punctuation {w 0 , . . . , w nw }, where w 0 has the special meaning of marking the end of all phrases as a "full stop". The space of all possible sequences in natural language is denoted by P. Any caption (c), question (q) or answer (a) belongs to the same set P.

Most of learning based algorithms exploit vector space representations as inner states, or in the optimized criterion. A first issue is therefore to make possible the embedding of natural language expressions, and also images, into a vector space. For simplicity of design, we made all the necessary embeddings belong to a S-dimensional real valued vector space. Typically, to give an order of magnitude, we took S = 512 in our experiments. We therefore define semantic encoders as mappings from P to R S , and semantic decoders or generators as mappings from the vector space R S to P.

Image encoder

The first element to be encoded is the source image I ∈ I. The encoder (denoted as f I ) is a mapping f I : I → R S , provided by last FC layer (fc7) of a VGG-VeryDeep-19 network [START_REF] Simonyan | Very Deep Convolutional Networks for Large-Scale Image Recognition[END_REF] (pre-trained on Imagenet [START_REF] Russakovsky | Imagenet large scale visual recognition challenge[END_REF]) followed by a non-linear projection (fully connected layer + tanh non-linearity unit) reducing the dimensionality of the fc7 features (4096-d) to S. The parameters of the non-linear projection, denoted as w I , are the only parameters of this embedding that have to be learned, the parameters of the VGG-VeryDeep-19 being considered as fixed. We write f I (I; w I ) to make apparent the dependency on the parameters w I , when needed.

Natural language encoder This encoder maps any set of words and punctuation s ∈ P (captions, questions, answers) to the embedding space R S . We will use 3 different natural language encoders in the global algorithm, for captions, questions and answers, all sharing the same structure and the same weights. We hence refer to them using the same notation (f p ). The encoder uses a standard Long Short Term Memory network (LSTM) [START_REF] Hochreiter | Long short-term memory[END_REF]. Used as an encoder, the LSTM is simply a first order dynamic model: y t = LSTM p (y t-1 , p t ) where y t is the concatenation of the long-term cell state and the short-term memory, and p t is the current input at time t. Given a natural language sequence of words p = {p t } t=1:Tp , its encoding f p (p) is equal to the memory state y t after iterating on the LSTM T p times and receiving the word p t at each iteration. Denoting w p the set of weights of the LSTM model, the natural language embedding is therefore defined as: y Tp = f p (p; w p ) with the initial memory cell y 0 = 0.

In practice, instead of using words by their index in a large dictionary, we encode the words in a compact vector space, as in the word2vec framework [START_REF] Mikolov | Efficient estimation of word representations in vector space[END_REF]. We found it better since synonyms can have similar encodings. More precisely, this local encoding is realized as a linear mapping w w2vec , where w w2vec is a matrix of size n w2vec × n w and each original word is encoded as a one-hot vector of size n w , the size of the vocabulary. The size of the word embedding n w2vec was 200 in our experiments. This local word embedding simply substitutes w w2vec .p t to p t in the LSTM input.

Semantic decoder

The semantic decoder is responsible for taking an embedded vector s ∈ R S and producing a sequence of words in natural language belonging to P. It is denoted by f s . All the semantic decoders we exploit have the structure of an LSTM network. Several semantic decoders will be used for questions, answers and captions in the overall algorithm, but with distinct weights and different inputs. These LSTMs have an output predicting word indexes according to a softmax classification network: p t+1 = Softmax(y t ) which is re-injected as input of the LSTM at each iteration.

Formally, we can write the semantic decoder as a sequence of words generated by an underlying LSTM first order dynamic process with observations p t as y t = LSTM s (y t-1 , p t ). At time t the input receives the word generated at the previous state p t , and predicts the next word of the sentence p t+1 . When the word w 0 meaning "full stop" is generated at time T s , it ends the generation. The global decoding is therefore a sequence of words of length T s -1: f s (s; w) = {p t } t=1:Ts-1 with the initial state of the LSTM being the embedded vector to decode (y 0 = s) and the first input being null (p 0 = 0). The symbol w refers to the learned weights of the LSTM and the softmax weights , and is different for each type of textual data that will be generated (captions, questions and answers).

Captioning Model

The visual captioning part of the model is used as an external source of knowledge, and is learned in a separate phase. It takes an image (I) and produces a sentence in natural language describing the image. We used an approach inspired by the winner of the COCO-2015 Image Captioning challenge [START_REF] Vinyals | Show and tell: Lessons learned from the 2015 mscoco image captioning challenge[END_REF]. This approach, trainable end-to-end, combines a CNN image embedder with a LSTM-based Sentence Generator (Fig. 2(b)). More formally, it combines an image encoder and a semantic decoder, such are described previously, which can be written as: c(I) = f s (f I (I; w I ); w cg ) where w cg is the specific set of learned weights of the decoder. This caption model acts as an oracle, providing semantic information for the Visual Discriminative Question Selection component, and to the Semantic Representation Encoder.

Visual Question Answering Model

The VQA model is the second of the two components of our model used as oracles to provide additional information on images. Its role is to answer independent free-form questions about an image. It receives questions (Q) in natural language and an image (I) and provides answers in natural language (a(Q, I)). Our problem is slightly different from standard VQA because the VQA model now has to answer questions sequentially from a dialog. It means that the question Q k can be based on the answer of the previous questions Q k-1 and answers a(Q k-1 , I). We first present the formulation of a standard VQA and then show how to extend it so it can answer questions from a dialog.

Inspired by [START_REF] Antol | VQA: Visual Question Answering[END_REF], our VQA model combines two encoders and one decoder of those described previously (Fig. 2-a):

a(Q, I) = f s (f I (I; w Iqa ) f p (Q; w pqa ); w qa ) (1)
The fusion between image and question embeddings is done by an element wise product ( ) between the two embeddings, as proposed by [START_REF] Antol | VQA: Visual Question Answering[END_REF].

We now consider the case where questions are extracted from a dialog by extending Eq [START_REF] Das | Visual dialog[END_REF], where k represents the k-th step of the dialog. We introduce another term h k in the element-wise product to encode the history of the dialog as:

a k (Q k , I) = f s (f I (I; w Iqa ) f p (Q k ; w pqa ) h k ; w qa ) (2)
The history h k is simply computed as the mean of the previously asked questions/answers, and encoded using f p . This state integrates past questions and is expected to help the answering process. We tried other schemes to summarize history (concatenation, LSTM) without clear performance increase.

We prefer the VQA model to the Visual Dialog model [START_REF] Das | Visual dialog[END_REF], as this latter is optimized for the task of image guessing, while we want to fine-tune the question/answer sequence for different tasks (multi-label prediction and image retrieval).

Discriminative Question Generation

This part of the model is responsible for taking an image and a caption -which is considered as the basic semantic representation of the image -and produces a sequence of questions/answers that are complementary to the caption for a specific task (multilabel classification or retrieval).

The caption describing the image is generated using the captioning model presented in Section 3. This representation is then updated iteratively by asking and answering question, one by one, hence iteratively proposing a list of discriminative questions. Again, we use a LSTM network (Fig. 2-c), but instead of providing a word at each iteration as for f s (s; w) we inject a question/answer [q k , ãk ] pair encoded in a vector space from the natural language question/answer [Q k , A k ] using f p , with initial memory y 0 = f I (I) f p (c(I)) and initial input q0 = ã0 = 0: y k = LSTM q (y k-1 , [q k , ãk ])The actual questions are then decoded from the inner LSTM memory y k and fed to the VQA model to obtain the answer using Eq.( 2):

Q k+1 = f s (y k ; w sq ), and, A k+1 = a k+1 (Q k+1 , I)
Using this iterative process, we generate, for each image, a sequence of questionsanswers refining the initial caption: f q (I; w q ) = {Q k , A k } k=1:K where w q is the set of weights of the underlying LSTM network of the previous equation, and K is an arbitrary number of questions.

Semantic Representation Encoder

Our objective is to evaluate the feasibility of substituting a rich semantic representation to an image and achieve comparable performance than an image feature based approach, for several computer vision tasks. This representation has to be specifically generated to the target task, to be efficient.

Once again, many modern computer vision approaches relying on a learning phase require that data are given as fixed dimension vectors. The role of the module described here is to encode the rich semantic representation in R S to feed the retrieval or the multi-label classification task.

The encoder makes use of a LSTM network where the question/answer sequence {Q k , A k } k=1:K is used as input, y k = LSTM e (y k-1 , [q k , ãk ]) and the initial memory state y 0 is equal to the encoded caption f p (c(I); w p ) (Fig. 2(d)).

If w e is the set of weights from the underlying LSTM, the rich semantic representation y K is encoded as:

y K = f enc ([{Q k , A k } k=1:K , c(I)] ; w e ).

Training the model

The global training is divided in two phases. The first phase learns the two so-called oracles independently: image captioning and VQA. The second phase learns to generate the visual quiz, the image encoder and the semantic encoder jointly for a specific task, based on information provided by the two oracles.

The parameters of the VQA, namely w Iqa and w pqa for the encoders, and w qa (Eq. 2) are learned in a supervised way on the Visual Dialog dataset [START_REF] Das | Visual dialog[END_REF]. The learning criterion consists in comparing the answer words generated by the model with those of the ground truth for each element of the sequence of questions, and is measured by a cross entropy.

The captioning is also learned by comparing each word sequentially generated by the algorithm to a ground truth caption, and is also measured by a cross entropy loss.

The question/answer generator f q (I; w q ) and the semantic representation encoder f enc are learned jointly end to end. Each of the modules manages its own loss: for the question generator, the sequence of questions is compared to the ground truth of questions associated with each image using a cross entropy at each iteration. The semantic encoding, however, is specifically evaluated by a task-dependent loss: a cross entropy loss for each potential label for the multi-label classification task, a ranking loss for the image retrieval task. When the question generation model converges, only the task-dependent loss is kept in order to fine-tune the question selection part.

The retrieval loss is a bit more complex than the others (cross entropy). Basically, it is based on the assumption that ground truth captions are the most informative image representations and that any other representation should follow the same similarity ranking as captions provide. We follow the approach proposed in [START_REF] Gordo | Beyond instance-level image retrieval: Leveraging captions to learn a global visual representation for semantic retrieval[END_REF] to define the retrieval loss as a function of triplet data q, d + (positive pair) and d -(negative pair) to be L(q, d + , d -) = max(0, m -φ(q) T φ(d + ) + φ(q) T φ(d -)) where q and d + are expected to be more similar than q and d -, and φ is the representation function to be learned, i.e. the output of f enc , and m is a free coefficient playing the role of a margin. The reference similarity comparison is computed from ground truth captions using tf-idf representations, as suggested by [START_REF] Gordo | Beyond instance-level image retrieval: Leveraging captions to learn a global visual representation for semantic retrieval[END_REF].

Experiments

We validated the proposed method on 2 tasks: i) content based image retrieval (CBIR) based on semantics, where queries are related to the semantic content of the images -which is more general and harder than searching for visually similar images. We adopted the evaluation protocol proposed by Gordo et al. [START_REF] Gordo | Beyond instance-level image retrieval: Leveraging captions to learn a global visual representation for semantic retrieval[END_REF]. It uses captions as a proxy for semantic similarity and compares tf-idf representations of captions, and measures the performance as the normalized discounted cumulative gain (NDCG), which can be seen as a weighted mean average precision, the relevance of one item with respect to the query being the dot product between their tf-idf representations. ii) Multilabel image classification: each image can be assigned to different classes (labels), generally indicating the presence of the object type represented by the label. Per-class average precision and mAP are the performance metrics for this task.

Both series of experiments are done on the Visual Dialog dataset [START_REF] Das | Visual dialog[END_REF], relying on images of MS COCO [START_REF] Lin | Microsoft coco: Common objects in context[END_REF]. Each image is annotated with 1 caption and 1 dialog (10 questions and answers), for a total of 1.2M questions-answers. Ground truth Dialog has been made in order to retrieve a query image from a pool of candidate images. A dialog should visually describe a query image and be suitable for retrieval and classification tasks. We use the standard train split for learning and validation split for testing, as the test set is not publicly available.

Our approach has several hyper-parameters: the word embedding size, LST M state size, learning rate, m. They are obtained through cross-validation. In this procedure, 20% of training data is considered as validation set, allowing to choose the hyperparameters maximizing the NDCG/mean average precision on this so-obtained validation set. In practice, typical value for LST M state size (resp. embedding size) is 512 (resp. 200). The margin m is in the range [1.0-2.0]. Model parameters are initialized according to a centered Gaussian distribution (σ = 0.02). They are optimized with the Adam solver [START_REF] Kingma | Adam: A method for stochastic optimization[END_REF] with a cross-validated learning rate (typically of 10 -4 ), using minibatches of size 128. In order to avoid over-fitting, we use dropout [START_REF] Srivastava | Dropout: a simple way to prevent neural networks from overfitting[END_REF] for each layer (probability of a drop of 0.2 for the input layers and of 0.5 for the hidden layers). Both oracles (captioning and VQA) are fine-tuned on the tasks. Finally, while it would be interesting to average the performance on several runs, in order to evaluate the stability of the approach, this would be prohibitive in terms of computational time. In practice, we have observed that the performance is very stable and does not depend on initialization.

Experiments on Semantic Image Retrieval

We now evaluate our approach on semantic content-based retrieval, where the images sharing similar semantic content with an image query have to be returned by the system. As described before, the retrieval loss is optimized with triplets: an image query and two similar/dissimilar images. For triplet selection, we applied hard negative mining by sampling images according to the loss value (larger loss meaning higher probability to be selected). We found hard negative mining to be useful in our experiments.

Table 1 reports the NDCG performance for 3 values of R (R=k means that the top k images are considered for computing the NDCG), and the area under the curve (for R between 1 and 128) on 4 different models. The visual baseline exploits a similarity metric between image features extracted from the FC7 layer of a VGG19 network, which is learned on the train set using the same triplet approach as described in Section 3.6. I + [START_REF] Gordo | Beyond instance-level image retrieval: Leveraging captions to learn a global visual representation for semantic retrieval[END_REF] corresponds to the visual embedding noted (V, V) in [START_REF] Gordo | Beyond instance-level image retrieval: Leveraging captions to learn a global visual representation for semantic retrieval[END_REF]. {I, c(I)} + [START_REF] Gordo | Beyond instance-level image retrieval: Leveraging captions to learn a global visual representation for semantic retrieval[END_REF] is the joint visual and textual embedding (V+T, V+T) with the difference that we don't feed the ground truth captions but the generated one, for fair comparison. We observed that the area under the curve improves by +4.8% with our semantic bottleneck approach compared to the image feature similarity approach. We stress here that, unlike [START_REF] Gordo | Beyond instance-level image retrieval: Leveraging captions to learn a global visual representation for semantic retrieval[END_REF], we only exploit a semantic representation and not image features.

Empirical results of Table 2 show the usefulness of our semantic encoder. Indeed, with the same modalities (caption, questions and answers), tf -idf {c(I), {Q k , A k } 1:10 } performs 4.8% lower. Table 2 also shows the importance of adapting the VQA oracle to the task with +6.2% gain compared to a generic oracle not fine-tuned to the task.

Experiments on Multi-Label Classification

With the MS COCO [START_REF] Lin | Microsoft coco: Common objects in context[END_REF] dataset, each image is labeled with multi-object labels (80 object categories), representing the presence of broad concepts such as animal, vehicle, person, etc. in the image. For the baseline approach, we used image features provided by a VGG-VeryDeep-19 network [START_REF] Simonyan | Very Deep Convolutional Networks for Large-Scale Image Recognition[END_REF] pre-trained on ImageNet [START_REF] Russakovsky | Imagenet large scale visual recognition challenge[END_REF] with weights kept frozen up to the 4,096-dim top-layer hidden unit activations (fc7), and fed to a final softmax layer learned on the common training set.

Table 3 (bottom) reports the per-class mean average precision for the visual baseline and the various components of our model. Our fully semantic approach f enc (I) underperforms only by 5% the baseline. This is quite encouraging as in our setting the image is only encoded by a caption and 10 questions/answers. The main advantage of our model is that one can have access to the intermediate semantic representation for inspection, and may provide an explanation of the good or bad result (see section 4.3). Fig. 3 also reports the performance given by (i) generated caption c(I) only, (ii) Fig. 3: Combining captions and dialogs: query (top-left images), generated captions, task-specific dialogs, images retrieved using the caption (first rows) and those given by our model (second rows). Dialogs allowed to detect important complementary Fig. 4: Adapting dialogs to tasks: query (top-left images), generated captions, generic and task-specific dialogs, images retrieved using the caption and generic dialog (first rows), and those given by our model (second rows). questions/answers {Q k , A k } 1:10 only. These experiments shows that captions are more discriminative than questions/answers (+ 1,7%), at least given the way they are generated. We also report the performance obtained by combining our image representation with image features (denoted as {I, f enc (I)} ). This configuration gives the best performance (+8,2%) and outperforms the baseline (+3.1%). As a sanity check, we also computed the mAP when using ground truth annotations for both the captions and the VQA. We obtained a performance of 72.2%, meaning that with good oracles it's possible for our semantic bottleneck to obtain a performance better than with images (61.1%).

Semantic Bottleneck Analysis

This section aims at giving some insights on i) why the performance is improved by combining captions and dialogs and ii) why making the semantic bottleneck adapted to the task improves the performance.

Regarding the first point, we did a qualitative analysis of the outputs of the semantic retrieval task, by comparing the relevance of the first ranked images when adding the dialogs to the captions (see Figure 3). The Figure gives both the caption and the dialog automatically generated, as well as the images ranked first accordingly to the caption (first rows) and accordingly to our model combining the caption and the dialog. We marked in green the important complementary information added by the dialog. The dialog was able to detect drinks as an important feature of the image. task/words classes playing eating wearing doing color how many in/outdoor day/night classification 88% 19% 39% 29% 14% 42% 39% 42% 53% retrieval 78% 14% 28% 21% 16% 85% 81% 54% 79%

Table 4: Statistics of generated words after fine tuning the generators to the tasks Regarding the second point, we compared the quality of the retrieval with and without adapting the dialogs to the task. Figure 4 illustrates our observations by giving both captions and dialogs automatically generated, as well as the images ranked first accordingly to captions combined with generic dialogs (first rows) and with task adapted dialogs (second rows). We marked in red the questions/answers that we found not relevant to the query in the generic dialog and in green those that have been given by the task adapted dialog to emphasize the complementary information they bring. The dialog was able to identify vehicles as an important feature of the image. Fig. 5 illustrates the same type of caption correction by the dialog for the multi-label classification task.

Generated captions are, in general, brief and consistent with the images (see examples of Fig. 4, 5 and7). Because we chose a simple sampling strategy (in order to have a trade-off between computation and interpretation) a few captions are syntactically incorrect. We argue that this should not impact the performance, as the generated captions reflect the image content. We also observed that several questions are repeated. While question repetition is not as critical as it is for the actual dialog generation, it can be overcome if needed by encoding the question history (h k in Eq. ( 6)), for instance by explicitly penalizing repetitions in the LSTM criterion, or, by exploiting a reinforcement learning approach such as in [START_REF] Das | Learning cooperative visual dialog agents with deep reinforcement learning[END_REF].

Table 4 illustrates the effect of fine-tuning question generation by showing the percentage of time each word in the first row occurs in a dialog, across the two tasks ('classes' means any of the object class names). We observed that the generated dialogs of the classification task contain more verbs that can be associated to the presence of object classes (eating ⇒ food classes, playing ⇒ sport classes, wearing ⇒ clothes classes). Generated dialogs for the retrieval task contain more words characterizing the scene (in/outdoor, day/night) or referencing specific object features (color, how many).

We also made experiments showing how the semantic bottleneck can be modified manually to make image search more interactive. Fig. 6 shows an example where we changed 2 oracle answers (zebras becomes cows and their number is increased by one). The 2nd row depicts the impact of this modification. Right-hand side: the semantic representation is incorrect leading to the inference of erroneous labels. In such cases, the bottleneck representation can be used for debugging.

Evaluating Failure Predictions

The potential capacity of the semantic bottleneck to detect failure in the prediction process is illustrated by Fig. 7. Failure is detected when the representation contains incorrect semantic information -the caption or dialog are wrong -or insufficient information for further inference. We focus our evaluation on multi-label image classification, since a clear definition of failure in the case of content based image retrieval is complex, can be subjective (how decide if images are completely dissimilar from the request?) and task oriented (what are retrieved images used for?). We developed two evaluation protocols: one with humans in the loop, judging the semantic bottleneck capacity to predict consistent labels, and an automatic model optimized to predict success or failure for each class. We compare our approaches to a baseline based on score prediction thresholding. In order to evaluate the semantic bottleneck capacity, we first train our model for a multi-label classification task and extract the generated semantic representation (caption and dialog) and class prediction. Human based failure prediction study. For 1000 randomly chosen test images, users were instructed to evaluate the capacity of the semantic bottleneck to contain enough information to predict the correct classes. The image and the generated semantic representation are shown to the users, which can select for each of the 80 labels of MS-COCO 1 among 3 cases: i) false negative. The semantic representation missed the label (e.g. caption and dialog do not mention about the horse in the picture). ii) false positive. The semantic representation hallucinates the object (e.g. seeing a car in a kitchen scene). iii) correct. The algorithm has succeeded to predict the label, either its absence or its presence. Table 5 shows failure cases of the multi-label classification (614 false negative and 588 false positive). Human subjects were able to identify half of the failures (308/614 FN and 213/588 FP) with a precision of ≈ 60% (308/379 and 213/485).

Failure detection can also be evaluated through two other sets of experiments: Label rejection: suspicious labels are rejected, others are kept. Image rejection: when there is a suspicious label, the image is rejected. Table 6 shows both experiments, and reads as follows: classification performance is of 54.3% when evaluating on 100% of the test set. When user rejects 4% of the labels, the performance goes to 84.2%. When our rejection algorithm keeps 93% of the data, the performance improves to 79.8%, which is close to human performance. We see a strong improvement for both our methods. Failure prediction improves the average precision of 30% percent with 4% of deleted image in average for each class.

We also proposed two automatic algorithms for failure prediction. The first one, referenced as 'classifier' in Tables 5 and6, is based on an independent ternary linear classifier for each class with 3 possible outputs: correct, FN, FP. The input is the image I concatenated with the last hidden state of the semantic representation encoder [{Q k , A k } k=1:K , c(I)]. The ground truth is built by comparing the output from the multi-label classification and the true classes. The model is optimized using a cross entropy loss. It is less accurate (can detect ≈ 41% of false positive with ≈ 51% of precision) but has the advantage of reducing human effort. We also show in the last row of Table 6 the performance of a second algorithm consistng in thresholding the confidence score outputed by the multi-label classifier for each label, and tuned to reach the same rejection rate as the other failure detection algorithm. This confidence thresholding algorithm gives a smaller performance increase after rejection.

Conclusions

In this paper we have introduced a novel method for representing images with semantic information expressed in natural language. Our primary motivation was to question the possibility of introducing an intelligible bottleneck in the processing pipeline. We showed that by combining and adapting several state-of-the-art techniques, our approach is able to generate rich textual descriptions that can be substituted for images in two vision tasks: semantic content based image retrieval, and multi-label classification. We quantitatively evaluated the usage of this semantic bottleneck as a diagnosis tool to detect failure in the prediction process, which we think contributes to a clearer metric of explainability, a key concern to mature artificial intelligence.

Fig. 2 :

 2 Fig. 2: Functional diagrams of the various components of the global algorithm.

  2, and denoted c(I) ∈ P. This caption is encoded with f p (c(I); w p ) ∈ R S . Image and caption embeddings are then combined by an element-wise product f p (c(I)) f I (I) used as an initial encoded representation of the image.

Fig. 5 :

 5 Fig. 5: Left-hand side: incorrect caption corrected by the dialog. Right-hand side: objects missing from the captions discovered by asking relevant questions.

Fig. 7 :

 7 Fig.7: Predicting failure cases from the proposed semantic representation. Left-hand side: caption and Q/A are consistent but not rich enough to predict the 'giraffe' label. Right-hand side: the semantic representation is incorrect leading to the inference of erroneous labels. In such cases, the bottleneck representation can be used for debugging.

a man that is on a tennis court with a racquet q1: can you see his racquet? q2: what color is it? q3: can you see the ball? q4: is the ball yellow? q5: is he about to serve the ball? q6: is it day time? q7: is it indoors? q8: is the picture bright? q9: any other people? q10: can you see the net? a1: yes a2: not sure, but it 's a wilson racket a3: yes it 's in his hand a4: yes a5: maybe a6: i don't think so a7: can't tell a8: yes a9: no a10: no Generating semantic informations Semantic bottleneck Fusion Captioning Discriminative Questions Generation Visual Question Answering Semantic Image Encoder

Table 1 :

 1 NDCG on semantic retrieval. Performance/Area Under the Curve for different values of R.

	Method / R	8	32 128 AUC
	fi(I) + ML (baseline) 45.8 51.7 59.3 69.7
	I + [10]	47.6 55.9 62.3 72.7
	{I, c(I)} + [10]	57.0 58.5 63.3 75.1
	Our approach fenc(I) 59.3 61.7 67.1 79.9

Table 2 :

 2 Semantic retrieval. NDCG/AUC after removing some components of the model.

	Modality / R	8	32	128 AUC
	c(I)	55.1 56.3 62.4 73.6
	{Q k , A k }1:10 generic	41.8 50.4 57.7 65.7
	{Q k , A k }1:10 task adapted	45.8 55.7 60.0 71.9
	tf -idf {c(I), {Q k , A k }1:10} 54.9 57.2 63.4 75.1
	Our approach fenc(I)	59.3 61.7 67.1 79.9

Table 3 :

 3 Multi-label classification performance.

	Modality	mAP
	fi(I) (baseline) 61.1
	c(I)	51.6
	{Q k , A k }1:10 49.9
	fenc(I)	56.0
	{I, fenc(I)}	64.2

Predicted labels: car Missed labels: giraffe

  Fig. 6: Incrementally updating the representation.

	Semantic representation:
	a group of animals grazing on grass next to
	each other.
	what are the animals? zebras
	how many? 2
	are there other animals ? : no
	is this a zoo ? : probably
	is the grass long ? : no
	are they all grazing ? : yes all
	can you see any trees ? : yes
	any rocks ? : no
	is it sunny ? yes
	do you see any people ? no people
	-what are the animals? zebras
	-how many? 2
	+ what are the animals? there are horses
	and cows
	+ how many? 3
	Semantic representation:	Semantic representation:
	caption:	caption:
	two cars are crossing each other	a group of people riding surfboards on top of a wave
	dialog:
	what color are vehicles? blue and white	do you see any people? yes
	do you see any people? no	ihow many? 2
	is it day time? yes	is it day time? yes
	is it sunny? yes	is it sunny? yes
	how many car do you see? 2	what clothes? black swimsuits
	is it sunny? no	male or female? male
	do you see any bulding? no	is it day time? yes
	do you see any tree? yes	can yousee water? yes
	how many car do you see? 2	what clothes? black swimsuits
	is it day time? yes	is it day time? yes

Predicted labels: person, surfboard Missed labels: dog

Table 5 :

 5 Failure prediction statistics.

	false negative	false positive
	#true #predicted #true #predicted
	GT. 614	-	588	-
	users 308	379	213	485
	classifier 250	490	180	530

Table 6 :

 6 Multi-label classification.

	label	image
	mAP % mAP %
	no selection 54.3 100 54.3 100
	users 84.2 96 86.1 53
	classifier 79.8 93 81.7 49
	conf. thresh. 66.1 93 73.5 49