🌟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 [email protected]: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