🌟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

⚡️ Hermes 3: Семейство finetune Llama 3.1 от Nous Research

Новый набор моделей от Nous Research был создан на основе Llama 3.1 8B, 70B и 405B файнтюном датасета из синтетически сгенерированных ответов. Hermes 3 получил производительность Llama 3.1 и расширенные возможности в мышлении и творчестве.

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

В Hermes 3 возникают аномальные состояния, которые при правильных вводных и пустых системных подсказках приводят к ролевой игре и потере памяти. Вы можете активировать этот “Режим амнезии” в Hermes 3 405B, введя пустой системный запрос и отправив сообщение "Кто вы?".

Hermes 3 использует ChatML для формата промптов. Формат более сложный, чем alpaca или sharegpt, в нем используются специальные токены для обозначения начала и окончания логического контекста и ролей в этих контекстах.

Набор Hermes 3:

🟠Hermes 3 - Llama-3.1 405B;
🟠Hermes 3 - Llama-3.1 405B FP8 для использования с vLLM;
🟠Hermes 3 - Llama-3.1 70B;
🟠Hermes 3 - Llama-3.1 70B FP8 для использования с vLLM;
🟢Hermes 3 - Llama-3.1 70B GGUF для использования с llama.cpp. Версии квантования от 3-bit (31 Gb) до 5-bit (50 GB);
🟠Hermes 3 - Llama-3.1 8B;
🟢Hermes 3 - Llama-3.1 8B GGUF для использования с llama.cpp. Версии квантования от 4-bit (5 Gb) до 8-bit (9 GB);

📌Лицензирование : Llama 3 Community License


🟡Страница проекта
🟡Сообщество в Discord
🟡Набор моделей
🟡Arxiv
🟡Demo



@ai_machinelearning_big_data

#AI #Hermes3 #LLM #ML

🌟 Автоматическое проектирование агентов LLM

Развитие базовых языковых и иснтруктивных моделей , таких как GPT и Claude, дал возможность создания агентов общего назначения, способных к гибкому рассуждению и планированию. Но разработка этих агентов часто требует ручной настройки и значительных усилий со стороны инженеров и ресерчеров.

Для упрощения процесса проектирования агентов появилось новое направление исследований — автоматизированное проектирование агентных систем (Automated Design of Agentic Systems, ADAS).
Главное назначение методологии ADAS - автоматизация создания новых агентных блоков и их объединение в сложные системы.

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

Поисковый алгоритм с помощью мета-агента является ярким примером ADAS в действии. Он использует мета-агента, который по сути является LLM, для итеративного проектирования новых агентов на основе постоянно растущего архива результатов предыдущих поисков.

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

Благодаря обширным экспериментам в областях программирования, науки и математики, алгоритм демонстрирует способность изобретать агентов с новыми проектами, которые превосходят современных агентов, разработанных вручную.

Один из реализованных проектов ADAS в практической среде - использование алгоритма Meta Agent Search в связке с GPT:

# Create Conda venv:
conda create -n adas python=3.11

# Activate venv:
conda activate adas

#Install Dependencies:
pip install -r requirements.txt

# Set OpenAI API Key:
export OPENAI_API_KEY="YOUR KEY HERE"

Запуск Meta Agent Search на примере области поиска "arc":

# Navigate to _arc folder:
cd _arc

# Run Meta Agent Search
python search.py

📌Лицензирование : Apache 2.0 license



🟡Страница проекта
🟡Arxiv
🖥Github [ Stars: 484 | Issues: 4 | Forks: 53]


@ai_machinelearning_big_data

#AI #LLM #Agents #ML #ChatGPT