Skip to content
Chelis docs

Oracle strategies

Beacon's oracle strategy determines how inputs are interpreted and under what conditions a proved verdict is sound. Select an oracle with the --oracle flag.

arb-point

Section titled “arb-point”

Singleton parsed-f64 inputs. Each named input binds to exactly one floating-point value.

Terminal window
chelis-beacon check model.wiredag --oracle arb-point --input x=1.5 --output-range '[0.0, 2.0]'

The proved verdict is fully sound: if Beacon reports proved, the output at that exact input point is guaranteed to lie within the target range.

arb-box

Section titled “arb-box”

Parsed-f64 input boxes. Each named input binds to a closed interval.

Terminal window
chelis-beacon check model.wiredag --oracle arb-box --input x='[1.0, 2.0]' --output-range '[0.0, 5.0]'

The proved verdict is fully sound: the output is guaranteed to lie within the target range for every point in the input box.

arb-split

Section titled “arb-split”

Bounded split oracle. Beacon recursively bisects the input box and verifies each leaf independently.

Terminal window
chelis-beacon check model.wiredag --oracle arb-split --input x='[0.0, 10.0]' --output-range '[0.0, 100.0]'

Beacon emits proved only when:

  1. The split leaves completely cover the original input box.
  2. No leaf remains unresolved (every leaf individually satisfies the target range).

If any leaf cannot be resolved within the split budget, Beacon reports the unresolved leaves and does not emit proved.

zonotope-verified

Section titled “zonotope-verified”

Zonotope lane with dependency tracking. This strategy maintains affine forms through the DAG, preserving correlations between intermediate values.

Key properties:

  • Refined Mul bounds: affine-remainder bounding for multiplication nodes tightens the output interval compared to naive interval arithmetic.
  • Arb-verified branch-and-bound: for nonzero tolerance bands, Beacon invokes an Arb-verified B&B API to resolve tight cases.
  • Dependency tracking: zonotope noise symbols carry through the DAG, preventing spurious interval blowup from correlated variables.
Terminal window
chelis-beacon check model.wiredag --oracle zonotope-verified \
  --input x='[0.0, 1.0]' \
  --output-range '[0.0, 1.0]'

The proved verdict under zonotope-verified is sound. The tighter bounds from dependency tracking mean this oracle resolves cases that arb-box cannot, at higher computational cost.