FLTEval

FLTEval is a minimal, Docker-only evaluation harness for FLT Lean tasks. It is shaped like SWE-bench evaluation: users submit diffs, the harness applies each diff inside the task image, runs Lean/SafeVerify checks, and writes per-instance and aggregate reports.

The harness does not run agents or generate traces.

License

FLTEval is distributed under the Apache License 2.0. SafeVerify source is not vendored in this repository; the evaluator reads it from the SafeVerify repository at the commits pinned in flteval/resources/safeverify/manifest.json.

Quick Start

uv run python -m flteval.harness.run_evaluation \
  --dataset_name data/flt_sample \
  --predictions_path submissions/leanstral_sweagent_sample_0.jsonl \
  --instance_ids imperialcollegelondon__flt-1611de00afff6d40cdb98aa669258fdaff38edb7 \
  --run_id leanstral-sample-smoke \
  --report_dir evaluation_results \
  --max_workers 1

preds.json may be mini-swe-agent's dictionary format:

{
  "instance-id": {
    "model_name_or_path": "model",
    "instance_id": "instance-id",
    "model_patch": "diff --git ..."
  }
}

Gold evaluation is supported:

uv run python -m flteval.harness.run_evaluation \
  --dataset_name data/flt_sample \
  --predictions_path gold \
  --instance_ids imperialcollegelondon__flt-1611de00afff6d40cdb98aa669258fdaff38edb7 \
  --run_id gold-smoke \
  --report_dir evaluation_results

Dataset Shape

Rows are SWE-bench-like and must include:

• instance_id
• problem_statement
• patch
• test_patch
• FAIL_TO_PASS
• PASS_TO_PASS
• install_config.lean_version
• install_config.axiom_list
• image_name or docker_image

For mini-swe-agent generation, prepared rows also expose:

• startup_patch
• startup_patch_delimiter

The bundled mini-swe-agent config writes startup_patch to /tmp/startup.patch with a quoted heredoc and applies it before the agent starts. It renders the target declarations into the agent prompt from FAIL_TO_PASS.

Prepare The Local FLT JSONL

uv run python scripts/prepare_dataset.py \
  path/to/raw-flt.jsonl \
  data/flt_sample/test.jsonl

This repository includes three sample artifacts:

• data/flt_sample/test.jsonl: a prepared 162-instance dataset sample.
• submissions/leanstral_sweagent_sample_0.jsonl: matching mini-swe-agent submissions for that sample.
• evaluation_results/sweagent_sample_0.leanstral_sweagent_sample_0.json: an aggregate evaluation report for the sample submissions.

data/flt_sample is a directory with test.jsonl so mini-swe-agent can load it as datasets.load_dataset("data/flt_sample", split="test"); FLTEval accepts the same directory path for verification.

The full public dataset should live on Hugging Face. This repository should only carry code, schema/docs, tests, and optionally a tiny sample.

SafeVerify Source

FLTEval keeps only a SafeVerify manifest in git. At evaluation time it reads Main.lean and lakefile.lean from a local SafeVerify checkout by commit SHA. If no checkout exists, the evaluator clones the repository into $XDG_CACHE_HOME/flteval/LeanstralSafeVerify or ~/.cache/flteval/LeanstralSafeVerify.

Useful overrides:

• FLTEVAL_SAFEVERIFY_PATH: use a specific SafeVerify checkout.
• FLTEVAL_SAFEVERIFY_REPO: clone from a specific repository URL.

To bump SafeVerify, update the manifest from a dataset that covers the Lean versions you need:

uv run python scripts/update_safeverify_manifest.py \
  data/flt_sample \
  --safeverify-version v1.0.8 \
  --safeverify-path ~/.cache/flteval/LeanstralSafeVerify

Then verify a prepared dataset has pinned SafeVerify entries:

uv run python scripts/validate_dataset.py \
  data/flt_sample \
  --check-safeverify-resources

The updater records both the tag and resolved commit for each Lean version. If a tag moved, the updater fails by default. After verifying the retag is intentional, rerun it with --accept-retags and commit the manifest change.

mini-swe-agent

Pass mini-swe-agent's default SWE-bench config first, then layer the FLTEval Lean overrides on top:

mini-extra swebench \
  --subset data/flt_sample \
  --split test \
  --filter '^imperialcollegelondon__flt-1611de00afff6d40cdb98aa669258fdaff38edb7$' \
  --config swebench.yaml \
  --config configs/mini-swe-agent/flt.yaml \
  --model <model> \
  --workers 1 \
  --output runs/<model>-flt

Then evaluate:

uv run python -m flteval.harness.run_evaluation \
  --dataset_name data/flt_sample \
  --predictions_path runs/<model>-flt/preds.json \
  --run_id <model>-flt \
  --report_dir evaluation_results

In mini-swe-agent's SWE-bench runner, run.env_startup_command is rendered with the full dataset row after the Docker environment is created and before the agent receives problem_statement. That is where startup_patch belongs. Extra row fields such as mcp_servers are ignored unless a config template explicitly references them.

See docs/dataset_schema.md for the row format and docs/prediction_schema.md for accepted submission formats.