Active Learning, Teachers, and Meta-Learning

Active learners query oracles. Teachers present data strategically. Meta-learners learn to learn. Also includes synthesizers and verifiers for the CEGIS paradigm.

Active Learner (Query Learning)

structure ActiveLearner (X : Type u) (Y : Type v) : Type (max u v)

An active learner can query oracles (membership, equivalence).

• hypotheses : HypothesisSpace X Y

  The hypothesis space

• learnMQ : MembershipOracle X Y → Concept X Y

  Learning with membership oracle: produce a hypothesis

• output_in_H_MQ (mq : MembershipOracle X Y) : self.learnMQ mq ∈ self.hypotheses

  Output is in hypothesis space

def IsPassive {X : Type u} {Y : Type v} (_L : BatchLearner X Y) : Prop

A passive learner receives data without querying.

Equations

• IsPassive _L = True

structure LearnerWithAdvice (X : Type u) (Y : Type v) (A : Type u_1) : Type (max (max u u_1) v)

A learner augmented with advice.

• base : BatchLearner X Y

  Base learner

• learnWithAdvice : A → {m : ℕ} → (Fin m → X × Y) → Concept X Y

  Advice-augmented learning: advice → sample → hypothesis

Teachers

structure Teacher (X : Type u) (Y : Type v) : Type (max u v)

A teacher presents examples to a learner according to some strategy.

• target : Concept X Y

  The concept the teacher is teaching

• teach : List (X × Y) → X × Y

  Teaching strategy: choose next example given what's been shown

def Teacher.teachingSequence {X : Type u} {Y : Type v} (T : Teacher X Y) : ℕ → List (X × Y)

Generate the teaching sequence: the teacher's strategy iterated.

Equations

• T.teachingSequence 0 = []
• T.teachingSequence n.succ = T.teachingSequence n ++ [T.teach (T.teachingSequence n)]

def IsOptimalTeacher {X : Type u} {Y : Type v} (T : Teacher X Y) (C : ConceptClass X Y) : Prop

An optimal teacher minimizes the number of examples needed to uniquely identify the target within concept class C. Formally: the teaching sequence distinguishes T.target from all other c ∈ C in at most k steps, and no teacher for the same target does it in fewer.

Equations

• One or more equations did not get rendered due to their size.

def IsAdversarial {X : Type u} {Y : Type v} (T : Teacher X Y) (C : ConceptClass X Y) : Prop

An adversarial teacher chooses examples that maximize learner error. For every learner state (represented by what the learner has seen so far), the teacher picks the example that is hardest for ANY learner to use.

Equations

• One or more equations did not get rendered due to their size.

def IsRandomTeacher {X : Type u} {Y : Type v} (T : Teacher X Y) : Prop

A random teacher draws examples uniformly: the teaching strategy does not depend on what data has been shown so far.

Equations

• IsRandomTeacher T = ∀ (data₁ data₂ : List (X × Y)), T.teach data₁ = T.teach data₂

structure MinimallyAdequateTeacher (X : Type u) (Y : Type v) : Type (max u v)

Minimally adequate teacher: provides membership queries and equivalence queries. Interface for Angluin's L* algorithm.

• mq : MembershipOracle X Y

  Membership oracle

• eq : EquivalenceOracle X Y

  Equivalence oracle

• consistent : self.mq.target = self.eq.target

  Both answer about the same target

Meta-Learner

structure MetaLearner (X : Type u) (Y : Type v) : Type (max u v)

A meta-learner: a learner that takes a concept class and produces a learner specialized for that class (learning-to-learn).

• metaLearn : ConceptClass X Y → BatchLearner X Y

  Given a concept class, produce a learner for that class

structure LLMCritic (X : Type u) (Y : Type v) extends Teacher X Y : Type (max u v)

LLM critic: a teacher that uses a language model as its strategy.

• target : Concept X Y
• teach : List (X × Y) → X × Y
• critiqueQuality : ℝ

  Critique quality score

def Synthesizer (X : Type u) (Y : Type v) : Type (max (max (max v u) v) u)

A synthesizer: produces candidate concepts from specifications.

Equations

• Synthesizer X Y = (List (X × Y) → Concept X Y)

def Verifier (X : Type u) (Y : Type v) (spec candidate : Concept X Y) : Type u

A verifier: checks whether a candidate concept satisfies a specification.

Equations

• Verifier X Y spec candidate = Option { x : X // candidate x ≠ spec x }