🌟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

⚡️ Qwen2.5 Family: Релиз Qwen2.5, Qwen2.5-Coder и Qwen2.5-Math.

Команда разработки Qwen (Alibaba Group) опубликовала большой релиз нового поколения моделей - Qwen2.5, специализированные модели: Qwen2.5-Coder, Qwen2.5-Math, их инструктивные и квантованные версии, анонсированы закрытые Qwen-Plus и Qwen-Turbo.

Вместе с релизом нового поколения 2.5 в отрытый доступ опубликована Qwen2-VL-72B-Instruct предыдущего поколения.

▶️ Qwen2.5

В дополнение к традиционным вариантам с 0,5-1,5-7-72 млрд параметров, Qwen2.5 предлагает две новые модели среднего размера 14 млрд и 32 млрд параметров и компактную модель 3 млрд параметров.

Qwen2.5 обучались на увеличенном и улучшенном наборе данных размером в 18 трлн токенов.

Значительно расширены знания моделей: возможности в области программирования,
усовершенствованы математические способности Qwen2.5, повышено соответствие ответов модели предпочтениям человека: следование инструкциям, генерация длинных текстов (до 8 тыс. токенов), понимание структурированных данных и генерация структурированных выводов (в частности, JSON).

Список моделей:

🟢Qwen2.5: 0.5B, 1.5B, 3B, 7B, 14B, 32B, 72B;

🟢Qwen2.5-Instruct: 0.5B, 1.5B, 3B, 7B, 14B, 32B, 72B;

🟢Qwen2.5-Instruct: все варианты в форматах GPTQ, AWQ, GGUF.

В дополнение к этим моделям открыт доступ по API для флагманских моделей: Qwen-Plus и Qwen-Turbo через Model Studio.

▶️ Qwen2.5 Coder

Qwen2.5-Coder доступна в трех размерах: 1,5 млрд, 7 млрд и 32 млрд параметров (последняя появится в ближайшее время). Обновление состоит из двух основных улучшений: больше объем обучающих данных и расширение возможностей программирования в общих задачах и в математике.

Модели обучались на массиве данных объемом 5,5 триллиона токенов, включающем исходный код, данные для сопоставления текста и кода и синтетические данные.

Qwen2.5-Coder поддерживает до 128 тысяч токенов контекста, знает 92 языка программирования и выполняет операции по генерации кода, автодополнению и исправлению кода.

Qwen2.5-Coder-Instruct имеет способность к обобщению, знает более 40 языков программирования, справляется с задачами, связанными с логическим мышлением в коде, и показывает высокие результаты в задачах, связанных с математическим мышлением.

Список моделей:

🟠Qwen2.5-Coder: 1.5B, 7B;

🟠Qwen2.5-Coder-Instruct: 1.5B, 7B;

🟠Qwen2.5-Coder-Instruct в формате GGUF: 1.5B, 7B.


▶️ Qwen2.5 Math

Qwen2.5-Math обучались на корпусе математических данных Qwen Math Corpus v2, который содержит более 1 трлн. токенов.

Помимо базовых моделей, серия Qwen2.5-Math включает в себя инструктивные модели: Qwen2.5-Math-Instruct и модель математического вознаграждения, Qwen2.5-Math-RM-72B.

Qwen2.5-Math-Instruct обучалась с использованием данных CoT и TIR на китайском и английском языках, а также данных SFT, созданных с использованием Qwen2.5-Math-RM-72B.

Список моделей:

🟠Qwen2.5-Math: 1.5B, 7B, 72B, RM-72B;

🟠Qwen2.5-Math-Instruct: 1.5B, 7B, 72B.


▶️ Вместе с релизом Qwen2.5, опубликована Qwen2-VL-72B-Instruct и ее квантованные Int8 и Int4 версии в форматах GPTQ, AWQ.


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

🟢Apache 2.0 для всех base и instruct моделей, кроме 3B и 72B.
🟠Qwen2.5-3B - Qwen Research License.
🟠Qwen2.5-72B и Qwen2.5-Math-72B - Qwen License.



🟡Страница проекта
🟡Коллекция моделей на HF
🟡Demo Qwen2.5-Instruct-72B
🟡Demo Qwen2.5-Coder-Instruct-7B
🟡Demo Qwen2.5-Math
🟡Сообщество в Discord
🖥Github


@ai_machinelearning_big_data

#AI #ML #LLM #Qwen

🌟 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

🌟 Llama-3.1-Centaur-70B: модель симуляции поведения человека.

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

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

Centaur создана на основе Llama 3.1 70B и дообучена на наборе данных Psych-101, включающем данные 60 000 участников, давших суммарно 10 000 000 ответов в 160 психологических экспериментах.

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

Centaur дообучалась методом QLoRA: к каждому слою базовой Llama 3.1 70B были добавлены низкоранговые адаптеры, при этом параметры базовой модели остались неизменными.

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

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

Кроме того, Centaur обобщает знания на "незнакомые" ситуации, которые не входили в датасет обучения: точно предсказывает поведение при измененных формулировках задач, структурах проблем и даже в совершенно новых областях.

Важный результат экспериментального тестирования - соответствия внутренних представлений Centaur нейронной активности человека.

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

⚠️ Centaur обучена на наборе данных, в котором выбор человека выражается символами "<<" и ">>".
Для оптимальной работы рекомендуется соответствующим образом настроить промпты.

⚠️ Модель запускается на 80 GB GPU.


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

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


🟡Модель
🟡Техотчет
🟡Датасет


@ai_machinelearning_big_data

#AI #ML #LLM #Centaur

🌟 OLMo 2: Новое поколение полностью открытых языковых моделей.

OLMo 2 - серия открытых языковых моделей, созданная для развития науки о языковых моделях .

Модели OLMo 2 доступны в вариантах 7B и 13B параметров и обучены на массиве данных объемом 5 трлн. токенов. Они демонстрируют производительность, сопоставимую или превосходящую аналогичные по размеру полностью открытые модели на английских академических тестах.

Разработчики OLMo 2 уделили особое внимание стабильности обучения, используя методы RMSNorm, QK-Norm, Z-loss регуляризация и улучшенная инициализация.

Обучение проводилось в 2 этапа. На первом этапе модели обучались на датасете OLMo-Mix-1124 (3,9 трлн. токенов). На втором этапе использовался специально подобранный набор данных Dolmino-Mix-1124 (843 млрд. токенов), состоящий из веб-данных, материалов из академических источников, форумов вопросов и ответов, инструкций и математических задачников. Для объединения моделей, обученных на разных подмножествах данных, применялся метод "model souping".

Для оценки OLMo 2 была разработана система OLMES (Open Language Modeling Evaluation System) из 20 тестов для измерения способностей модели. OLMo 2 превзошел предыдущую версию OLMo 0424 по всем задачам и показал высокую эффективность по сравнению с другими открытыми моделями.

▶️Набор моделей OLMo 2:

🟢Базовые модели: OLMo-2-1124-7B и OLMo-2-1124-13B

🟠GGUF-версии: OLMo-2-1124-7B-GGUF и OLMo-2-1124-13B-GGUF

🟢Инструктивные версии: OLMo-2-1124-7B-Instruct и OLMo-2-1124-13B-Instruct

🟠DPO-версии: OLMo-2-1124-7B-DPO и OLMo-2-1124-13B-DPO

🟠SFT-версии: OLMo-2-1124-7B-SFT и OLMo-2-1124-13B-SFT

🟠Reward Model - версия OLMo-2-1124-7B-RM


▶️Пример инференса OLMo-2-7B c HF Transformers:

from transformers import AutoModelForCausalLM, AutoTokenizer
olmo = AutoModelForCausalLM.from_pretrained("allenai/OLMo-2-1124-7B")
tokenizer = AutoTokenizer.from_pretrained("allenai/OLMo-2-1124-7B")
message = ["Language modeling is "]
inputs = tokenizer(message, return_tensors='pt', return_token_type_ids=False)
# optional verifying cuda
# inputs = {k: v.to('cuda') for k,v in inputs.items()}
# olmo = olmo.to('cuda')
response = olmo.generate(**inputs, max_new_tokens=100, do_sample=True, top_k=50, top_p=0.95)
print(tokenizer.batch_decode(response, skip_special_tokens=True)[0])

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


🟡Страница проекта
🟡Набор моделей
🟡Demo
🖥GitHub


@ai_machinelearning_big_data

#AI #ML #LLM #OLMo2

🌟 EXAONE 3.5: Набор инструктивных моделей от LG AI.

LG AI Research опубликовала 3 новые инструктивные двуязычные (английский и корейский) модели EXAONE 3.5 с контекстным окном в 32 тыс. токенов:

🟠2.4B – компактная модель для использования на устройствах;,
🟠7.8B – универсальная модель;
🟢32B – высокопроизводительная модель для задач, требующих максимальной эффективности.

Разработчики EXAONE 3.5 улучшили эффективность обучения моделей. На этапе предварительного обучения из наборов данных удалялись дубликаты и личная информация, что позволило повысить качество ответов моделей и оптимизировать использование ресурсов. На этапе постобработки применялись методы SFT и DPO, чтобы улучшить способность моделей понимать инструкции и предпочтения пользователей.

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

К каждой модели, LG AI выпустил квантованные версии в форматах AWQ и GGUF.

⚠️ EXAONE 3.5 - инструктивные модели, поэтому рекомендуется использовать системные промпты, представленные в примере кода инференса.

▶️Пример инференса EXAONE-3.5-7.8B-Instruct на Transformers:

import torch
from transformers import AutoModelForCausalLM, AutoTokenizer

model_name = "LGAI-EXAONE/EXAONE-3.5-7.8B-Instruct"

model = AutoModelForCausalLM.from_pretrained(
    model_name,
    torch_dtype=torch.bfloat16,
    trust_remote_code=True,
    device_map="auto"
)
tokenizer = AutoTokenizer.from_pretrained(model_name)

prompt = "%Prompt%" 

messages = [
    {"role": "system", "content": "You are EXAONE model from LG AI Research, a helpful assistant."},
    {"role": "user", "content": prompt}
]
input_ids = tokenizer.apply_chat_template(
    messages,
    tokenize=True,
    add_generation_prompt=True,
    return_tensors="pt"
)

output = model.generate(
    input_ids.to("cuda"),
    eos_token_id=tokenizer.eos_token_id,
    max_new_tokens=128,
    do_sample=False,
)
print(tokenizer.decode(output[0]))

📌Лицензирование: EXAONE AI Model License.


🟡Статья
🟡Набор моделей
🟡Demo 7.8B
🟡Arxiv
🖥GitHub


@ai_machinelearning_big_data

#AI #ML #LLM #EXAONE #LG

🌟 Bamba-9B: эффективная Hybrid Mamba2 модель.

Bamba-9B - модель, разработанная IBM, Princeton, CMU и UIUC на основе полностью открытых данных. Модель демонстрирует улучшение пропускной способности в 2.5 раза и снижение задержки инференса в 2 раза по сравнению с Transformers в vLLM. Bamba-9B доступна для использования в HF Transformers, vLLM, TRL и llama.cpp.

Bamba-9B использует уникальный распределенный, не сохраняющий состояние data loader, обеспечивающий бесшовное возобновление работы, автоматическое масштабирование, потоковую передачу данных с zero-overhead for shuffling.

Модель основана на архитектуре NVIDIA hybrid Mamba2, но с некоторыми изменениями. Bamba-9B имеет 32 слоя, из которых 3 полноценных слоя внимания и 29 слоев Mamba2, в то время как NVIDIA hybrid Mamba2 имеет 29 слоев, из которых 4 слоя внимания и 25 слоев Mamba2.

Bamba-9B была обучена на 2.2T токенов с датасетом Dolma v1.7 на первом этапе и FineWeb-edu и Cosmopedia на втором.

По проведенным замерам, средняя производительность Bamba-9B почти сравнима с Llama 3.1 8B (45.53 против 44.68), при том что Llama 3.1 8B была обучена на 7x большем объеме данных.

Bamba-9B превзошла Olmo 7B, обученную на идентичном количестве токенов и наборах данных. В сравнении с другими моделями на базе Mamba/Mamba2, Bamba-9B показывает хорошие результаты, при этом обеспечивая значительное улучшение (до 5x) эффективности логического вывода.

▶️ Планы разработчиков на дальнейшее развитие Bamba:

🟠увеличение длины контекста модели Bamba-9B (сейчас - 4096);
🟠улучшение модели путем обучения на дополнительных данных и точной настройки на наборах данных SFT.

▶️ Опубликованный набор моделей:

🟢Bamba 9B - финальная версия модели после 2-х этапов обучения
🟢Bamba 9B 2T - чекпоинт после 1 этапа трейна с датасетом Dolma v1.7
🟠Bamba 9B 1.8T - промежуточный чекпоинт 1 этапа обучения

🟢Bamba 9B FP8 - квантованная с помощью llm-compressor версия Bamba 9B
🟢Bamba 9B 2T FP8 - квантованная с помощью llm-compressor версия Bamba 9B 2Т
🟠Bamba 9B 1.8T FP8 - квантованная с помощью llm-compressor версия Bamba 9B 1.8Т

▶️Пример инференса на Transformers с Bamba-9B:

from transformers import AutoModelForCausalLM, AutoTokenizer

model = AutoModelForCausalLM.from_pretrained("ibm-fms/Bamba-9B")
tokenizer = AutoTokenizer.from_pretrained("ibm-fms/Bamba-9B")

message = ["Mamba is a snake with following properties  "]
inputs = tokenizer(message, return_tensors='pt', return_token_type_ids=False)
response = model.generate(**inputs, max_new_tokens=64)
print(tokenizer.batch_decode(response, skip_special_tokens=True)[0])

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


🟡Статья
🟡Набор моделей
🖥GitHub


@ai_machinelearning_big_data

#AI #ML #LLM #Bamba #IBM