law sample_below

bend-ml-llama@0.2.1.0 · main.bend:1391

import Base
import bend-ml-tensor-array@0.1.19.0/main.bend as TA

1391# LAW (sample_below): from logits xs with at least one value, the id sample draws is below the length of xs: an id
1392# of the vocabulary, whatever the temperature, k, p and draw.
1393# PROOF: the top-k pass only stores ids of xs, each below its length (topk_below, from i = 0 and no candidates),
1394# and the draw returns one of them (pick_below, through the top-p count, whatever it is).
1395law sample_below:
1396  for +xs: List<&2, F32>
1397  for +temp: F32
1398  for +k: Nat
1399  for +p: F32
1400  for +u: F32
1401  for pos: {True{} == TA.leb(1n, List.length(&2, F32, xs)) : Bool}
1402  {True{} == TA.leb(1n+Cand.i(sample(xs, temp, k, p, u)), List.length(&2, F32, xs)) : Bool}