🌟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

🌟 Lite Oute 2 Mamba2Attn: базовая и инструктивная SLM на архитектуре Mamba2.


OuteAI выпустила второе поколение легких моделей на 250М параметров каждая :

🟢 Lite Oute 2 Mamba2Attn 250M Base
🟢 Lite Oute 2 Mamba2Attn 250M-Instruct

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

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

Базовая модель была обучена на 30 миллиардах токенов из корпуса данных, структура которого - 50% датасета dclm-baseline-1.0 b 50% fineweb-edu. Инструктивная версия прошла дообучение с SFT и DPO.

Обе модели имеют 4 слоя внимания из общего количества 32, такая конфигурация позволяет минимизировать потери при проверке, что подтверждено исследованием о соотношении слоев самовнимания к MLP.

▶️ Рекомендованные параметры для Instruct - модели:

🟢Temperature: 0.1 - 0.4
🟢Repetition Penalty: 1.10 - 1.12

▶️Ограничения:

🟠Непоследовательная точность. Примите во внимание, что обе модели - малого размера, инференс в некорорых задачах может быть неполным или неточным;
🟠Отсутствие глубины контекста. В некоторых задачах, модели могут не соответствовать ожиданиям глубины запоминания контекста;
🟠Баланс лаконичности. Модель иногда испытывает трудности с балансом между краткостью и детализацией, давая либо слишком краткие ответы, либо излишне повторяя заданную информацию.


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


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


@ai_machinelearning_big_data

#AI #SLM #Mamba2 #ML #Oute

⚡️ Qwen2-VL: второе поколение VLM моделей от Alibaba Cloud.

Qwen2-VL - это новая версия VLMs, основанная на Qwen2 в семействе моделей Qwen. По сравнению предыдущим поколением, Qwen2-VL обладает возможностями:

🟢Распознавание изображений с различным разрешением и соотношением сторон;
🟢VQA-понимание видеороликов продолжительностью более 20 минут с поддержкой диалога;
🟢Интеграция с носимыми устройствами (мобильный телефон, робот и т.д) в качестве агента управления;
🟢Мультиязычность внутри входных данных, например на изображениях или видео.
🟢Улучшенное распознавание объектов и предметов;
🟢Расширенные возможности в области математики и понимания программного кода.

Набор Qwen2-VL состоит из трех основных моделей, две из которых публикуются в отrрытом доступе. Модель Qwen2-VL-72B доступна только по API:

🟠Qwen2-VL-72B;
🟢Qwen2-VL-7B-Instruct;
🟢Qwen2-VL-2B-Instruct,

и их квантованные версии в форматах AWQ и GPTQ в разрядностях Int8 и Int4.

Архитектура моделей. как и в прошлом поколении основана на ViT 600M и LLM Qwen2, но с добавлением двух ключевых модификаций:

🟠использование NDR (Naive Dynamic Resolution), который позволил обрабатывать входные данные любого разрешения, преобразуя их в динамическое количество визуальных токенов. Эта реализация максимально близка к имитации зрительного восприятия человека.

🟠технология Multimodal Rotary Position Embedding (M-ROPE). Благодаря деконструкции оригинального rotary embedding на три части, представляющие временную и пространственную информацию, M-ROPE дает возможность LLM одновременно захватывать 1D( текст ), 2D( визуал ) и 3D( видео ) информацию.

⚠️ Ограничения в возможностях и слабые стороны поколения состоят в том, что модели не умеют извлекать звук из видео, а их знания актуальны на июнь 2023 года.

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

▶️Использование и интеграция Qwen2-VL возможна с инструментами и на фреймворках: Transformers, vLLM, Llama-Factory, AutoGPTQ, AutoAWQ.


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


🟡Страница проекта
🟡Набор моделей
🟡Demo
🟡Сообщество в Discord
🖥Github [ Stars: 59 | Issues: 3 | Forks: 2]


@ai_machinelearning_big_data

#AI #Qwen #ML #GPTQ #VLM #AWQ

🌟 Автоматическое проектирование агентов 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