MiniF2F · premise retrieval benchmark · SciLib

⊢ Experiment

MiniF2F · premise retrieval benchmark

488 MiniF2F tasks × 104 runs each = 50 752 Lean-REPL verified runs. SciLib-GRC21 vs LeanSearch / LeanFinder / LeanExplore.

MiniF2F — стандартный набор задач формальной математики (олимпиадные задачи IMO/AMC/AIME, базовые теоремы), переведённый сообществом в Lean4. Задачи короткие, тематически разнообразные, часто требуют нестандартного сочетания лемм — что делает MiniF2F хорошим тестом для систем подбора посылок.

Постановка

Все 488 задач прогнаны через четыре пайплайна (SciLib-GRC21, LeanSearch, LeanFinder, LeanExplore) при 104 различных конфигурациях (режимы поиска, top-k, профили признаков). Итого 50 752 запуска. Каждый прогон верифицируется через Lean REPL (Mathlib v4.28.0-rc1).

Стратификация задач (по pass@1 baseline без подсказок)

  • impossible (186, 38%): A0 = 0% — задачи, которые базовая Lean-модель не решает даже с идеальными подсказками.
  • hard (59, 12%): A0 = 1–25% — partial-capability tasks, критическая зона улучшения.
  • sweet (29, 6%): A0 = 25–75% — где подсказки чувствительны.
  • easy (214, 44%): A0 ≥ 75% — задачи решаются почти всегда.

Главный результат на hard-страте (59 задач)

  • A0 (без подсказок) — 28.8%.
  • B1 (только векторный поиск Qdrant) — 37.9%.
  • SciLib-GRC21 (граф + векторная аугментация) — 48.9% · +20.1 п.п. к baseline.

Сравнение со SOTA Lean-поисковиками (все 488 задач)

СистемаPass@1 (все)Pass@1 (hard)p-value
LeanSearch47.9%6.2%0.032
LeanFinder48.8%7.3%0.100
LeanExplore47.0%5.7%0.001
SciLib-GRC2150.0%8.6%baseline

Воспроизводимость

Конфигурации, версии моделей, сиды и срез Mathlib зафиксированы. Прогон занимает около 12 часов на узле 32 vCPU + RTX 3090. Подробности — в карточке датасета MiniF2F Runs; полные логи доступны по запросу.

Metrics

{
  "benchmark": "MiniF2F",
  "tasks": 488,
  "total_runs": 50752,
  "methods": ["SciLib-GRC21", "LeanSearch", "LeanFinder", "LeanExplore"],
  "metric": "pass@1 with Lean REPL verification",
  "mathlib_version": "v4.28.0-rc1",
  "compute": "32 vCPU + RTX 3090, ~12h end-to-end",
  "stratification": {"impossible": 186, "hard": 59, "sweet": 29, "easy": 214}
}

← To the lab