🧠 StepFun‑Prover Preview: 32B‑модель обучилась доказывать теоремы, общаясь с Lean 4

📌 Что делает классический prover :
Он просто перебирает возможные доказательства, не зная, в каком направлении двигаться. Это как угадывать код на замке: пробуешь один вариант, не подошло — пробуешь следующий.

📌 Что делает новая модель StepFun‑Prover)
Она "разговаривает" с Lean 4 — проверяющей системой формальных доказательств. Если модель предлагает доказательство и Lean выдает предупреждение или ошибку, модель читает это как обратную связь и учится. В следующий раз она делает более точную попытку.

🧠 В итоге:

Вместо перебора 30+ вариантов вслепую, как у обычных систем, модель с первого раза решает до 70 % задач, потому что понимает и учитывает отклик от системы.

Это как решать задачу в школе, где тебе не просто говорят «неправильно», а объясняют, что именно не так — и ты быстро учишься.

🔍 Как это работает:
- Исходные задачи из Lean очищаются и превращаются в набор для обучения синтаксису и вызовам тактик.
- На этих данных обучаются 7B и 32B‑модели на базе DeepSeek, с последующей правкой ошибок Kimina‑Prover.
- Модель учится смешивать обычный текст, код на Lean и sandbox‑ответы — всё в одном длинном контексте.
- Вознаграждение бинарное: если Lean-программа принимает доказательство — 1, иначе — 0.

📈 Результат:
- 32B‑модель обходит конкурентов на 72B более чем на 5 % (при этом использует **1 попытку вместо 32**).
- Увеличение длины контекста с 4K до 20K токенов повышает pass@1 с 58 % до 70 %.
- Модель сокращает доказательства, читая варнинги и на лету рефакторя тактики.

📦 Open‑веса (7B и 32B) выйдут скоро — можно будет запускать даже на скромном GPU.

📄 Paper: https://arxiv.org/abs/2507.20199