Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.mcts-falsification

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/mcts_falsification.clj2 definitions, 3 theorems

AHoF V19 MCTS for Falsification: Monte Carlo tree search over the space of system behaviours to find a specification violation, selecting child nodes by their UCB score and keeping the higher-scoring child: prefers-child-zero? u0 u1 = decide (u1 <= u0) tree-value u0 u1 = if (u1 <= u0) then u0 else u1 (the larger UCB) over exact rationals. Proved native and axiom-free: the selection decision, the tree value (max), and the switch when the second child scores higher. Requires audit/decide-nnrat-at-most, logic/if-data (both in the D63 checkpoint). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.mcts-falsification` prints this classification.

mcts-fal/prefers-child-zero? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

mcts-fal/tree-value :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

mcts-fal/prefers-higher-ucb :
  → bo/is-safe 3/4 1/2 = data/true

mcts-fal/tree-value-is-maximum :
  → fsc/node-value 3/4 1/2 = 3/4

mcts-fal/switches-child :
  → bo/is-safe 1/2 3/4 = data/false