babelbench

Working repo of the Cross-Paradigm Proof-Translation Benchmark (Secure Program
Synthesis Fellowship): measuring whether LLMs understand proof structure or merely
pattern-match system-specific syntax, via verifier-grounded translation tasks across
proof systems (target: ~150 theorem pairs; Coq↔Lean, TLAPS↔Dafny, cross-cluster).

The repo began life at the gr.inc OpenReward hackathon (April 2026) as LTLVerifyEnv,
a single-language-family RL environment for formal-verification tasks. It has since
been restructured into the installable babelbench package and repointed at the
translation-benchmark research arc described above — see History and
ROADMAP.md for where it's headed.

What exists today

• 8 verifier adapters (Dafny, TLA+/TLC, FlyVy, FizzBee, mypyvy, Lean 4, Agda, Rocq) — src/babelbench/verifiers/
• An OpenReward RL/eval environment with 9 splits, 2,054 tasks total — src/babelbench/server.py
• Rollout drivers (OpenAI + Anthropic/Vertex) and verifier-grounded scoring — src/babelbench/rollout/, src/babelbench/scoring/
• Audited hackathon-era results — results/hackathon/ (see AUDIT.md there for which numbers are trustworthy)

What's not built yet — the pluggable scorer and the curated theorem-pair corpus — is
tracked in ROADMAP.md. The Coq/Lean adapters now exist and their toolchains
ship in the image; what they still lack is corpus breadth, not plumbing.

Quickstart (first hour)

git clone git@github.com:swist/fv-worlds.git && cd fv-worlds
python3 -m pip install -e ".[dev,rollout]"
bash scripts/fetch_datasets.sh          # populates datasets/ (pinned upstreams)
python3 -m pytest tests/                # offline selftests — no verifiers needed

# Run 3 Dafny->TLA translation tasks against the deployed env:
export OPENREWARD_API_KEY=...           # + ANTHROPIC_API_KEY, or Vertex (below)
python3 -m babelbench.rollout.run_rollout_claude \
    --env-name swist/fv-worlds --split translation_dafny_to_tla \
    --max-tasks 3 --run-name hello-xlate
python3 -m babelbench.scoring.score_translation results-translation_dafny_to_tla-hello-xlate.jsonl

run_rollout_claude.py also accepts --task-index (pick a starting task),
--max-steps / --max-tokens (per-turn caps), --model, and --results (override
the output path). Run python3 -m babelbench.rollout.run_rollout_claude --help for
the full, current list — flags occasionally change as the harness evolves, so treat
--help as the source of truth over any doc, including this one.

Auth

• Anthropic API key: export ANTHROPIC_API_KEY=... (console.anthropic.com)
• Google Vertex (no Anthropic key): export ANTHROPIC_VERTEX_PROJECT_ID=... CLOUD_ML_REGION=global
  — the drivers auto-detect from these env vars (--provider forces one path).
  This is the path for anyone using a corporate GCP project instead of a personal
  Anthropic key (run gcloud auth application-default login once if credentials
  are missing).
• OpenAI (run_rollout.py): export OPENAI_API_KEY=...

Verifiers & the Docker images

The verifier adapters shell out to real toolchains, which ship in one of two images.
Nothing else needs installing locally — scripts/fv.py is the only entrypoint.

• Dockerfile ("base") — all 8 verifiers.
• Dockerfile.lite ("lite") — 4 verifiers only: Dafny, TLA+/TLC, Lean 4, Rocq.
  Same app stage as base; the dropped languages' splits report TOOL_MISSING here.

Both auto-publish to ghcr.io/<org>/<repo>:base / :lite on push to master
(.github/workflows/publish-images.yml); build locally with the commands below.

# Build once (~15 min+; the first stage compiles FlyVy from Rust source, and
# the Mathlib cache fetch adds more on top).
docker build --platform linux/amd64 --load -t fv-worlds:base .
docker build --platform linux/amd64 --load -f Dockerfile.lite -t fv-worlds:lite .

# Confirm the image works: runs real proofs, false theorems, and malformed
# sources through every proof assistant and checks the exact Status of each.
scripts/fv.py --selftest
FV_WORLDS_IMAGE=fv-worlds:lite scripts/fv.py --selftest --langs dafny,tlaplus,lean4,rocq

# Verify a single file (this is what the rollout agent calls each round).
scripts/fv.py lean4 datasets/translation_pa/lean4/add_zero.lean
scripts/fv.py dafny path/to/task.dfy
scripts/fv.py tlaplus path/to/Spec.tla --translation   # composite reward

fv.py prints the verifier's feedback plus a STATUS=<value> trailer and exits 0
iff the source verifies. It bind-mounts the live src/ over the image's editable
install, so adapter edits take effect without rebuilding. Override the image tag
with FV_WORLDS_IMAGE or --image; scope the self-test with --langs lean4,rocq.

--platform linux/amd64 is required everywhere: the image bundles x86_64 binaries,
and a native arm64 run dies with a rosetta ld error. On Apple Silicon everything runs
emulated, so verification is slower than the 60s default timeout might suggest
(LTLV_VERIFY_TIMEOUT raises it).

base was 8.21 GB before Mathlib was added (now several GB more — Mathlib's
prebuilt cache alone typically runs multiple GB); lite is smaller on both
verifier count and (once trimmed) build time. Every install step hard-fails the
build rather than warning: a missing toolchain makes its adapter report
TOOL_MISSING, which scores 0.0 and reads as a model failure in results rather
than as broken infrastructure. The Dockerfile header documents what to prune
first if you need base smaller.

Splits

9 splits, 2,054 tasks total. All splits share the same env API
(check(language, source) non-terminal reward 0, submit(language, source)
terminal). Most splits use a binary reward — 1.0 iff the verifier accepts, 0.0
otherwise — but spec_synthesis and translation_dafny_to_tla layer a composite
reward on top instead (see below).

See docs/splits.md for per-split task shape, field semantics, and the difficulty
ladder these splits were originally designed around.

Why DafnyBench is excluded from dataset_invariants

DafnyBench has been in every frontier model's training corpus since 2024. Including
it in the main invariant-filling split would inflate the headline number with
memorization, not capability. We keep DafnyBench on disk for two purposes instead:

• dataset_dafnybench — the contaminated baseline, useful as a known recall surface
• dataset_mutated — the same problems, structurally rewritten; the gap between
  pass rates on these two splits is the memorization measurement

babelbench.scoring.eval_mutation_gap computes that gap directly.

Reward structure

Sparse and verifier-grounded — reward comes from a real verifier's accept/reject
decision, delivered only at episode termination via submit.

Standard splits (dataset_*, synthesis, smoke):

• 1.0 if the verifier exits cleanly AND the output classifier returns VERIFIED
• 0.0 if rejected, parse error, timeout, or Status.REWARD_HACK (Dafny's syntactic
  guard caught a literal assume false / assume {:axiom} false variant)

spec_synthesis split (composite, still fully programmatic — no LLM judge):

• 0.0 if the source contains a reward-hack construct (multiplicative gate)
• 0.5 if the spec verifies but is vacuous (probe: delete the first body statement;
  if the spec still verifies, it wasn't load-bearing)
• 1.0 if the spec verifies AND the probe rejects (the spec was genuinely needed)

translation_dafny_to_tla split (composite, still fully programmatic — no LLM
judge — see docs/splits.md for the full detail):

• 0.5 if TLC accepts the submitted TLA+ source
• 0.3 if the property is non-trivial (a mutation probe shows it's load-bearing)
• 0.2 reserved for a bidirectional check — not yet implemented

The check tool returns the same verifier feedback mid-episode but yields reward 0
and does not terminate, so the model can iterate against it.

This is becoming pluggable. The verifier's accept/reject decision remains ground
truth for every task, but the scoring layer around it — how "verified" gets turned
into a number, and eventually how cross-system translations get judged as "proving
the same thing" — is being generalized so alternative scorers (proof-trace heuristics,
an LLM grader evaluated against verifier truth) can be compared on equal footing.
See ROADMAP.md and CLAUDE.md's Scoring policy section.

Repo layout

Provenance & licenses

MIT for the environment scaffolding. Vendored corpora retain their upstream licenses
(all permissive — DafnyBench MIT, tlaplus/Examples MIT, FlyVy MIT, FizzBee Apache-2.0,
mypyvy BSD-3-Clause, IronFleet MIT). Full attribution, source repos, and pinned
commits are in datasets/PROVENANCE.md — run bash scripts/fetch_datasets.sh to
populate datasets/ and examples/ironfleet_reference/ from those pins.

IronFleet is vendored as reference material only for synthesis prompts, not
graded directly — it requires Dafny 3.4.0 and ~50K LoC of interdependent proofs that
won't verify file-by-file. Don't try to "fix" this; it's a deliberate scope boundary.

History

Built at the gr.inc OpenReward hackathon (April 2026) as LTLVerifyEnv, a
verifier-grounded RL environment spanning five formal-verification languages. The
hackathon-2026-04-final git tag preserves that state in full, including the eval
logs that were later pruned from master. docs/archive/ carries the deck-era
narrative docs (DECK.md, DECK_BRIEF.md, HANDOFF.md, findings-2026-04-25.md) —
useful for the "how did we get here" story, but their quantitative claims should be
checked against results/hackathon/AUDIT.md before being cited anywhere new.