🌟DeepSeek-Prover: Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search.

DeepSeek-Prover-V1.5 - набор из языковых моделей для доказательства теорем в Lean 4.
"V1.5" означает обновление DeepSeek-Prover-V1 с некоторыми ключевыми нововведениями.

Во-первых, процесс обучения: предварительная подготовка на базе DeepSeekMath, затем контрольная работа с набором данных, включающим логические комментарии на естественном языке и код Lean 4. Это устраняет разрыв между рассуждениями на естественном языке и формальным доказательством теоремы. В набор данных также входит информация о промежуточном тактическом состоянии, которая помогает модели эффективно использовать обратную связь с компилятором.

Во-вторых, проводится обучение с подкреплением, используя алгоритм GRPO для изучения обратной связи с помощником по проверке. Тут выравнивается соответствие модели формальным спецификациям системы проверки.

В-третьих, RMaxTS, варианте поиска в дереве по методу Монте-Карло. Он присваивает встроенные вознаграждения на основе изучения тактического пространства состояний, побуждая модель генерировать различные пути доказательства. Это приводит к более обширному исследованию пространства доказательств.

В результате получился набор моделей с абсолютной точностью генерации в 46,3% на тестовом наборе miniF2F. Этот показатель лучше, чем у GPT-4 и моделей RL, специализирующихся на доказательстве теорем.

Набор DeepSeek-Prover:

🟠DeepSeek-Prover-V1.5 Base. Идеально подходит для первоначального изучения и понимания возможностей модели и основ для формальных математических рассуждений, но требует дальнейшего обучения для оптимальной работы;
🟠DeepSeek-Prover-V1.5 SFT. Модель для задач, требующих умеренных навыков доказательства теорем за счет рассуждений на естественном языке и информации о тактическом состоянии.
🟠DeepSeek-Prover-V1.5 RL. Рекомендуется для решений, требующих высочайшей точности и производительности при формальном доказательстве теорем. К SFT-версии добавлены дополнительная оптимизация на основе Proof Assistant Feedback и обучение с подкреплением.

▶️Установка и запуск:

# Clone the repository:
git clone --recurse-submodules git@github.com:deepseek-ai/DeepSeek-Prover-V1.5.git
cd DeepSeek-Prover-V1.5

# Install dependencies:
pip install -r requirements.txt

# Build Mathlib4:
cd mathlib4
lake build

# Run paper experiments:
python -m prover.launch --config=configs/RMaxTS.py --log_dir=logs/RMaxTS_results

📌Лицензирование кода репозитория: MIT license

📌Лицензирование моделей: DEEPSEEK License


🟡Набор моделей
🟡Arxiv
🟡Датасет
🟡Сообщество в Discord
🖥Github [ Stars: 53 | Issues: 0 | Forks: 1]


@ai_machinelearning_big_data

#AI #LLM #Math #ML

🌟 OpenMathInstruct-2: математический датасет и набор моделей от NVIDIA.

OpenMathInstruct-2 состоит из 14 млн. пар "вопрос-решение" (примерно 600 тысяч уникальных вопросов) и является одним из крупнейших общедоступных наборов данных для обучения LLM в математике.

Набор данных создан на основе Llama-3.1-405B-Instruct путем синтеза решений для существующих вопросов из наборов данных MATH и GSM8K и генерации новых задач и решений.

Результаты абляционных экспериментов, которые проводились для поиска оптимальных параметров синтеза, показали, что:

🟢формат решения имеет значение, причем чрезмерно подробные решения негативно сказываются на производительности модели;

🟢данные, сгенерированные сильной моделью-учителем, превосходят по качеству данные, полученные от более слабой модели;

🟢процесс обучения устойчив к наличию до 20% решений низкого качества;

🟢разнообразие вопросов имеет решающее значение для масштабирования данных.

Итоговые данные, включенные в датасет прошли тщательную деконтаминацию с использованием конвейера lm-sys и ручной проверки на поиск дубликатов с тестовыми наборами данных.

OpenMathInstruct-2 показал высокую эффективность при обучении LLM.

Модель Llama3.1-8B-Base, обученная на OpenMathInstruct-2, превзошла Llama3.1-8B-Instruct на 15,9% по точности на наборе данных MATH, а OpenMath2-Llama3.1-70B обошла Llama3.1-70B-Instruct на 3,9%.

Датасет выпущен в 3-х размерностях: полный набор (примерно 7.5 GB) и уменьшенные версии train_1M (640 Mb), train_2M (1.3 Gb) и train_5M (3.1 Gb).

▶️ Модели, дообученные на этом датасете:

🟠OpenMath2-Llama3.1-70B, в формате Nemo, квантованные версии GGUF (от 3-bit до 8-bit);

🟠OpenMath2-Llama3.1-8B, в формате Nemo, квантованные версии GGUF (от 2-bit до 8-bit).


📌Лицензирование датасета : CC-BY-4.0 License.

📌Лицензирование моделей: Llama 3.1 Community License.


🟡Набор моделей
🟡Arxiv
🟡Датасет


@ai_machinelearning_big_data

#AI #ML #LLM #MATH #NVIDIA #Dataset

📌Как линейная алгебра может помочь при разработке web-приложения.

Интересная и познавательная статья разработчика Ивана Шубина о том, как он использовал матрицы для создания интерактивного редактора диаграмм Schemio.

Изначально, редактор позволял создавать простые фигуры и манипулировать ими, но с введением иерархии объектов возникла необходимость в сложных преобразованиях координат. Матрицы стали ключом к решению этой проблемы, позволяя эффективно управлять перемещением, вращением и масштабированием объектов.

Для преобразования глобальных и локальных координат между собой использовались матричные преобразования. Умножение матриц дало возможность комбинировать преобразования, а инверсия матрицы помогает переводить координаты из глобальных в локальные.

Иван подробно описывает, как матрицы помогают управлять поворотом и масштабированием объектов относительно опорной точки и как они используются при монтировании и демонтировании объектов, чтобы избежать нежелательных коллизий.

Таким образом, матричная математика стала решением для расширения возможностей редакторе Schemio.

🔜 Читать полную версию статьи

#Math #LinearAlgebra #Webdev

🌟 Математические датасет OpenMathReasoning и модели OpenMath-Nemotron - победители олимпиады AIMO-2.

NVIDIA представила новый подход к обучению моделей для сложных математических задач, заняв первое место в конкурсе Kaggle AIMO-2.

Секрет — в огромном датасете OpenMathReasoning, который состоит из 540 тыс. уникальных задач с Art of Problem Solving, 3,2 млн. многошаговых решений (CoT) и 1,7 млн. примеров с интеграцией кода (TIR).

Для сравнения: это в разы больше, чем в популярных аналогах MATH и GSM8K. Все это дополнено 566 тыс. примеров для обучения генеративному выбору решений (GenSelect) — методу, который лучше, чем классическое голосование большинством.

OpenMathReasoning создавался тщательно и ответственно. Сначала задачи фильтровались через Qwen2.5-32B, чтобы убрать простые или дублирующие бенчмарки. Затем DeepSeek-R1 и QwQ-32B генерировали решения, а итеративная тренировка с жесткой фильтрацией улучшала качество. Например, код в TIR-решениях должен был не просто проверять шаги, а давать принципиально новые вычисления — вроде перебора вариантов или численного решения уравнений.

Модели OpenMath-Nemotron (1,5B–32B параметров), обученные на этом наборе данных показали SOTA-результаты. 14B-версия в режиме TIR решает 76,3% задач AIME24 против 65,8% у базового DeepSeek-R1. А с GenSelect, который анализирует 16 кандидатов за раз, точность взлетает до 90%. Даже 1,5B-модель с GenSelect обгоняет 32B-гиганты в отдельных тестах.


📌Лицензирование: CC-BY-4.0 License.


🟡Набор моделей
🟡Arxiv
🟡Датасет
🖥GitHub


@ai_machinelearning_big_data

#AI #ML #Math #Dataset #NVIDIA

✔️ Deep Think в 2.5 Pro — интеллект, который учится думать по-настоящему.

Это не просто новая версия — это качественный скачок в способности ИИ к рассуждению.
Благодаря технологиям параллельного мышления, Deep Think анализирует сразу несколько возможных решений, прежде чем выбрать лучшее. Он размышляет не линейно, а как человек — сомневается, сравнивает, проверяет гипотезы.

📊 Результаты впечатляют:
Модель справляется с задачами, которые долгое время считались недостижимыми для машин.
Она набирает высокие баллы на USAMO 2025 — одном из самых сложных математических соревнований,
лидирует в LiveCodeBench — бенчмарке для кодинга уровня олимпиад,
и уверенно проходит MMMU, показывая 84% на тесте мультимодального мышления.

Gemini 2.5 Pro уже доступен в Jules — асинхронном агенте для кодинга, который справляется со сложными задачами в больших кодовых базах, на которые раньше уходили часы.

Он может планировать шаги, вносить изменения в файлы и многое другое — всего за несколько минут. ⏱️

Jules уже в публичной бета-версии → jules.google

✔️Еще команда DeepMind представила Gemini Diffusion: новый, подход в генерации текста. Вместо предсказания слов напрямую, модель создаёт ответы путём поэтапного уточнения шума — работает как искусственный «ремесленник», постепенно шлифуя результат.

Такой итеративный процесс особенно эффективен для задач программирования и математики, где требуется не просто единичный ответ, а быстрый цикл проб и корректировок. Модель способна многократно уточнять решения, улучшая их на каждом шаге, и демонстрирует впечатляющие результаты в этих областях.

Можно подать заявку в лист ожидания → https://goo.gle/44MwCW3

✔️ Google представили генератор видео Veo 3 — он генерирует видео сразу со звуком и даже с озвучкой э и липсинком.

Доступен с сегодняшнего дня в Gemini!

@ai_machinelearning_big_data


#GoogleIO #AI #DeepThink #Reasoning #Math #Code #Multimodal