A new invariant for the AFP Horn learning algorithm José L. Balcázar (UPC)

part of ongoing work (with unclear destiny) with Lenny Pitt, Bardia Sadri (UIUC) and others

Learning via Queries

Active Learning: the learning process interacts with a fixed target concept Concept modeled as a set of (positive) instances: inductive bias Interaction through a Query Protocol Most popular protocol:

Membership queries Equivalence queries

Termination implies correctness

Propositional Logic Context

Instances are bit vectors of length n Equivalently:

tuples in a relation of a binary database propositional models

In the last view, each concept is then a propositional theory

Our Case

Inductive bias is: we assume that the target concept is described by a conjunction of m propositional Horn clauses

Known: Horn theories are exactly those closed under bitwise intersection

Upper bound (Angluin/Frazier/Pitt 1992): algorithm making O(nm^{2}) queries

Lower bound (Arias/Khardon/Servedio 2003): certificate size Ω(nm)

Interest

Outside visibility!

Khardon first-order extensions (ILP, MRDM) Kivinen and Mannila (databases) Kearns, Kautz, and Selman

(knowledge compilation) ...

Extremely sensitive algorithm that we should understand better

Context and Notation

H^{∗} Horn formula on n variables Clauses α → v, α a term, v a variable or ⊔ ⊓ (definite Horn clauses for today) Equivalently, H^{∗} is closed under bitwise intersection Negative assignments denoted x⊖ (x |̸= H^{∗}) Positive assignments denoted z⊕ (z ⊧ H^{∗})

The Angluin/Frazier/Pitt Algorithm

Maintain set P of positive examples seen so far Maintain negative examples x_{1}, …, x_{t} (Each one chases a different clause of the target H^{∗}) From the x_{i}, construct a sensible hypothesis H^{•} consistent with P Process the counterexample y using memberships

Processing the Counterexample (sort of)

y⊕: add to P (reduces the hypothesis H by removing all clauses inconsistent with y) y⊖: compare to x_{1}, …, x_{t}

i := min({j|(x_{j} ∧ y)⊖, x_{j} ≰ y} ∪ {t + 1}) (suggestion: imagine that x_{t+1} = 111...1) x_{i} := [x_{i} ∧]y (refines a negative example)

Refinement: x_{i} ≰ y ⟺ (x_{i} ∧ y) < x_{i}

Termination

We bound t ≤ m, where m is the number of clauses in any arbitrary Horn axiomatization of H^{∗} Each x_{i} is refined at most n times According to [AFP], the following suffices: if x_{i} |̸= (α → v) and x_{j} |̸= (α → v) for i ≠ j, then H^{∗} |̸= (α → v) Want: a stronger argument that explains what happens if we change the algorithm a bit

Towards a New Invariant

A preliminary invariant:

∀i < j ∃z⊕ [x_{i} ∧ x_{j} ≤ z < x_{j}]

y⊕ does not affect it x_{i} refined into x_{i} ∧ y maintains it y becoming x_{t+1} (one case):

x_{i} ∧ x_{t+1} = (x_{i} ∧ y)⊕ < y for all i ≤ t About the Preliminary Invariant (I)

∀i < j ∃z⊕ [x_{i} ∧ x_{j} ≤ z < x_{j}]

Assume x_{i} |̸= (α → v) and x_{j} |̸= (α → v) for i ≠ j

x_{i} ∧ x_{j} ≤ z: thus z ⊧ α

z ≤ x_{j}: thus z |̸= v, and z |̸= (α → v)

But z⊕, so H^{∗} |̸= (α → v)

About the Preliminary Invariant (II)

∀i < j ∃z⊕ [x_{i} ∧ x_{j} ≤ z < x_{j}]

x_{j} refined into x′_{j} = x_{j} ∧ y maintains it: x_{i} ∧ x′_{j} = x_{i} ∧ x_{j} ∧ y =

= (x_{i} ∧y)∧(x_{i} ∧x_{j}) ≤ (x_{i} ∧y)∧z ≤ x_{j} ∧y = x′_{j} But j > i: assume i was not refined because (x_{i}∧y)⊕ By closure of H^{∗} under bitwise intersection, z′ = ((x_{i} ∧ y) ∧ z)⊕ Problem: maybe i was not refined because x_{i} ≤ y

Intuition about the New Invariant

H^{•} has the form ⋀{x_{i} → v} including all clauses that are not disproved by some positive example Consider x^{•} = ⋀{v|H^{•} ⊧ (x → v)} Similarly x^{∗} = ⋀{v|H^{∗} ⊧ (x → v)}, x^{∗}⊕ The construction of H^{•} implies x^{∗} ≤ x^{•} If y ⊧ H^{•} and x_{i} ≤ y, then x_{i} ≤ x^{∗} ≤ x^{•} ≤ y For i < j, any y that refined x_{j} may have had two reasons for skipping x_{i}, and both are good but must be argued separately

The Invariant

∀i < j

∃z_{i,j}⊕ ∃x_{i,j} ∃y_{i,j} x_{j} = x_{i,j} ∧ y_{i,j}, x_{i}^{∗} ≤ y_{i,j}, x_{i} ∧ x_{i,j} ≤ z_{i,j} < x_{i,j}

Call that expression I_{i,j}

How to Refine Several Antecedents

Consider I_{i,j} and I_{j,i} One of them suffices for each pair Keep a directed graph indicating ¬I_{i,j} Use it to refine several x_{i} but ensuring that, for each j, either I_{i,j} or I_{j,i} (Details not yet worked out - unclear what it buys!) Goal: an algorithm making O(mn) queries