On Belief Change for Multi-Label Classifier Encodings

1 Introduction

Integrating learning and reasoning is one of the key challenges of AI today, and as such, it attracted much attention from several scientific communities, especially the neuralsymbolic computation one (NeSy) and the statistical relational learning and AI one (StarAI) [Raedt et al., 2020; Besold et al., 2017; d'Avila Garcez et al., 2019; Russell, 2015; Raedt et al., 2016]. The motivations for integrating learning and reasoning are numerous, giving rise to many research issues and associated methods for handling them.

One of these issues consists in leveraging knowledge to improve machine learning (ML) systems (especially, classifiers of various types) in terms of accuracy / data efficiency (see e.g., [Hu et al., 2016; Donadello et al., 2017; Xu et al., 2018; Xie et al., 2019; Chen et al., 2020]). For instance, a background theory T can be exploited during the learning phase used to generate the parameters of C; T can be viewed as a soft constraint that promotes solutions that are close to satisfying assignments, and this proves useful for generating better classifiers (see e.g., [Xie et al., 2019]).

However, such approaches do not guarantee that the learned classifier will classify every new instance in a way that is consistent with T. Furthermore, they are not applicable when the classifier has already been learned and the training set is not available any longer. In such a case, the learned classifier C itself must be modified to comply with T .

Noticeably, recent works have shown how ML classifiers C of various types can be encoded as Boolean circuits Σ (alias transparent or "white" boxes) (see e.g., [Narodytska et al., 2018; Shih et al., 2019; Shi et al., 2020]). In the following, we do not make any strong assumption on the nature of the classifier that is considered. C is supposed to be a discrete multi-label classifier: given a set X = {x1, · · · , xn} (its elements are Boolean features) and a set Y = {y1, · · · , ym}, that is disjoint with X (its elements are the labels, denoting classes / concepts), C is a mapping associating with each input instance (a vector x ∈ X of n Boolean values assigned to the variables of X) a vector y ∈ Y of m Boolean values assigned to the variables of Y . We also assume that a Boolean circuit Σ that encodes C is available. Σ is required to have the same input-output behaviour as C: for any pair (x, y) for which y = C(x), we have yj = 1 precisely when the output variable yj of the circuit Σ on the input x is set to 1. Such a circuit Σ can be viewed as a compact representation of the classes Y , as they are recognized by C.

Thanks to such encodings, the classification task w.r.t. C can be based on the associated circuit Σ, and achieved efficiently from this circuit. Indeed, it is well-known that the circuit value problem that consists of computing the output of a given Boolean circuit on a given input is complete for P under uniform AC0 reductions. 1 In terms of time complexity, this problem can be solved in linear time in the size of the circuit simply by a topological sort. Furthermore, beyond the classification task, both explanation and verification queries about C can be addressed via the corresponding classification circuit Σ [Darwiche and Hirth, 2020; Audemard et al., 2020].

Interestingly, it turns out that the problem of modifying C once learned so that it complies with T can also be delegated to the corresponding Boolean circuit Σ. This problem amounts to a belief change issue, a question studied for decades in the knowledge representation (KR) community. Here, T is supposed to be more reliable than Σ because of the noise that may pervade the data used to learn the classifier C. One is then interested in modifying Σ as few as possible in order to comply with T. What does "comply" mean depends of the nature of change one wants to deal with (e.g., belief revision, belief update). However, as we shall show soon, usual belief change operations (belief revision and belief update) that gave rise to an abundant literature in KR are not suited to the task at hand. A new change operation dedicated to multi-label classifier encodings is needed.

1 We assume the reader acquainted with basics of complexity theory (see e.g., [Papadimitriou, 1994] otherwise).

In the rest of the paper, the following research questions are considered:

• How to characterize multi-label classifier encodings Σ?
• What does it mean for a multi-label classifier encoding Σ to comply with some background knowledge T ?
• How to define belief change operators ⋆ that are suited to the task of making a multi-label classifier encoding Σ to comply with some background knowledge T ?
• How do ⋆ operators differ from standard belief change operators, i.e., belief revision and belief update operators?
• How hard is it to compute rectified classifications, i.e., classifications from Σ ⋆ T ?
• How hard is it to evaluate how much a multi-label classifier encoding Σ complies with a background theory T ?

Our contributions are as follows. A logical characterization of multi-label classifier encodings is pointed out. Several notions of compliance of multi-label classifier encodings with some background knowledge are presented. A new belief change operation, called rectification, that is specific to multi-label classifier encodings, is introduced. We characterize the family of rectification operators from an axiomatic perspective and exhibit some operators from this family. In addition, the standard belief change postulates that every rectification operator satisfies and those it does not are identified. Especially, we prove that the families of rectification operators and those of revision operators / update operators are disjoint. The problem of computing rectified classifications is shown hard in general, but tractable restrictions of this problem are provided. Similarly, we show that evaluating how much a multi-label classifier encoding complies with a background theory is computationally demanding in the general case, but easy when some requirements on the representations of Σ and T are satisfied.

The rest of the paper is organized as follows. After some formal preliminaries (Section 2), we present in Section 3 a condition, called XY -classification property, that characterizes multi-label classifier encodings; we present as well several notions of compliance suited to multi-label classifier encodings. In Section 4, the family of rectification operators is defined and its connections to other belief change operators are investigated. In Section 5, some computational issues about rectification and compliance are considered. Section 6 discusses additional related work. Finally, Section 7 concludes the paper and gives some perspectives for further research. Proofs are not reported in the paper for space reasons (a full-proof version of the paper is available at www.cril.fr/∼marquis/rectification.pdf).

2 Formal Preliminaries

Propositional logic. The propositional languages Lconsidered in this paper are defined over a finite and non-empty set PS of propositional variables (that includes but does not necessarily restrict to X ∪ Y ) and standard connectives. The elements of a propositional language L are called representations, and for any such representation Σ, we denote by Var(Σ) the subset of variables of PS occurring in Σ. As usual, atomic representations include propositional variables in PS , and Boolean constants in {⊤, ⊥}. A literal is a propositional variable, possibly negated, or a Boolean constant. Any propositional variable x is called a positive literal, and the negation of x, denoted ¬x or x, is called a negative literal. If ℓ is a literal x (resp. ¬x), then its complementary literal ∼ ℓ is ¬x (resp. x). For any subset X of PS, LX denotes the set of literals based on the variables of X. A term is a conjunction of literals, and a clause is a disjunction of literals. A canonical term over X is a consistent term into which every variable of X occurs (as such, or negated).

Given a set of variables V ⊆PS, an interpretation over V is a mapping ω from V to B = {0, 1}. When a total ordering < over PS is provided, interpretations can be represented by bit vectors from the set V . For instance, if V = {v1, v2} such that v1 < v2, then the mapping ω such that ω(v1) = 0 and ω(v2) = 1 can be represented by (0, 1). Propositional representations are interpreted in a classical way. For a representation Σ and an interpretation over any superset of V = Var(Σ), we use ω |= Σ to denote the fact that ω if a model of Σ according to the semantics of propositional logic. That is, assigning the variables of Σ to truth values as specified by ω makes Σ true. By [Σ] we denote the set of models of Σ over Var(Σ), and by ‖Σ‖ we denote the number of models of Σ over Var(Σ). In particular, Σ is inconsistent if ‖Σ‖ = 0, and consistent otherwise. Σ is said to be complete when it has a unique model. A representation Σ2 is a logical consequence of a representation Σ1 (denoted Σ1 |= Σ2) if Σ1 ∧ ¬Σ2 is inconsistent. Σ1 and Σ2 are logically equivalent (denoted Σ1 ≡ Σ2) if they are logical consequences of each other.

Given a representation Σ and a consistent term γ, the conditioning of Σ by γ is the representation obtained by replacing in Σ every occurrence of a variable v ∈ Var(γ) by ⊤ if v is a positive literal of γ and by ⊥ if ¬v is a negative literal of γ. When V is a subset of propositional variables from PS, Σ is said to be independent of V if there is a representation Φ logically equivalent to Σ such that Var(Φ) ∩ V = ∅. The forgetting of V in Σ, denoted ∃V.Σ, is (up to logical equivalence) the most general consequence of Σ that is independent of V . The projection of Σ onto V is the forgetting of V in Σ, where V denotes the set PS \V . Let us mention that ∃V.Σ can be computed as a propositional representation, thanks to the following inductive characterization:

• ∃∅.Σ ≡ Σ,
• ∃{v}.Σ ≡ (Σ | ¬v) ∨ (Σ | v),
• ∃(V ′ ∪ {v}).Σ ≡ ∃V ′ .(∃{v}.Σ).

Finally, we are interested in properties of propositional languages L that state the existence of polynomial-time algorithms for answering some queries (consistency testing CO, model counting CT) from representations in L, or for achieving some transformations over such representations (conditioning CD, forgetting FO, bounded conjunction ∧BC). See [Darwiche and Marquis, 2002] for details.

Propositional belief change. Belief revision consists in incorporating into an existing belief base ϕ (a propositional formula) a new piece of evidence µ (a propositional formula).

The following postulates have been pointed out for characterizing rational revision operators ◦ over a finite propositional language [Katsuno and Mendelzon, 1991b]:

Definition 1 (KM revision operator). A KM revision operator ◦ is a mapping associating with a change formula µ ∈ L and a formula ϕ ∈ L, a new base ϕ ◦ µ from L, such that for every formula µ, µ′ ∈ L, for any consistent formulae ϕ, ϕ′ ∈ L, it satisfies the following postulates:

• (R1) ϕ ◦ µ |= µ;
• (R2) If ϕ∧ µ is consistent, then ϕ ◦ µ ≡ ϕ∧ µ;
• (R3) If µ is consistent, then ϕ ◦ µ is consistent;
• (R4) If ϕ ≡ ϕ′ and µ ≡ µ′ , then ϕ ◦ µ ≡ ϕ′ ◦ µ′ ;
• (R5) (ϕ ◦ µ) ∧ µ′ |= ϕ ◦ (µ ∧ µ′ );
• (R6) If (ϕ ◦ µ) ∧ µ′ is consistent, then ϕ ◦ (µ ∧ µ′ ) |= (ϕ ◦ µ) ∧ µ′ .

Belief update mainly focuses on determining how a belief state (typically represented by a belief base ψ) should evolve in order to take into account a new piece of information µ reflecting an explicit evolution of the world.

The following postulates [Katsuno and Mendelzon, 1991a] have been pointed out for characterizing rational update operators ⋄:

Definition 2 (KM update operator). A KM update operator ⋄ is a mapping associating with a change formula µ ∈ L and a formula ψ ∈ L, a new base ψ⋄µ from L, such that for every formula µ, µ′ ∈ L, for any consistent formulae ψ, ψ′ ∈ L, it satisfies the following postulates:

• (U1) ψ ⋄ µ |= µ;
• (U2) If ψ |= µ then ψ ⋄ µ ≡ ψ;
• (U3) If ψ and µ are consistent then ψ ⋄ µ is consistent;
• (U4) If ψ ≡ ψ′ and µ′ ≡ µ′ then ψ ⋄ µ ≡ ψ′ ⋄ µ′ ;
• (U5) (ψ ⋄ µ) ∧ µ′ |= ψ ⋄ (µ ∧ µ′ );
• (U6) If ψ ⋄ µ |= µ′ and ψ ⋄ µ′ |= µ then ψ ⋄ µ ≡ ψ ⋄ µ′ ;
• (U7) If ψ is complete then (ψ⋄µ)∧(ψ⋄µ′ ) |= ψ⋄ (µ∨µ′ );
• (U8) (ψ ∨ ψ′ ) ⋄ µ is equivalent to (ψ ⋄ µ) ∨ (ψ′ ⋄ µ).

3 Classification and Compliance

Let us first make formal what "classifying" means when dealing with (general) propositional representations:

Definition 3 (classification). Let ϕ be a propositional representation in L over PS, and let X and Y be two disjoint subsets of PS. Let x ∈ X and y ∈ Y . ϕ is said to classify x (as y) if and only if the propositional representation ϕ(x), defined by ϕ(x) = ∃Y .(ϕ | x), has a unique model over Y , namely y. The set of instances x that are classified by ϕ is C(ϕ) = {x ∈ X | ∃y ∈ Y s.t. ϕ classifies x as y}.

Example 1. Let X = {x1, x2}, Y = {y}, and Z = {z}. Let ϕ = (x1 ∧ x2 ∧ y ∧ z) ∨ (x1 ∧ y). When x = (1, 1) we have ϕ(x) ≡ y. Thus ϕ classifies (1, 1) as (1). Similarly, ϕ classifies (0, 0) and (0, 1) as (0). On the other hand, when x = (1, 0) we have ϕ(x) ≡ ⊥, showing that ϕ does not classify (1, 0). We thus have C(ϕ) = {(1, 1), (0, 0), (0, 1)}.

For any propositional representation ϕ ∈ L and any x ∈ X, it can be observed that ϕ(x) ≡ (∃X ∪ Y .ϕ)(x). Intuitively, this equivalence indicates that the pieces of information in ϕ that do not only depend on X and Y are irrelevant to the classification task when X represents the features and Y the labels.

Now, in order to be considered as the encoding of a Boolean classifier C with features in X and labels in Y , a propositional representation Σ is expected to exhibit the XY - classification property:

Definition 4 (XY -classification property). A propositional representation Σ ∈ L has the XY -classification property when it is equivalent to an XY -classification circuit, i.e., a DAG D such that:

• the source nodes of D are associated with the variables in X and for every variable y of Y , there is a sink node of D that is associated with y;
• every node N in D, except the source nodes, is associated with a specific variable vN from Y ∪ Z; vN is the output of a gate, the inputs of it being the parents of N in D; this gate corresponds to an equivalence of the form vN ⇔ ϕN , where ϕN is a formula from L over the variables associated with the parents of N.

From a logical standpoint, an XY -classification circuit is viewed as the conjunction of all the equivalences associated with its nodes, thus a formula over X ∪ Y ∪ Z where X, Y, Z ⊆ PS .

Example 2. Let X = {x}, Y = {y}, and Z = {z}. Let Σ = (x ⇔ z) ∧ (y ⇔ z). Obviously enough, Σ has the XY -classification property.

When Σ has the XY -classification property, every variable v of Σ is definable in Σ in terms of X, meaning that there exists a formula ϕXv built upon variables of X, only, such that Σ |= v ⇔ ϕXv . Though necessary, this definability condition on the variables is not sufficient to characterize the XY - classification property. Indeed, any inconsistent representation Σ satisfies it, but an inconsistent Σ is not equivalent to any XY -classification circuit. Actually, the right concept required here is the one of unambiguous definability [Lang and Marquis, 2008]. Thus, beyond the definability condition, a propositional representation Σ that has the XY -classification property must be such that Σ | x is consistent for every x ∈ X (this is mandatory to ensure that every instance x is associated with at least one y ∈ Y , the definability condition guaranteeing the unicity of y).

Obviously enough, every propositional representation Σ that has the XY -classification property is such that C(Σ) = X: Σ must classify every instance. Note that the converse implication does not hold: take X = {x}, Y = {y}, and Z = {z}, and ϕ = (x ∧ y ∧ z) ∨ (x ∧ y). ϕ is such that C(ϕ) = X but ϕ does not have the XY -classification property (z is not defined in ϕ in terms of X).

Assuming that a background theory T is available, it is expected that Σ complies with T. Indeed, T contains pieces of belief that can be supposed more certain than those implicitly recorded in Σ since the latter ones have been learned from data that can be noisy. Accordingly, the primacy is given to T , and when Σ does not comply with T , Σ should be (minimally) modified so as to become compliant with T . Depending on what "compliant" means, several belief change operations can be considered.

Thus, in the belief revision case, Σ complies with T precisely when Σ is consistent with T . When this is the case, the change operation that is expected simply consists in conjoining Σ with T, so as to retain all the models of T which are also models of Σ. This is imposed by the rationality postulate (R2) for revision. In the remaining case, some models of T are selected, the selection process being based on Σ.

It turns out that the notion of compliance and the corresponding change operation required for incorporating a background theory T into a XY -classification circuit Σ are not the ones considered in belief revision:

Example 3. Let X = {x1, x2} and Y = {y}. Let Σ = (x1 ∧x2) ⇔ y, T = (x1 ∧x2) ⇔ y. Σ∧T is consistent (it is equivalent to x1 ∧y), thus following (R2), a rational revision of Σ by T should be equivalent to x1 ∧ y. However, x1 ∧ y is not equivalent to any XY -classification circuit.

The problem is that the selection process achieved by the revision operation is performed modelwise. Indeed, the representation theorem for belief revision given in [Katsuno and Mendelzon, 1991b] indicates that the models of Σ revised by T are among the models of T that are minimal w.r.t. a faithful ordering associated with Σ. If one wants to guarantee that the resulting representation is equivalent to a XY -classification circuit, the selection process must satisfy a constraint that concerns the whole set of resulting models (and not each model taken individually). This constraint is given by the XY -classification property stating that, after the change, for every x ∈ X there is a unique model extending x (this model also extends a unique y ∈ Y ). Noticeably, instead of the standard notion of revision, considering refined revision operators as proposed in [Creignou et al., 2014] for handling propositional fragments would not be enough to guarantee that Σ once revised by T has the XY -classification property.

Accordingly, the notion of compliance considered in belief revision (i.e., recovering consistency) is not convenient here. Several notions of compliance of an XY -classification circuit with a background theory T can be considered instead:

Definition 5 (compliances). Let Σ, T be two propositional representations from L s.t. Σ has the XY -classification property. Let x ∈ X.

• Σ is classification-compliant with T on x iff Σ(x) ≡ T (x).
• Σ is knowledge-compliant with T on x iff Σ(x) |= T(x).
• Σ is fact-compliant with T on x iff Σ(x) |= F(T, x)

It can be easily checked that for every T and every x, we have T(x) |= F(T, x). In addition, for every x that is classified by T , we have T (x) ≡ F (T, x).

Clearly enough, when Σ is classification-compliant with T on x, we have x ∈ C(T): Σ and T classify x in the same way. Knowledge compliance is less demanding since it requires only that the classification achieved by C (thus, Σ) on x coheres with what T "says" about the classes of x. Especially, knowledge compliance does not ask T to classify x. Fact compliance asks even less since it does not focus on all what T implies about the classes of x, but only on the class membership (or non-membership) relations that can be deduced from T . Thus, we have the following proposition:

Proposition 1. Let Σ, T be two propositional representations from L s.t. Σ has the XY -classification property. Let x ∈ X.

• If Σ is classification-compliant with T on x, then Σ is knowledge-compliant with T on x.
• If Σ is knowledge-compliant with T on x, then Σ is factcompliant with T on x.

The converse implications do not hold:

Example 4. Let X = {x1, x2} and Y = {y1, y2}. Let Σ = (x1 ⇔ y1) ∧ (x2 ⇔ y2) and T = ((x1 ∧ x2) ⇒ (y1 ∧ y2)) ∧ (x1 ⇒ (y1 ∨ y2)) ∧ (x1 ⇒ (y1 ∨ y2)). Let x1 = (1, 1), x2 = (1, 0), x3 = (0, 1). We have:

• T(x1) ≡ y1 ∧ y2: Σ is classification-compliant with T on x1 since Σ(x1) ≡ y1 ∧ y2.
• T(x2) ≡ y1 ∨ y2: Σ is knowledge-compliant with T on x2, but not classification-compliant with T on x2, since Σ(x2) ≡ y1 ∧ y2.
• F(T, x3) is valid, therefore Σ is fact-compliant with T on x3 but it is not knowledge-compliant with T on x3, given that T (x3) ≡ y1 ∨ y2 and Σ(x3) ≡ y1 ∧ y2.

Observe that when T is inconsistent with x, any representation Σ that has the XY -classification property is factcompliant with T on x because F(T, x) is valid. However, since T (x) is inconsistent, Σ is neither knowledge-compliant nor classification-compliant with T on x.

4 Rectifying a Classifier Representation

Whatever the notion of compliance under consideration, if Σ is not compliant with T on a given x, then Σ must be "rectified" so as to make it compliant with T on x since primacy is given to T. Making it more formal calls for a notion of rectification operator:

Definition 6 (rectification operator). A rectification operator ⋆ is a mapping associating with two propositional representations T and Σ where Σ has the XY -classification property, a propositional representation Σ ⋆ T , called a rectified representation, such that:

(RE1) Σ ⋆ T has the XY -classification property;

• (RE2) If Σ is fact-compliant with T on x ∈X, then (Σ ⋆ T )(x) ≡ Σ(x);
• (RE3) For any x ∈X, (Σ ⋆ T)(x) |= F(T, x);

(RE4) If T is inconsistent, then Σ ⋆ T ≡ Σ;

The admissible mappings ⋆ are required to satisfy a number of postulates, namely the rectification postulates (RE1-RE6). (RE1) states a key condition, asking any rectification operation to preserve the XY -classification property. It is the most demanding postulate since it requires that for every x ∈ X, Σ⋆T is consistent with x and furthermore that (Σ⋆T )∧x has a single model. (RE2), (RE3), and (RE4) capture the principle of minimal change and the primacy of T over Σ. Thus, (RE2) states that there is no reason to rectify the classification of any x as achieved by Σ whenever Σ is fact-compliant with T on x when Σ is classification-compliant with T on x, as shown by Proposition 1. In the remaining case, (RE3) constrains the way the rectified representation Σ ⋆ T classifies x by requiring that the class membership relationships imposed by T on x are satisfied. Indeed, (RE3) ensures that Σ ⋆ T is fact-compliant with T on every x. For those x that are classified by T , (RE3) ensures that Σ ⋆ T is knowledge-compliant with T on x; more than that, (RE1) and (RE3) together guarantee that Σ⋆T is classification-compliant with T on every x that is classified by T . Note that F (T, x) is valid whenever T is inconsistent so that (RE3) is trivially satisfied in this case. (RE4) deals with the case when T is inconsistent; in such a situation, a minimal change of Σ consists in not modifying it at all. (RE5) is a (rather standard) syntax-independence postulate (it has the same form as the ones of (R4) and (U4)). Finally, (RE6) states that the result of rectifying Σ by T must not depend on the variables not directly involved in the classification task, i.e., those variables outside X ∪ Y .

At that stage, it is important is to check that one can find operators ⋆ that do satisfy (RE1-RE6):

Definition 7 (⋆D, ⋆s ).

• Let ◦D denote Dalal revision operator [Dalal, 1988], such that for any ϕ, α, the models of ϕ ◦D α consist of the models of α which are as close as possible to ϕ w.r.t. Hamming distance. Let ⋆D be the mapping associating with a background formula T and a propositional representation Σ that has the XY -classification property, a propositional representation Σ ⋆D T such that

where for any x ∈ X, (Σ⋆DT )(x) = Σ(x)◦DF (T, x).

• Let s be any selection function, i.e., a mapping associating with a consistent propositional representation α over Y a canonical term s(α) representing a model of α. We assume that s is syntax-independent, meaning that s(α) = s(α′ ) whenever α ≡ α′ .

Let ⋆s be the mapping associating with a background theory T and a propositional representation Σ that has the XY -classification property, a propositional representation Σ ⋆s T such that

• (Σ ⋆s T)(x) = Σ(x) if Σ is fact-compliant with T

Example 5. Let us consider again the sets of variables X = {x1, x2} and Y = {y1, y2}, and the formula Σ = (x1 ⇔ y1) ∧ (x2 ⇔ y2) given at Example 4, and let us take now T = (x1 ∧ x2 ∧ y1 ∧ y2) ∨ (x1 ∧ y1). We have T ((0, 1)) ≡ F(T, (0, 1)) ≡ y1. Since Σ((0, 1)) ≡ y1 ∧ y2, Σ is not factcompliant with T on (0, 1). We have (Σ ⋆D T)((0, 1)) ≡ (y1 ∧ y2) ◦D y1 ≡ y1 ∧ y2. If for any x, s(T(x)) is given as the minimal element of T(x) w.r.t. the ordering < over the interpretations over Y such that 00 < 01 < 10 < 11, we have (Σ ⋆s T)((0, 1)) ≡ s(y1) ≡ y1 ∧ y2. Hence, we have Σ ⋆s T ̸≡ Σ ⋆D T.

Observe that ⋆s is well-defined since for any x such that T(x) is inconsistent, Σ is fact-compliant with T on x.

Proposition 2. ⋆D and every ⋆s are rectification operators.

Taking advantage of ⋆D for rectifying Σ so as to account for T simply consists, for every x ∈ X, in revising Σ(x) by F(T, x) using Dalal revision operator. Since Σ(x) and F(T, x) are terms over Y , the revision process enforces every literal of F(T, x) to hold in (Σ ⋆D T)(x) while keeping unchanged every other literal of Σ(x) (thus, ensuring that (Σ ⋆D T)(x) has a single model over Y ). As expected, the revision step using ⋆D has no effect on Σ(x) whenever Σ is fact-compliant with T on x.

A similar conclusion can be drawn when considering any ⋆s instead of ⋆D. However, for those x such that Σ is not fact-compliant with T on x, when ⋆s is considered, a more severe revision of Σ(x) is achieved; indeed, s(T(x)) implies F(T, x) but the converse does not hold in general. Since s(T(x)) |= T(x) holds, it is guaranteed that Σ ⋆s T is knowledge-compliant with T on such x (note that this property of knowledge-compliance is not guaranteed for those x when ⋆D is used instead). Clearly, the choice of a ⋆s operator comes at the expense of specifying a selection function s, but in many cases one can take advantage of additional information to define s. For instance, one can select a model of T(x) which is implied by a maximal number of models of Σ (i.e., a most frequent class assignment).

Note that when dealing with mono-label classification problems, ⋆D and ⋆s coincide, whatever s:

As explained previously, the (RE3) postulate asks the rectified representation Σ⋆ T to satisfy the less demanding form of compliance, namely fact-compliance. Two strengthenings of the (RE3) postulate, suited respectively to knowledgecompliance and classification-compliance, could have been envisioned instead:

(RE3') For any x ∈X, (Σ ⋆ T)(x) |= T(x);

(RE3") For any x ∈ X, (Σ ⋆ T)(x) |= T(x), and for any x ∈ X that is classified by T , we have

(RE3') strengthens (RE3) in order to ensure that the rectified representation Σ ⋆ T is knowledge-compliant with T on every x, and (RE3") strengthens (RE3') in order to ensure in addition that the rectified representation Σ ⋆ T is classification-compliant with T on every x that is classified by T. It can be observed that stating (RE3") as ∀x ∈ X, (Σ ⋆ T)(x) ≡ T(x) would not be appropriate because this statement conflicts with (RE1) given that T is not required to satisfy the XY -classification property. Since the condition stating that for any x ∈ X that is classified by T, (Σ ⋆ T )(x) ≡ T (x) holds is already satisfied by the rectification operators in the sense of Definition 6, (RE3") actually is equivalent to (RE3') in presence of the other postulates. Thus considering (RE3") in addition to (RE1-RE6) and (RE3') would be useless.

Finally, (RE3') has not been retained because this postulate is incompatible with (RE2). Indeed, it can be the case that Σ(x) |= F(T, x) while Σ(x) ̸|= T(x). Take for instance X = {x}, Y = {y1, y2}, Σ = (x ⇔ y1) ∧ (x ⇔ y2), and T = x ⇔ (y1 ∨ y2). For x = (1), we have Σ(x) ≡ y1 ∧ y2, F(T, x) ≡ ⊤, and T(x) ≡ y1 ∨ y2. Thus, no rectification operator can satisfy (RE3').

Nevertheless, it can be noted that (RE3') is compatible with the following weakening (RE2') of (RE2):

Accordingly, we can define a family of operators ∗s (similar to ⋆s ) as follows. Let s be any selection function, as in Definition 7. We define the ∗s operator by:

where for any x ∈ X,

• (Σ ∗s T)(x) = Σ(x) if Σ is knowledge-compliant with T on x,
• (Σ ∗s T)(x) = s(T(x)) otherwise.

It can be shown that ∗s operators satisfy (RE2') and (RE3') (for space reasons, we refrain from presenting ∗s operators in more detail in this paper).

Finally, in order to figure out in a more accurate way how rectification operators differ from other change operators, we have evaluated the compatibility of the rectification postulates with those characterizing belief revision operators and belief update operators. The main results are:

Proposition 4. Every rectification operator satisfies (R3) and (R4), but none of them satisfies (R1), (R2), (R5), or (R6).

Proposition 5. Every rectification operator satisfies (U2), (U3), (U4), (U7), and (U8), but none of them satisfies (U1) or (U5). Some rectification operator satisfies (U6) but not all of them.

The main consequence of Proposition 4 and Proposition 5 is that the family of rectification operators and the families of KM revision (resp. KM update) operators are disjoint. Accordingly, our results clearly show that, from an axiomatic point of view, rectification is a change operation that is clearly distinct from rational revision or update.

5 Some Computational Issues

Computing rectified classifications. We are first interested in the complexity of determining the class of any input instance x when classified by the rectified classification circuit Σ ⋆ T . Formally:

Definition 8 (classifying from a rectified classifier encoding). CLASSIFICATION(⋆) is the following decision problem:

• Input: Two propositional representations Σ, T s.t. Σ has the XY -classification property, x ∈ X, ℓ ∈ LY .
• Output: Does (Σ ⋆ T)(x) |= ℓ hold?

When Σ is a CNF formula obtained by applying Tseitin transformation [Tseitin, 1968] to a XY -classification circuit, the class assignment Σ(x) associated with a given x can be computed in time linear in |Σ| (one can compute the value of every variable of Σ | x using unit propagation since this mimicks the way the values of the outputs of the gates are computed in a XY -classification circuit each time the values of the inputs are provided). Thus, it is interesting to determine whether such a tractability result for classification still holds when Σ ⋆ T is considered instead of Σ. Unfortunately this is not the case, whatever the rectification operator ⋆:

Proposition 6. For every rectification operator ⋆, CLASSIFICATION(⋆) is both NP-hard and coNP-hard even if Σ is a CNF formula obtained by applying Tseitin transformation to a XY -classification circuit, |Σ| is bounded by a constant, and T is a CNF formula.

Interestingly, classifying from a rectified classifier encoding is computationally easier for some rectification operators, provided that T is represented in a propositional language that offers some specific properties:

Proposition 7. Let x ∈ X be an instance to be classified by a classifier C encoded by Σ, y ∈ Y be the corresponding prediction (i.e., y = C(x) = Σ(x)), and T be be a propositional representation from a language that supports in polynomial time CD, FO, and CO. Then:

• (Σ ⋆D T)(x) can be computed in time polynomial in n + m + |T |.
• If s is any selection function that runs in time polynomial in the size of its input, then (Σ⋆s T)(x) can be computed in time polynomial in n+m+ |T|.

What makes the last proposition useful is the existence of succinct languages L supporting CD, FO, and CO, especially the DNNF language [Darwiche, 2001], and the existence of translators (alias compilers) for turning representations from more standard languages (in particular the CNF one) into DNNF representations.

Measuring how much a classifier complies with a background theory. In order to verify a classifier C via its encoding Σ, it is useful to evaluate the proportion of x ∈ X for which Σ complies with the background theory T on x. If this proportion is high, there is no problem since one expects a high level of compatibility between C and T . Otherwise, it may prove reasonable to learn C again using another training set, or to clean the training set used before a second training round. One step further, it can prove useful to determine such a proportion when the instances under consideration are compatible with a given feature assignment x or x with x ∈ X, or more generally with a combination x′ of such feature assignments. For instance, when the proportion is lower under assignment x than in the case no feature assignment has been considered, this may reflect incorrect values for x in the training set. To make it more formal, let us consider the following definition:

Definition 9 (knowledge compliance degree). Given two propositional representations Σ and T such that Σ has the XY -classification property, and x′ ∈ X′ with X′ ⊆ X, the knowledge compliance degree kcd(Σ, T, x′ ) of Σ with T given x′ is given by kcd(Σ, T, x′ ) =

Unsurprisingly, computing the knowledge compliance degree of Σ with T given x′ is computationally demanding:

Proposition 8. Computing kcd(Σ, T, x′ ) is #P-hard, even under the restriction when T is a monotone 2-CNF formula.

When additional assumptions on the representations of Σ and T are made, computing kcd(Σ, T, x′ ) becomes tractable: Proposition 9. If Σ and T belong to a language L that supports ∧BC, CD, and CT and T is such that Var(T) ⊆ X ∪ Y , then for any x′ , kcd(Σ, T, x′ ) can be computed in time polynomial in the input size.

Again, what makes the last proposition valuable is the existence of succinct representation languages L supporting ∧BC, CD, and CT, especially the languages of (structured) d-DNNF respecting a fixed vtree [Pipatsrisawat and Darwiche, 2008; Pipatsrisawat and Darwiche, 2010] and its subsets, SDD [Darwiche, 2011] and OBDD [Bryant, 1986], as well as the existence of compilers targeting those languages.

6 Other RelatedWork

Theory revision is a research question that has stimulated much effort in the ML community since the 90's (see e.g., [Wrobel, 1994]). In a nutshell, theory revision is the problem of correcting a given, roughly correct, theory Σ. Typically, Σ represents pieces of knowledge, provided by an expert, and it comes with a set of labelled instances x (examples and counter-examples of a concept). Most of the time, Σ is a logical representation, based on atoms describing features and concepts (or classes), and x is classified by Σ as an element of class C (respresented by an atom) whenever C can be deduced from Σ and x [Ourston and Mooney, 1990]. When an instance is not recognized as it should be, Σ must be minimally modified so as to classify all instances correctly, and this is the purpose of theory revision. A related issue is to minimize the number of syntactic revision operations (such as the addition or deletion of literals) needed to obtain the target theory from Σ [Goldsmith et al., 2002].

Rectification and theory revision are connected by some common goal (correcting misclassifications). Furthermore, like rectification, theory revision does not amount to belief revision: revising a theory by an example using a belief revision operator would enforce the instance to hold in the revised theory, which is not the same as ensuring the revised theory to classify the instance in the right way. However, rectification and theory revision are based on different inputs (in the rectification setting, change formulae do not reduce to instances but can be complex representations linking features and classes) and assumptions (in theory revision, the theory considered at start is not required to classify every instance, even if it is in an incorrect way, and this property is not expected to be maintained) and for those reasons, rectification operators differ from theory revision operators (especially, the former ones are typically syntax-dependent while the latter ones are not).

7 Conclusion

We have presented a new belief change operation, called rectification, that is specific to multi-label classifier encodings Σ. Such an operation aims to minimally modify such an encoding Σ so as to make it to comply with some background theory T, that is considered more reliable than Σ. Several notions of compliance have been presented. Focusing mainly on fact-compliance, we have characterized the family of rectification operators ⋆ from an axiomatic perspective and have exhibited some operators from this family. We have identified the standard revision and/or update postulates that every rectification operator satisfies and those it does not. We have also identified complexity bounds for the problems of computing rectified classifications and of measuring the knowledge compliance of a given Σ with a given T . Though both problems are computationally hard, we have found tractable restrictions of them based on the DNNF language and its subsets. Accordingly, those languages appear as valuable for representing classifier encodings given that they are already known as useful for ensuring the tractability of a number of XAI queries [Audemard et al., 2020].

This work is a step towards leveraging some background knowledge T within the classification circuit Σ associated with a classifier C, taking advantage of the fact that T is more reliable than the data from which C has been learned. Being a first step, the present work calls for a number of perspectives. One of them consists in deriving representation theorems for the rectification operators, giving constructive characterization results for their family. We plan also to study in more depth the family of operators ensuring knowledgecompliance, i.e., operators satisfying (RE2') and (RE3') instead of (RE2) and (RE3). Finally, another important perspective for further research concerns the representation side: the rectified representations Σ ⋆D T and Σ ⋆s T , as given by Definition 7, are of size exponential in the number n of features. This makes their computation impractical most of the time. In order to address this issue, more succinct representations for Σ ⋆D T and Σ ⋆s T must be looked for.

Acknowledgements

Many thanks to the anonymous reviewers for their comments and suggestions. This work has benefited from the support of the AI Chair EXPEKCTATION of the French National Research Agency (ANR). It was partially supported by TAILOR, a project funded by EU Horizon 2020 research and innovation programme under GA No 952215.