Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.imitation-irl

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/imitation_irl.clj4 definitions, 4 theorems

Kochenderfer imitation-learning / inverse-RL / structure-learning cores as higher-order-function compositions, proved axiom-free, extending the 222 AHoF catalog: D18.3 SMILe : stochastic mixture of expert-imitating policies (convex blend) D18.5 max-margin IRL : reward makes the expert beat alternatives by a margin (sound) D18.6 max-entropy IRL : trajectory probability = exp-weight / partition (normalized) D5.3 structure learning: hill-climb the DAG by score (accepted neighbor >= current) The SMILe blend reuses nnrat/wsum2 (bounded by convex-at-most-max); the margin test is a decidable order on expert-vs-(alternative+margin) with soundness; max-entropy is a normalized weight (divide); structure search reuses nnrat-minmax max. Native and axiom-free; chains nnrat-convex on d63.

Depends onmath.rational.nnrat.convex

irl/smile-mixture :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

irl/margin-satisfied :
  (x₁ x₂ x₃ : ℚ≥0)
  → data/Bool

irl/maxent-probability :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

learn/structure-accept :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

irl/smile-within-max :
  (w0 w1 p0 p1 : ℚ≥0)
  (hw : w0 + w1 = 1)
  → bo/bootstrap-632 w0 w1 p0 p1 ≤ minmax/max p0 p1

irl/margin-sound :
  (expert alt margin : ℚ≥0)
  (ok : irl/margin-satisfied expert alt margin = data/true)
  → alt + margin ≤ expert

irl/maxent-probability-example :
  → accuracy/accuracy 3 4 = 3/4

learn/structure-improves :
  (current neighbor : ℚ≥0)
  → current ≤ game/pomg-value current neighbor