AI Entropy Control

IDLE

Quick Start

Run LM Studio or Ollama.
Serve this over http:// (e.g., python -m http.server 8000).
Set API Base and Chat Model (LM Studio defaults below).
Click Check API. Then use Self-Test or Start.

Clean UI Hide advanced controls

Use http://

API & Providers

API Base

API Key

Chat Model

Lookahead Model

Emb Base

Emb Model

Safety Provider

Contradiction Provider

Live Lookahead

APS (speculative)

0.00

Entropy

0.00

Perplexity

0.00

Speculative Next Sample

Lookahead: —logprobs: no

Ignore rails (debug)

Drafts K Cluster thr

Weights & Thresholds

θ_hi (High)70%

Emergency brake threshold

θ_lo (Low)55%

Safe resume threshold

λ (EMA)80%

Smoothing factor

θ_crit (Critical)85%

Critical anomaly level

w_R (Repetition)30%

Weight for repetitive content

w_C (Contradiction)20%

Weight for logical contradictions

w_N (Topic Drift)20%

Weight for topic deviation

w_S (Safety)15%

Weight for safety violations

w_J (Injection)10%

Weight for prompt injection

w_P (PII)5%

Weight for personal information

w_A (APS)60%

Weight for anomaly score

w_V (Velocity)25%

Weight for change velocity

w_F (Frequency)15%

Weight for generation frequency

w_SE (Speculative)20%

Weight for speculative execution

Predictive Upgrades

CUSUM ramp detector Entropy/Perplexity gate Speculative lookahead

CUSUM k

CUSUM h

Entropy ≤

Perplexity ≤

Lookahead tokens

ALC / ALCad (Control Loop)

N_tail (tokens withheld)

K_RESUME (frames <= θ_lo)

Cooldown τ (ms)

cad_base (ms)

cad_min (ms)

cad_max (ms)

α (APS influence)

β (velocity influence)

γ (stability streak)

Hysteresis Δ

ALCad adjusts lookahead frequency and horizon using APS and its velocity. ALC enforces brake/cooldown/resume & tail-buffer non‑leakage.

System Status

IDLE

High Threshold (θ_hi)

0.70

Low Threshold (θ_lo)

0.55

APS* (Blended)

0.000

Critical (θ_crit)

0.85

Live Anomaly Scores

Prompt & Controls

Explanations

Compliance Records

No compliance records yet.

Live Output

Reasons:

Formal Verification — nuXmv

This section embeds the enhanced nuXmv model (AEC_nuXmv_model_v2.smv) and provides a one-click download & quick run commands.

nuXmv Model (read-only)

MODULE main
CONSTANTS
  NTAIL := 5;        -- withheld tokens
  TAU   := 5;        -- cooldown ticks
  KRES  := 4;        -- consecutive LOW frames to resume
  CAD_MIN := 1;      -- min cadence
  CAD_MAX := 5;      -- max cadence
  BASE    := 3;      -- base cadence
  ALPHA   := 1;      -- APS influence on cadence
  BETA    := 1;      -- velocity influence on cadence
  GAMMA   := 1;      -- stability streak influence on cadence
;

VAR
  -- Finite automaton states
  state : {IDLE, GENERATING, ANALYZING, BRAKED, RESUME};

  -- APS bucket and numeric proxy
  aps   : {LOW, MID, HIGH, CRIT};
  aps_num : 0..3;          -- LOW=0, MID=1, HIGH=2, CRIT=3
  aps_prev : 0..3;         -- previous aps_num
  vel      : -3..3;        -- velocity = aps_num - aps_prev
  stable_streak : 0..10;   -- increments when aps=LOW, resets when aps>=HIGH

  -- Environment inputs (nondeterministic)
  start : boolean;         -- prompt event
  look  : boolean;         -- trigger lookahead
  gen   : boolean;         -- attempt to generate a token this step

  -- Cooldown & resume counters
  cooldown : 0..TAU;
  kframes  : 0..KRES;

  -- Cadence (explicit) and previous cadence for monotonic checks
  c      : CAD_MIN..CAD_MAX;
  c_prev : CAD_MIN..CAD_MAX;

  -- Tail queue (concrete, but abstract content): counts only
  tail_count        : 0..NTAIL;  -- withheld tokens
  risky_tail_count  : 0..NTAIL;  -- how many withheld tokens were generated under HIGH/CRIT

  -- Outputs / derived
  emit     : boolean;
  violation: boolean;

ASSIGN
  init(state) := IDLE;
  init(aps) := LOW;
  init(aps_num) := 0;
  init(aps_prev) := 0;
  init(vel) := 0;
  init(stable_streak) := 0;
  init(cooldown) := 0;
  init(kframes) := 0;
  init(c) := BASE;         -- start in base, will be clipped
  init(c_prev) := BASE;
  init(tail_count) := 0;
  init(risky_tail_count) := 0;
  init(emit) := FALSE;
  init(violation) := FALSE;

  -- Environment choices each step
  next(aps) := {LOW, MID, HIGH, CRIT};
  next(start) := {TRUE, FALSE};
  next(look)  := {TRUE, FALSE};
  next(gen)   := {TRUE, FALSE};

  -- Map aps to numeric bucket
  next(aps_num) := case
    next(aps) = LOW  : 0;
    next(aps) = MID  : 1;
    next(aps) = HIGH : 2;
    TRUE             : 3; -- CRIT
  esac;

  -- Track previous APS and velocity
  next(aps_prev) := aps_num;
  next(vel) := next(aps_num) - aps_num;

  -- Stability streak: increment when APS LOW, reset when APS >= HIGH; hold otherwise
  next(stable_streak) := case
    next(aps) = LOW                      : (stable_streak < 10) ? stable_streak + 1 : 10;
    (next(aps) = HIGH | next(aps) = CRIT): 0;
    TRUE                                 : stable_streak;
  esac;

  -- State transitions (with immediate braking on HIGH/CRIT)
  next(state) := case
    (next(aps) = HIGH | next(aps) = CRIT) : BRAKED;

    state = IDLE & start     : GENERATING;
    state = IDLE & !start    : IDLE;

    state = GENERATING & look : ANALYZING;
    state = GENERATING & !look: GENERATING;

    state = ANALYZING & (next(aps) = LOW | next(aps) = MID) : GENERATING;
    state = ANALYZING & !(next(aps) = LOW | next(aps) = MID) : BRAKED;

    state = BRAKED & (cooldown = TAU) & (kframes = KRES) & (next(aps) = LOW) : RESUME;
    state = BRAKED : BRAKED;

    state = RESUME : GENERATING;

    TRUE : state;
  esac;

  -- Cooldown counter (only while BRAKED)
  next(cooldown) := case
    state != BRAKED & next(state) = BRAKED : 0;             -- entered BRAKED
    next(state) = BRAKED & cooldown < TAU  : cooldown + 1;  -- count up
    next(state) = BRAKED & cooldown = TAU  : cooldown;      -- hold
    next(state) != BRAKED                  : 0;             -- reset on leave
    TRUE : cooldown;
  esac;

  -- K_RESUME consecutive LOW frames while BRAKED
  next(kframes) := case
    next(state) = BRAKED & next(aps) = LOW & kframes < KRES : kframes + 1;
    next(state) = BRAKED & next(aps) != LOW                 : 0;
    next(state) != BRAKED                                    : 0;
    TRUE : kframes;
  esac;

  -- Cadence update (clipped linear law): c' = clip(BASE - ALPHA*aps_num - BETA*vel + GAMMA*stable_streak)
  next(c_prev) := c;
  next(c) :=
    case
      TRUE :
        let raw := BASE - ALPHA*next(aps_num) - BETA*next(vel) + GAMMA*next(stable_streak) in
          (raw < CAD_MIN) ? CAD_MIN :
          (raw > CAD_MAX) ? CAD_MAX : raw;
    esac;

  -- Tail queue management
  -- On entering BRAKED: discard tail entirely (non-leakage policy)
  next(tail_count) := case
    state != BRAKED & next(state) = BRAKED : 0;
    -- Generate: enqueue withheld token up to NTAIL
    gen & tail_count < NTAIL               : tail_count + 1;
    gen & tail_count >= NTAIL              : tail_count;
    -- Safe emission: only when not BRAKED, APS LOW, and no risky tokens remain
    next(state) != BRAKED & next(aps) = LOW & risky_tail_count = 0 & tail_count > 0 : tail_count - 1;
    TRUE : tail_count;
  esac;

  next(risky_tail_count) := case
    state != BRAKED & next(state) = BRAKED : 0;  -- discard risky tokens on brake
    -- Generate under high risk: mark in risky count (bounded by tail capacity)
    gen & (next(aps) = HIGH | next(aps) = CRIT) & risky_tail_count < NTAIL : risky_tail_count + 1;
    -- Safe emission only allowed when risky_tail_count = 0; thus no decrement here
    TRUE : risky_tail_count;
  esac;

  -- Emission and violation flags
  next(emit) := next(state) != BRAKED & next(aps) = LOW & risky_tail_count = 0 & tail_count > 0;
  -- Violation if an emission occurs while any risky token remains (should never happen)
  next(violation) := next(emit) & (risky_tail_count > 0);

-- =====================
--  PROPERTIES TO CHECK
-- =====================

-- 1) Non-leakage: never emit while a risky token exists
INVARSPEC G !(emit & (risky_tail_count > 0))

-- 2) Immediate brake on HIGH/CRIT
LTLSPEC G( (aps = HIGH | aps = CRIT) -> X state = BRAKED )

-- 3) Eventual resume after cooldown + KRES LOW frames
LTLSPEC G( (state = BRAKED & cooldown = TAU & kframes = KRES & aps = LOW) -> F state = RESUME )

-- 4) No oscillation before ready: remain BRAKED until conditions met
LTLSPEC G( (state = BRAKED & !(cooldown = TAU & kframes = KRES & aps = LOW)) -> X state = BRAKED )

-- 5) Cadence bounds must always hold
INVARSPEC G (c >= CAD_MIN & c <= CAD_MAX)

-- 6) Cadence responsiveness: if APS increases (num), cadence should not increase next step
--    i.e., aps_num' > aps_num  =>  c' <= c
LTLSPEC G( (aps_num < next(aps_num)) -> X (c <= c_prev) )

-- 7) Cadence responsiveness: if APS decreases and we are stably LOW, cadence should not decrease
LTLSPEC G( (aps_num > next(aps_num) & next(aps) = LOW & stable_streak >= 1) -> X (c >= c_prev) )

nuXmv AEC_nuXmv_model_v2.smv
go
check_invar
check_ltlspec
simulate -k 25 -r

Automaton Diagram

States: IDLE → GENERATING → ANALYZING → BRAKED → RESUME. Guards: APS thresholds, cooldown τ, K_RESUME, tail-buffer non-leakage, cadence bounds.

AI Entropy
Control

Building trust in
autonomous systems

Three-layer protection

Adaptive Thresholds

Tail Non-Leakage

Explainable Signals