🏅 Ещё одна золотая медаль для ИИ на Международной математической олимпиаде (IMO)!

Стартап Harmonic запустил чат‑бота Aristotle — ИИ, который получил золото на IMO‑2025, решая задачи в формализованном виде.

📱 Aristotle уже доступен в приложении (iOS и Android). Он не просто решает задачи — он гарантирует отсутствие галлюцинаций в своих ответах, потому что все решения формально проверяются.

🧠 Фокус модели — на задачах количественного мышления (математика, логика и т.д.)

💰 Harmonic недавно привлек $100M инвестиций и уже оценён в $875M. Их цель — создать математический суперинтеллект.

И да, основатель Harmonic — это CEO Robinhood Влад Тенев.

🔥 Прямо сейчас это, возможно, самый надёжный ИИ для точных наук.

Получи грант до 1,65 млн ₽ на высшее образование в ведущем ИТ-университете по специальности «Безопасность информационных систем»

Стань белым хакером и начни зарабатывать 200к+ уже через 2 года обучения!

НЕЙМАРК — ИТ-университет нового поколения:
1) реальные стажировки в технологических гигантах: Яндекс, ВК, Сбер, Альфа-Банк и другие
2) возможность запустить стартап при поддержке наставников во время обучения
3) освоение криптографии, пентестинга, анализа уязвимостей, а также принципа разработки защищённого ПО
4) 2 диплома: НГТУ им. Алексеева и НЕЙМАРК
5) отсрочка от армии 
6) суперсовременные общежития в центре города

Узнай, как учиться бесплатно в лучшем ИТ-университете НЕЙМАРК — переходи в бот и забирай инструкцию! 

Реклама. НЕЙМАРК, УНИВЕРСИТЕТ НЕЙМАРК. ИНН 5256209106.

📈 Как повысить точность LLM в задачах по математике?

Новая статья показывает: если дать модели примеры на двух уровнях, можно поднять точность на 16% даже для моделей с 8B параметров.

🧠 Что делают авторы:
1. Разбивают задачу на 3 ключевых элемента: тип, ключевые термины и метод решения. Это называют "conceptual unit".
2. По ним находят похожие задачи с решениями — и вставляют в промпт.
3. Во время поиска (MCTS) модель на каждом шаге сравнивает своё решение с мини-базой реальных фрагментов решений.
4. Специальная reward-модель оценивает шаги и направляет дерево в сторону осмысленных решений.

📊 Результаты:
— LLaMA‑3.1‑8B: с 46.6% до 52.5% на OlympiadBench
— Qwen2‑7B: до 60.6%
— Прирост точности сохраняется при увеличении пула примеров, но время почти не растёт (+5%)

⚠️ Если убрать один из уровней (примеры до поиска или во время) — прирост снижается вдвое. Оба уровня работают только вместе.

📄 arxiv.org/abs/2507.05557

🎯 Одна из самых красивых идей в математике — вычисление площади фигуры с помощью случайных точек

Не верится, что такое возможно?
Смотри на анимацию ниже: мы бросаем случайные точки в квадрат и считаем, сколько из них попали в круг.
Так можно приближённо вычислить площадь круга — а значит и значение π!

🔍 Как это работает:
1. Берём квадрат, в который вписан круг (например, единичный)
2. Бросаем N случайных точек в квадрат
3. Считаем, сколько из них попало внутрь круга
4. Отношение количества «внутренних» точек к общему числу даёт приближение площади круга

👉 Это называется метод Монте‑Карло — простой, но мощный инструмент для численных приближений.

@data_math

#math #geometry #π #montecarlo #visualmath

🧠 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 внутри архива.

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

📌 StepFun-Prover-Preview-7B & 32B — LLM для формального доказательства теорем с интеграцией внешних инструментов

Модели используют обучение с подкреплением и обратную связь от окружения для эффективной генерации доказательств в Lean 4.

🔥 7B — на уровне DeepSeek-Prover-V2-671B и Kimina-Prover-72B на тесте miniF2F (pass@1)
💡 32B — опережает всех известных аналогов на 4%+ (miniF2F, pass@1)
📈 Человеко-подобное уточнение доказательств
🛠 Отлично подходит для исследователей, развивающих математическое мышление моделей

- HuggingFace: https://huggingface.co/stepfun-ai/StepFun-Prover-Preview-32B
- GitHub:https://github.com/stepfun-ai/StepFun-Prover-Preview

#StepFun #FormalTheoremProving #AI4Math