The Glass Box Approach: Verifying Contextual Adherence to Values Andrea Aler Tubella∗ and Virginia Dignum Umeå University {andrea.aler, virginia.dignum}@umu.se Abstract should be visible to the people who use, regulate, and are im- pacted by systems that employ those algorithms [Lepri et al., Artificial Intelligence (AI) applications are being 2018]. However, decisions made by predictive algorithms can used to predict and assess behaviour in multiple be opaque because of many factors, for instance IP protec- domains, such as criminal justice and consumer tion, which may not always be possible or desirable to elim- finance, which directly affect human well-being. inate [Ananny and Crawford, 2018]. Yet, accidents, misuse, However, if AI is to be deployed safely, then people disuse, and malicious use are all bound to happen. Since hu- need to understand how the system is interpreting man decisions can also be quite opaque, as are the decisions and whether it is adhering to the relevant moral val- made by corporations and organisations, mechanisms such as ues. Even though transparency is often seen as the audits, contracts, and monitoring are in place to regulate and requirement in this case, realistically it might not ensure attribution of accountability. In this paper, we propose always be possible or desirable, whereas the need a similar approach to monitor and verify artificial systems. to ensure that the system operates within set moral On the other hand, the current emphasis on the delivery bounds remains. of high-level statements on AI ethics may also bring with it In this paper, we present an approach to evaluate the the risk of implicitly setting the ‘moral background’ for con- moral bounds of an AI system based on the moni- versation about ethics and technology as being about abstract toring of its inputs and outputs. We place a ‘Glass principles [Greene et al., 2019]. The high-level values and Box’ around the system by mapping moral values principles are dependent on the socio-cultural context [Turiel, into contextual verifiable norms that constrain in- 2002]; they are often only implicit in deliberation processes. puts and outputs, in such a way that if these remain The shift from abstract to concrete therefore necessarily in- within the box we can guarantee that the system ad- volves careful consideration of the context. In this sense, heres to the value(s) in a specific context. The focus the subsumption of each value into functionalities will vary on inputs and outputs allows for the verification and from context to context the same way it can vary from sys- comparison of vastly different intelligent systems– tem to system. For example, consider the value fairness: it from deep neural networks to agent-based systems– can have different normative interpretations, e.g. equal ac- whereas by making the context explicit we expose cess to resources or equal opportunities, which can lead to the different perspectives and frameworks that are different actions. This decision may be informed by domain taken into account when subsuming moral values requirements and regulations, e.g.national law. Often, these into specific norms and functionalities. We present choices made by the designer of the system and the contexts a modal logic formalisation of the Glass Box ap- considered are hidden from the end-user, as well as for future proach which is domain-agnostic, implementable, developers and auditors: our aim is to make them explicit. and expandable. This paper presents the Glass Box approach [Aler Tubella et al., 2019] to evaluating and verifying the contextual ad- herence of an intelligent system to moral values. We place 1 Introduction a ‘Glass Box’ around the system by mapping abstract values Artificial Intelligence (AI) has the potential to greatly im- into explicit verifiable norms that constrain inputs and out- prove our autonomy and wellbeing, but to be able to inter- puts, in such a way that if these remain within the box we act with it effectively and safely, we need to be able to trust can guarantee that the system adheres to the value in a certain it. Trust in Artificial Intelligence (AI) is often linked to algo- context. The focus on inputs and outputs allows for the verifi- rithmic transparency [Theodorou et al., 2017]. This concept cation and comparison of vastly different intelligent systems; includes more than just ensuring algorithm visibility: the dif- from deep neural networks to agent-based systems. Further- ferent factors that influence the decisions made by algorithms more, we make context explicit, exposing the different per- spectives and frameworks that are taken into account when ∗ Contact Author subsuming moral values into specific norms and functional- ities. We present a modal logic formalisation of the Glass vation, by monitoring input and output streams only. We in- Box approach which is domain-agnostic, implementable, and sist on this feature as we do not always have access to the expandable. internals of the system, neither do we always have access to the designs of a system. 2 The Glass Box approach Designing the tests is naturally one of the most complex steps of this process: the main challenge is the computational The Glass Box approach [Aler Tubella et al., 2019], as de- tractability of these checks and their correspondence with the picted in Figure 1, consists of two phases which inform each low-level norms and their implementation. Different levels of other: interpretation and observation. It takes into account granularity in the norms pose different constraints for testing: the contextual interpretations of abstract principles by taking the cost of checking that the outcome for a certain input re- a Design for Values perspective [Van de Poel, 2013]. mains within certain bounds is very different than having to The interpretation stage is the explicit and structured pro- consider data of a whole database of inputs and outputs. Part cess of translating values into specific design requirements. It of the challenge is then determining the required granularity entails a translation from abstract values into concrete norms of the Glass Box and testing: a too rough approximation can comprehensive enough so that fulfilling the norm will be con- possibly cap many potentially compliant behaviours, whereas sidered as adhering to the value. Following a Design for Val- a too specific one may limit the adaptation of the AI system. ues approach, the shift from abstract to concrete necessar- From the observation stage we give feedback to the in- ily involves careful consideration of the context. For each terpretation stage: the testing informs us on which require- context we build an abstract-to-concrete hierarchy of norms ments are being fulfilled and which aren’t, which may prompt where the highest level is made-up of values and the lowest changes in the implementation or in the chosen requirements. level is composed of fine-grained concrete requirements for The observation stage is therefore fundamental both at a de- the intelligent system only related to its inputs and outputs. sign stage to verify that the intelligent system is functioning The intermediate levels are composed of progressively more as desired, and after deployment to explicitly fill in stakehold- abstract norms, and the connections between nodes on each ers on how the system is interpreting and whether it is verifi- level are contextual. When building an intelligent system, ably adhering to the relevant moral values without having to each requirement is distilled into functionalities implemented reveal its internal working. into the system in order to fulfill it. At the end of the inter- pretation stage we therefore have an explicit contextual hier- 3 Running example archy which can be used to provide high-level transparency for a deployed system: depending on which requirements are As an example, we will consider an intelligent system used being fulfilled, we can provide explanations for how and ex- to filter CVs as a recruitment tool. Note that the ethical val- actly in which context the system adheres to a value. Note ues, norms and functionalities highlighted in what follows are that the interpretation stage is also useful for the evaluation used purely as an example, and we do not claim that they of a system, as it provides grounding an justification for sys- are the most appropriate to adhere to, but rather are used to tem requirements, in terms of the norms and values they are demonstrate the approach. an interpretation. That is, it indicates a ‘for-the-sake-of’ rela- As a starting point, the designers of the system must iden- tion between requirements and values. tify the relevant ethical values that they wish to adhere to, The low-level requirements inform the observation stage depending on the legal framework, the company policies, the of our approach, as they indicate what must be verified and standards they are following, etc. They could, for example, checked. In the observation stage, the behaviour of the sys- settle on fairness and privacy. The next step is to unravel what tem is evaluated with respect to each value by studying its these values mean in terms of recruitment decisions from dif- compliance with the requirements identified in the previous ferent perspectives. stage. In [Vázquez-Salceda et al., 2007] two properties for In the case of fairness, they could consider several angles. norms to be enforceable are identified: (1) verifiability i.e., In the context of the Swedish law, for instance, fairness in the low-level norms must allow for being machine-verified recruitment means, amongst other things, non-discrimination given the time and resources needed, and (2) computational between male and female applicants. A design requirement tractability, i.e. whether the functionalities comply with the to guarantee fairness in this context can therefore be that the norms can be checked on any moment in a fast, low cost way. ratio of acceptances vs rejections has to be the same for both Note that this is a requirement for the observation stage and men and women (which can be calculated purely from the not necessarily for the design stage: some of the norms cho- inputs and outputs of the system). This requirement is then sen for the design stage might be easily implementable, but taken into account for implementation: for example, it can hard to monitor. In the observation stage, to each requirement be decided –rather ineffectively [Reuters, 2018]– to exclude identified in the interpretation stage, we assign one or sev- gender from the inputs of the system. In the same way, each eral tests to verify whether it is being fulfilled. Testing may legal requirement in terms of fairness will be translated into range through a variety of techniques, from simply checking specific requirements for the system. whether input/output verify a particular relationship, to com- Another perspective for fairness can be provided by com- plex methods such as statistical testing, formal verification or pany policy. It can for example be deemed that it is fair to model-checking. These must be performed without knowl- give preference to those applicants that are already working edge about the internal workings of the system under obser- for the company. In this case, the requirement for the sys- values interpretation observation norms input system output stage stage requirements Figure 1: The two stages of the Glass Box Approach: an Interpretation stage, where values are translated into design requirements, and an Observation stage, where we can observe and qualify the behaviour of the system. tem would be that applicants from within the company are exact connection between abstract and concrete concepts in prioritised. Functionality-wise, this can be translated into the each context. assignment of weights for each variable considered in the im- Several authors have proposed counts-as statements as a plementation. means to formalise contextual subsumption relations [Aldew- In the same way, other perspectives (e.g. European law, ereld et al., 2010]. With this relation, we can build logical HR recruitment guidelines) and other values (e.g. privacy, statements of the form: “X counts as Y in context c” [Searle, responsibility) will be taken into account and distilled into 1995; Jones and Sergot, 1995]. The semantics of counts-as is requirements and functionalities, providing a contextual hier- often interpreted in a classificatory light [Grossi et al., 2005], archy of values, norms, requirements and functionalities as a i.e. “A counts-as B in context c” is interpreted as “A is a result of the interpretation stage. subconcept of B in context c”. Thus, counts-as statements At this point, we proceed to the observation stage where can be understood as expressing classifications that hold in a testing procedures are devised for each of the functionali- certain context. At the same time, from a different seman- ties identified in the previous stage. To test whether the ra- tic viewpoint a counts-as operator can be used not only to tio of acceptances vs rejections is the same for both men and express classifications that happen to hold in a context, but women, we can for example check periodically after every to represent the classifications that define the context itself. 100 decisions whether the two ratios are within 5% of each Counts-as can also encode constitutive rules [Grossi et al., other. To test whether applicants from within the company are 2008], that is, the rules specifying the ontology that defines prioritised, we can take random samples of applicants from each context. outside and inside the company, and check that the accep- To formally represent the hierarchy of functionalities, re- tance rate for the latter group is higher. With the results of quirements, norms and values resulting from the interpreta- these tests in hand, we can reason about which values are be- tion stage of the Glass Box approach both outlooks are nec- ing verified (or not) in each context. essary. On one hand, contexts are defined by the connec- tions between more concrete lower level concepts to abstract values, precisely corresponding to the notion of constitutive 4 Formalising the Glass Box counts-as. On the other hand, once the contexts are estab- Since AI applications exist in a huge variety of areas, the lished, we aim to be able to reason about which combina- formalisation we present is based on predicate logic: it is tions of functionalities lead to the fulfillment of each norm domain-agnostic and can be adapted to any application. Cru- i.e. about the classifications holding in each context. Both cially, it is also implementable: the hierarchy of checks, views of counts-as admit compatible representations in modal norms and values can be encoded in logical programming logic as shown in [Grossi et al., 2008]: we will use the for- languages, and the complexity of the system in terms of the malism and semantics presented there, which we will briefly queries that we will pose to it is well within the reach of cur- introduce in this subsection. rent techniques. The logic we will consider is Cxtu,− . It is a multi- modal homeogeneous K45 [Blackburn et al., 2007], ex- 4.1 Counts-as tended with a universal context, negations of contexts, and The interpretation stage entails a translation from abstract nominals which denote the states in the semantics. values into concrete norms and requirements comprehensive Definition 1. Language Lu,− n is given by: a finite set P of enough so that fulfilling the norm will be considered as ad- propositional atoms p, an at most countable set N of nomi- hering to the value, with careful consideration of the context. nals denoted by s disjoint from P, and a finite non-empty set Normative systems are often described in deontic-based lan- K of n/2 atomic context indexes denoted by c including a guages, which allow for the representation of obligations, per- distinguished index u representing the universal context. The missions and prohibitions. With this approach, however, we set C of context indexes is given by the elements c of K and aim to not only describe the norms themselves, but also the their negations −c and its elements are denoted by i, j, . . . Further, the alphabet of Lu,− n contains the set of boolean A model M for the language Lu,− n is a pair (F, I) where connectives {¬, ∧, ∨, →} and the operators [ ] and h i. F is a C XT >,\ frame and I is a function I : P ∪ N → P(W ) The set of well-formed formulae of Lu,− n is given by the such that: following BNF: - For all nominals s ∈ N, there is a state w such that φ ::= ⊥ | p | s | ¬φ | φ1 ∧φ2 | φ1 ∨φ2 | φ1 → φ2 | [i]φ | hiiφ . I(s) = {w} (the interpretation of a nominal is a single Formulae in which no modal operator occurs are called ob- state) ; jective. - For all states w ∈ W there is a nominal s ∈ N such that Logic Cxtu,− is axiomatized via the following axioms and I(s) = {w} (every state has a name) . rules schemata: Definition 3. We define satisfaction for C XT>,\ frames as (P) all tautologies of propositional calculus follows: (Ki ) [i](φ1 → φ2 ) → ([i]φ1 → [i]φ2 ) M, w  s iff I(s) = {w} ij (4 ) [i]φ → [j][i]φ M, w  [c]φ iff ∀w0 ∈ Wc : M, w0  φ M, w  [−c]φ iff ∀w0 ∈ W \ Wc : M, w0  φ (5ij ) ¬[i]φ → [j]¬[i]φ where s ranges over nominals and c ranges on the context (Tu ) [u]φ → φ indexes in K. The boolean clauses and clauses for the dual (⊆ .ui) [u]φ → [i]φ modal operator are defined in a standard way and are omitted. (Least) huis With satisfaction defined in this way, the following theo- rem holds. (Most) hui(s ∧ φ) → [u](s → φ) Theorem 1. Logic Cxtu,− is sound and complete with re- (Covering) [c]φ ∧ [−c]φ → [u]φ spect to C XT>,\ frames. (Packing) h−cis → ¬hcis For a detailed proof, the interested reader is invited to refer (Dual) hiiφ ↔ ¬[i]¬φ to [Grossi et al., 2008]. The intuitive reading of the semantics is that W contains all the possible worlds (or states) consid- (Name) I F ` s → θ THEN ` θ, for s not occurring in θ ered in the model. For each context, Wc contains the states (MP) I F ` φ1 AND ` φ1 → φ2 THEN ` φ2 that are possible with the added restrictions of the context. Then, the set of possible worlds in the universal context coin- (Ni ) I F ` φ THEN ` [i]φ cides with all possible worlds, and the set of possible worlds for the negation of a context is the complement of its set of where i, j are metavariables for the elements of C, c denotes possible worlds. elements of the set of atomic context indexes K, u is the uni- The specific requirements on nominals capture the idea that versal context index, v ranges over nominals, and θ in rule each nominal is only satisfied in a single state, and that in ev- Name denotes a formula in which the nominal denoted by s ery state there is at least one nominal that is satisfied: nom- does not occur. inals can therefore simply be interpreted as names for each state. Logics with nominals are called hybrid logics [Blackburn Logic Cxtu,− provides us with the theoretical machinery et al., 2007]: they blur the lines between syntax and se- to be able to define both classificatory and constitutive counts- mantics, allowing us to express possible states (semantics) as operators, which we will use to build and explore hierar- through formulae (syntax). In this application, the presence chies of norms and values. of nominals allows for the definition of rules C OVERING and PACKING, fundamental to capture the concept of the comple- Definition 4. Let γ1 , γ2 be objective formulae. ment of a context. This becomes clearer when looking at the The classificatory counts-as is statement “γ1 counts as γ2 semantics: logic Cxtu,− enjoys a possible-world semantics in context c” is formalised in Cxtu,− by in terms of a particular class of multiframes. In this type of γ1 ⇒cl c γ2 := [c](γ1 → γ2 ) . semantics, we represent the states that are possible in each context, and consider an interpretation function I which as- Let Γ be a set of formulae, with γ1 → γ2 ∈ Γ. The consti- sociates to each propositional atom the set of states which tutive counts-as statement “γ1 counts as γ2 by constitution in make it true. the context c defined by Γ” is formalised in Cxtu,− by Definition 2. A C XT>,\ frame F is a structure γ1 ⇒co c,Γ γ2 := [c]Γ ∧ [−c]¬Γ ∧ ¬[u](γ1 → γ2 ) . hW, {Wi }i∈C i where: - There is a set K such that C = K ∪ {−c|c ∈ K} ; Note that for constitutive counts-as statements, both the name c of the context and the formulae Γ that define it have to - W is a finite set of states (possible worlds) ; be specified. This corresponds to the notion that constitutive - {Wi }i∈C is a family of subsets of W such that: there statements are those statemnts that we take as a definiton for exists a distinguished u ∈ C with Wu = W (there is a the context. If c is defined by Γ, an equivalent set of formu- universal context), and such that for every atomic con- lae Γ0 defines the same context c, but the constitutive state- text c ∈ K we have that W−c = Wu \ Wc . ments that hold in c, Γ0 are different than those that hold in c, Γ and correspond to the formulae of Γ0 . On the other hand, 4.3 Glass Box verification the classificatory statements holding in a context remain the The observation stage consists on checking that the lower- same no matter which set of equivalent formulae we choose level norms devised at the interpretation stage are in fact ad- as its definition, since they don’t define the context but rather hered to. Even if we restrict tests to constraints on the in- correspond to inferences that hold in it. puts and outputs of a system, they can encode a number of complex behaviours, from obliging the input or output to stay 4.2 Glass Box contexts within certain parameters, to imposing a certain relationship The end-result of the interpretation stage is a collection of between the input and output as a function of each other, to contexts, each given by a hierarchy of functionalities and comparing the inputs and outputs to other similar cases. Fur- norms fulfilling values. In this sense, contexts are defined by thermore, the tests need to be computationally checkable in the hierachy that holds in them. For this reason, we will for- a reasonable time. Once devised, these tests will be trans- mally define contexts through the set of implications that de- lated into propositional variables that will encode whether a fine it, which we can then implement via constitutive counts- test has failed or has passed. The results of these tests will as statements. be entered into the Glass Box by means of these variables, Furthermore, our aim is for contexts to be hierarchies of which we can then use to reason about whether a value has progressively more concrete terms. For this reason we need to been verified in a certain context. In this stage we therefore partition our language, given by the set of propositional atoms need to specify which tests are associated with each low-level we work with, into levels. Intuitively, given a hierarchy of norm in each context, and how. norms and values, we will assign a level to each propositional Definition 6. Let PO be a finite set of binary predicates. We atom it is composed of, corresponding to its position in the denote by pPO the elements of PO and by γ PO objective for- hierarchy in terms of concreteness. In addition, this allows mulae built on the propositional atoms of PO and ∧ and ∨, for the use of different vocabulary for each level. Contexts are given by then formed by defining how the propositional atoms of level i are related to atoms representing more abstract concepts at γ PO ::= pPO | ¬γ PO | γ1PO ∧ γ2PO | γ1PO ∨ γ2PO . level i − 1. Let c be an interpretation context on a partition P of set PI Definition 5. Let PI be a set of propositional atoms. given by a collection of subsets Fic ⊆ Pi , 0 ≤ i ≤ N and a Given a subset S ⊆ PI we denote by pS the elements of set of objective formulae Γc . S and by γ S the objective formulae built on the propositional A testing context ∆c for c is a collection of objective for- atoms of S, given by mulae of the form c γ S ::= pS | ¬γ S | γ1S ∧ γ2S | γ1S ∨ γ2S | γ1S → γ2S . γ PO → pFN −1 c A hierarchy is a partition P = {P0 , . . . , PN } of PI i.e. a such that for every pFN −1 ∈ FNc −1 there is at least one such collection of sets such that P0 t · · · t PN = PI . formula. An interpretation context c in a hierarchy P is given by: An observation box on PO associated to an interpretation box {c ∈ K} is given by a set {∆c |c ∈ K} where each ∆c is - a collection of subsets Fic ⊆ Pi , 0 ≤ i ≤ N ; a testing context for c. - a collection Γc of objective formulae of the form Notice that we don’t consider implication in the vocabulary c Fi+1 Fic of tests, since we will operate with concrete test results that γ →p return either “pass” or “fail”, and it theoretically makes no Fic semantic sense, given a specific outcome of the testing, to such that for every p , 0 ≤ i < N there is at least one such formula in Γc . reason in general about whether a certain test result implies another test result. When referring to an interpretation context, we will often abuse language and omit the family of subsets of the parti- 4.4 Reasoning inside the Glass Box tion included in its definition, as it is recoverable from Γc . Interpretation and observation boxes contain all the implica- Let P be a hierarchy on a set PI . An interpretation box is tions that define each context. We can now use counts-as a finite collection K of interpretation contexts in P. to build a framework that will allow us to reason about the With this characterisation, we represent the hierarchy of statements that hold in each context. Given an interpreta- concepts, from most abstract to most concrete, as a partition. tion box and an associated observation box, following Def- Elements of P0 correspond to values and elements of PN cor- inition 1 we will build a language on the propositional atoms respond to functionalities. Each interpretation context c is of P = PI t PO and the context labels in K. given by explicitly stating the relationships from more con- Additionally, we will need to specify a set N of nominals crete to more abstract concepts by specifying them in Γc . denoting every possible world that we consider in our model. Note that at the interpretation stage the lowest level of the Following the semantics of Definition 2, this set corresponds hierarchy defining the context is given by functionalities and to the set of states that are possible within the universal con- not by the verification procedures. These are designed and text. Since all the restrictions in our framework are contex- seamlessly incorporated to the Glass Box in the second stage tual and not universal, all the truth value assignments for the of the process, allowing for a modular approach. elements of P can hold in the universal context. Thus we will define N as a set of 2|P| elements, allowing for a one-to- Values one correspondence between elements of N and all possible worlds, i.e. truth value assignments, in the semantics. counts as Definition 7. A Glass Box is given by: - A set of propositional atoms P = PI t PO ; Norms - An interpretation box {c ∈ K} on a hierarchy P on PI ; - An associated Glass observation box {∆c |c ∈ K} on counts as PO ; counts as Requirements counts as - A set N of 2|P| elements. Given a Glass Box, we can build language Lu,− n on P, N and K 0 = K ∪ {u}, where u is an additional context name, Functionalities Tests following Definition 1. We consider logic Cxtu,− on this language. For each c ∈ K, let Υc = Γc ∪ ∆c . We define the Glass Figure 2: Formalisation of the Glass Box approach Box constitution as the conjunction of formulae ^ GB := (γ ⇒co posing are answerable in a reasonable time. Furthermore, it c,Υc p) . c∈K would be desirable to be able to solve the satisfiability prob- γ→p∈Υc lems we will pose with existing tools. Having encoded the Glass Box in a logical system (see Fig- To address both of these points, we will show that answer- ure 2), we can now reason about the statements that hold in ing questions of the form “does γ count as γ 0 in context c it. With the implementation in mind, we are particularly inter- in the Glass Box?” is equivalent to checking whether the im- ested in classificatory statements, which allow us to describe plication γ → γ 0 holds propositionally with the assumptions for example which combinations of norms count as satisfying of Υc . This is in fact a very intuitive result: the only con- a value in a context. The following definition illustrates some straints on a context c in the Glass Box are those set-up by its of the statements which we will want to hold in the Glass definition through Υc , and therefore any deduction in context Box. c only needs to consider these constraints. We therefore re- Definition 8. We say that an objective formula γ is incom- duce our question to a satisfiability problem in propositional patible with context c if logic with a finite number of propositions. In real-life ap- plications, our human-made vocabulary for norms and values ` GB → (γ ⇒cl c ⊥). should remain reasonably small. Additionally, the number of Incompatible formulae imply both a formula and its negation tests performed needs to remain relatively small as well for in context c, and therefore we wish to remove them from the computational reasons. Thus answering queries in our propo- set of formulae that verify a certain norm or value.c sitional language should easily remain well within the reach We say that a combination of functionalities γ FN counts as of SAT-solvers and answer set programming approaches. value pP0 in context c if it is not incompatible with c and Proposition 2. Let γ be an objective formula. We have that c ` GB → (γ FN ⇒cl P0 c p ). ` GB → [c]γ iff ` Υc → γ . We say that a test result γ PO verifies value pP0 in context c if it is not incompatible with c and Proof. Right to left is easy to see. It is given by the following deduction: ` GB → (γ PO ⇒cl P0 c p ). 1 (hypothesis) ` Υc → γ Formulae incompatible with a certain context correspond 2 (Nc ) ` [c](Υc → γ) to statements that do not make semantic sense: they may be 3 (Kc ), (MP) ` [c]Υc → [c]γ contradictory by themselves in this context, or lead to con- 4 (P), (MP) ` GB → [c]γ . tradictions within the context by for example, implying that both a value and its negation are satisfied. Left to right will be proven making use of the soundness Crucially for an effective implementation, given a certain of the logic with the semantics introduced in Definition 2. test result, we want to answer the question of whether this Consider the model M given by (hW, {Wi }i∈C i, I) where: result verifies a certain value in a given context. Thus we - W is the set of all possible valuations for P ; need to find a proof of GB → (γ PO ⇒cl P0 c p ), or to show - For each c ∈ K, Wc is the set of truth-value assignments that there is no such proof. We therefore need to address the for P in which Υc holds, and we set W −c := W \ Wc issue of the search-complexity of our system. and Wu := W ; (Multi)modal logics with a universal modality have an EXPTIME-complete K-satisfaction problem [Hemaspaan- - I : P → P(W ) assigns to each propositional atom the dra, 1996] and adding nominals maintains this bound [Are- set of states where its assignment is true ; ces, 2004]. For our system to be suitable for an implemen- - I : N → P(W ) is a one-to-one assignment between the tation, we need to show that the specific queries we will be elements of N and the elements of W . M is a model for the language Lu,− n . [Ananny and Crawford, 2018] M. Ananny and K. Crawford. If we assume that ` GB → [c]γ holds in logic Cxtu,− , Seeing without knowing: Limitations of the transparency then by soundness M  GB → [c]γ. Furthermore, it is easy ideal and its application to algorithmic accountability. New to see that M  GB, from the definition of M. Therefore Media & Society, 20(3):973–989, 2018. M  [c]γ holds. [Areces, 2004] C Areces. The computational complexity of Thus, by definition, ∀w0 ∈ Wc : M, w0  γ. Therefore, hybrid temporal logics. Logic Journal of IGPL, 8(5):653– in every truth-value assignment where Υc holds, also γ holds 679, 9 2004. i.e. Υc → γ holds propositionally. [Blackburn et al., 2007] P. Blackburn, J. van Benthem, and F. Wolter. Handbook of modal logic. Elsevier, 2007. 5 Discussion [Greene et al., 2019] D. Greene, A. Hoffmann, and L. Stark. The Glass Box approach is both an approach to software de- Better, nicer, clearer, fairer: A critical assessment of the velopment, a verification method and a source of high-level movement for ethical artificial intelligence and machine transparency for intelligent systems. It provides a modular learning. In Proceedings of the 52nd Hawaii International approach integrating verification with value-based design. Conference on System Sciences, 2019. Achieving trustworthy AI systems is a multifaceted com- [Grossi et al., 2005] D. Grossi, J-J.Ch. Meyer, and F.P.M. plex process, which requires both technical and socio-legal Dignum. Modal Logic Investigations in the Semantics of initiatives and solutions to ensure that we always align an in- Counts-as. Proceedings of ICAIL’05, 2005. telligent system’s goals with human values. Core values, as [Grossi et al., 2008] D. Grossi, J-J.Ch. Meyer, and F.P.M. well as the processes used for value elicitation, must be made Dignum. The many faces of counts-as: A formal analysis explicit and that all stakeholders are involved in this process. of constitutive rules. Journal of Applied Logic, 6(2):192– Furthermore, the methods used for the elicitation processes 217, 6 2008. and the decisions of who is involved in the value identifica- tion process are clearly identified and documented. Similarly, [Hemaspaandra, 1996] Edith Hemaspaandra. The Price of all design decisions and options must also be explicitly re- Universality. Notre Dame Journal of Formal Logic, 37(2), ported; linking system features to the social norms and val- 1996. ues that motivate or are affected by them. This should always [Jones and Sergot, 1995] A.J.I. Jones and M. Sergot. A For- be done in ways that provide inspection capabilities —and, mal Characterisation of Institutionalised Power. Logic hence, traceability— for code and data sources to ensure that Journal of IGPL, 4(3):427–443, 6 1995. data provenance is open and fair. [Lepri et al., 2018] B. Lepri, N. Oliver, E. Letouzé, A. Pent- The formalisation we presented in this paper allows for im- land, and P. Vinck. Fair, transparent, and accountable al- plementation while remaining highly versatile: this approach gorithmic decision-making processes. Philosophy & Tech- is not only useful for black boxes, as more information can nology, 31(4):611–627, 2018. easily be included in the hierarchy and the testing. Further- more, by including a universal context, we can easily include [Reuters, 2018] Reuters. Amazon ditched AI re- universal context-free statements that may hold in particular cruiting tool that favored men for technical applications. We aim to expand it into concrete implemen- jobs. The Guardian, Oct 2018. Available at tations in answer set programming. Beyond concrete imple- https://www.theguardian.com/technology/2018/oct/ mentations, further work will include studying the effects of 10/amazon-hiring-ai-gender-bias-recruiting-engine. this type of value-oriented transparency. [Searle, 1995] J Searle. The construction of social reality. Free Press, New York, 1995. Acknowledgements [Theodorou et al., 2017] A. Theodorou, R.H. Wortham, and This work was partially supported by the Wallenberg AI, Au- J.J. Bryson. Designing and implementing transparency for tonomous Systems and Software Program (WASP) funded by real time inspection of autonomous robots. Connection the Knut and Alice Wallenberg Foundation. Science, 29(3):230–241, 7 2017. References [Turiel, 2002] E. Turiel. The culture of morality: Social de- velopment, context, and conflict. Cambridge University [Aldewereld et al., 2010] H. Aldewereld, S. Álvarez- Press, 2002. Napagao, F.P.M. Dignum, and J. Vázquez-Salceda. Making Norms Concrete. In Proc. of 9th Int. Conf. on [Van de Poel, 2013] I. Van de Poel. Translating values into Autonomous Agents and Multiagent Systems (AAMAS design requirements. In Philosophy and engineering: Re- 2010), pages 807–814, Toronto, Canada, 2010. flections on practice, principles and process, pages 253– [Aler Tubella et al., 2019] A. Aler Tubella, A. Theodorou, 266. Springer, 2013. F.P.M. Dignum, and V. Dignum. Governance by Glass- [Vázquez-Salceda et al., 2007] J. Vázquez-Salceda, Box: Implementing Transparent Moral Bounds for AI H. Aldewereld, D. Grossi, and F.P.M. Dignum. From Behaviour. In Proceedings of the Twenty-Eighth Inter- human regulations to regulated software agents’ behavior. national Joint Conference on Artificial Intelligence (IJ- Artificial Intelligence and Law, 16(1):73–87, 2007. CAI’2019), 2019. To appear.