🧠 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

💥 Китайская AI-модель по математике — абсолютный прорыв

Свежая научная статья из Китая показала не просто сильную, а *лучшую в мире* AI-модель для решения олимпиадных задач по математике:

🏅 Модель взяла золото на IMO 2025
📈 Решает 78% всех задач прошлых IMO
🧠 Покрывает более 50% задач Putnam
✅ Даёт 100% точность на miniF2F (тест от OpenAI)
⚔️ Обходит AlphaGeometry2 от Google

📌 Как работает:
- Использует формальные доказательства на языке Lean
- МОдель открыл новые методы для решения геометрии, которых раньше не было
- Первая лаборатория, которая опубликовала полноценную статью о внутренностях модели

AI в математике выходит на новый уровень — и Китай сейчас показывает, что он идет в авангарде открытий.

📌 Статья

@machinelearning_interview

📸 Разработчик запустил свой код на сервере, имея лишь возможность изменения содержимого комментария в Python-скрипте

Участник соревнования UIUCTF 2025 обошёл ограничения задачи, где можно было изменять только содержимое комментария в Python-скрипте и подробно рассказал об этом. Вместо поиска уязвимостей в парсере, он использовал особенность интерпретатора — выполнение ZIP-архивов как Python-кода.

Секрет в структуре ZIP-файлов: Python ищет метаданные в конце архива, что позволило вставить архив в комментарий, сохранив валидность исходного скрипта. При запуске такого скрипта выполнялся код из main.py внутри архива.

🔗 Ссылка - *клик*