Formal Philosophy Experiment

TauEnergy replayable training experiment

Route learning with Tau kept in charge

This page presents the public snapshot for the TauEnergy workbench. The model ranks candidate routes, while Tau or deterministic certificate checks verify route validity. The snapshot ships metrics and replay instructions, excluding Tau source, Tau binaries, and private formula corpora.

advisory energy ranker verifier decides license-aware replay invalid accepts: 0

Replay command inside TauLang-Experiments

./scripts/run_tau_energy_training_demo.sh --accept-tau-license --quick

Genuine optimization

8.0x

Solver-call reduction reported by the indexed impacted-factor route.

Measured learned top-1

92.16%

Held-out route-choice accuracy from Tau-checked measured training cases.

Ordered-BDD curriculum best

93.75%

Best top-1 result after adding fragment-specific BDD training examples.

Weakest holdout family

ordered_bdd

4.17% top-1 on the hardest family holdout.

Reasoning split

The experiment treats route choice as a learned proposal problem. Syntax checks, Tau executions, route certificates, and replay verification operate as deterministic gates. This strict boundary is the core architecture readers can inspect. Click any stage below to inspect its behavior.

Stage 1 LLM

Translates human intentions into logical, machine-readable work packets.

Stage 2 TauEnergy

Ranks candidate routes using learned formula-shape evidence.

Stage 3 WES

Explores candidate spaces and builds replayable execution certificates.

Stage 4 Tau

Authoritative verifier gating route entry via deterministic logic checks.

Interactive Routing Pipeline Inspector

LLM Translation Stage

Trust Boundary Untrusted Input
Deterministic Gate No (Advisory/Heuristic)
Domain Object WorkPacket

Translates fuzzy user requirements into verified, structured work packets before passing to internal optimizers.

REPLAYABLE PIPELINE TELEMETRY IDLE
// Click 'Run Pipeline Trace' to simulate a route calculation.

Ordered-BDD curriculum

The curriculum establishes a broad baseline before injecting BDD-specific examples. This targeted addition demonstrates that fragment-specific examples successfully steer route ranking. Click any step bar below to inspect training impact.

Supported claims

  • 1

    A public metric snapshot loads from a static JSON artifact.

  • 2

    The included reports record zero invalid accepts.

  • 3

    The replay path requires readers to obtain Tau from the official source following license review.

  • 4

    The ranker improves search ordering in the measured workbench, while verification remains strictly deterministic.

Assumptions

Assumption A: The public JSON snapshot accurately summarizes the local replay artifacts.

Assumption B: Tau syntax and route behavior drift over time; therefore, claims require fresh local replay before serving as current performance evidence.

Boundary limits

This experiment does not claim that TauEnergy proves correctness, that TauJEPA proves future safety, or that a learned route selector replaces Tau's authoritative checks. The trained model operates strictly as an advisory ordering aid.

Reader replay

Readers must reproduce the workbench from the TauLang-Experiments repository after reviewing Tau's license. The quick path regenerates the public snapshot; the full path reruns the broader training bundle.

Quick replay

./scripts/run_tau_energy_training_demo.sh --accept-tau-license --quick

Full replay

./scripts/run_tau_energy_training_demo.sh --accept-tau-license --full

Loading public metric snapshot...