mistralai/FLTEval

mistralai/FLTEval

Description: Docker-only evaluation harness for FLT Lean tasks

Language: Python

License: Apache-2.0

Stars: 0

Forks: 0

Open issues: 0

Created: 2026-07-02T15:38:32Z

Pushed: 2026-07-02T15:38:53Z

Default branch: main

Fork: no

Archived: no

README:

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 \
--workers 1 \
--output runs/-flt

Then evaluate:

uv run python -m flteval.harness.run_evaluation \
--dataset_name data/flt_sample \
--predictions_path runs/-flt/preds.json \
--run_id -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](docs/dataset_schema.md) for the row format and [docs/prediction_schema.md](docs/prediction_schema.md) for accepted submission formats.