DeepSeek-Prover-V1.5 - набор из языковых моделей для доказательства теорем в Lean 4.
"V1.5" означает обновление DeepSeek-Prover-V1 с некоторыми ключевыми нововведениями.
Во-первых, процесс обучения: предварительная подготовка на базе DeepSeekMath, затем контрольная работа с набором данных, включающим логические комментарии на естественном языке и код Lean 4. Это устраняет разрыв между рассуждениями на естественном языке и формальным доказательством теоремы. В набор данных также входит информация о промежуточном тактическом состоянии, которая помогает модели эффективно использовать обратную связь с компилятором.
Во-вторых, проводится обучение с подкреплением, используя алгоритм GRPO для изучения обратной связи с помощником по проверке. Тут выравнивается соответствие модели формальным спецификациям системы проверки.
В-третьих, RMaxTS, варианте поиска в дереве по методу Монте-Карло. Он присваивает встроенные вознаграждения на основе изучения тактического пространства состояний, побуждая модель генерировать различные пути доказательства. Это приводит к более обширному исследованию пространства доказательств.
В результате получился набор моделей с абсолютной точностью генерации в 46,3% на тестовом наборе miniF2F. Этот показатель лучше, чем у GPT-4 и моделей RL, специализирующихся на доказательстве теорем.
Набор DeepSeek-Prover:
# 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
@ai_machinelearning_big_data
#AI #LLM #Math #ML
Please open Telegram to view this post
VIEW IN TELEGRAM
Please open Telegram to view this post
VIEW IN TELEGRAM
Forwarded from Machinelearning
Новый набор моделей от 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:
@ai_machinelearning_big_data
#AI #Hermes3 #LLM #ML
Please open Telegram to view this post
VIEW IN TELEGRAM
Please open Telegram to view this post
VIEW IN TELEGRAM
Llama-3.1-Minitron-4B-Width-Base - это базовая текстовая модель, которая может быть адаптирована для различных задач генерации естественного языка.
Она получена путем обрезки (pruning) Llama-3.1-8B за счет сокращения размера эмбеддинга, количества attention heads и промежуточной размерности MLP.
После было выполнено продолженное обучение с дистилляцией, используя набор данных размером 94 миллиарда токенов.
Корпус обучения (набор данных) модели Llama-3.1-Minitron-4B-Width-Base включает английские и многоязычные тексты, код и другие письменные материалы.
Источники данных охватывают различные области: право, математика, наука, финансы. Для улучшения производительности режима "чата", в процессе обучения были добавлены данные в формате вопрос-ответ.
Дата актуальности корпуса обучения - июнь 2023 года.
При создании были использованы техники Grouped-Query Attention (GQA) и Rotary Position Embeddings (RoPE).
Архитектурные характеристики:
⚠️ На момент публикации, поддержка Llama-3.1-Minitron-4B-Width-Base в Hugging Face Transformers находится на рассмотрении.
Для использования модели выполните рекомендованные разработчиками инструкции или запустите модель в NeMo v.24.05
Есть неофициальные квантованные GGUF - версии модели в семи разрядностях, от 2-bit (1. 84Gb) до 16-bit (9.03 Gb).
@ai_machinelearning_big_data
#AI #NVIDIA #LLM #ML #Minitron
Please open Telegram to view this post
VIEW IN TELEGRAM
Please open Telegram to view this post
VIEW IN TELEGRAM
Clapper - это инструмент визуализации историй, разрабатываемый как пет-проект сотрудником Huggingface Julian Bilcke
Созданный год назад, Clapper не предназначен для замены традиционных видеоредакторов или AI-редакторов, использующих 3D-сцены в качестве исходного материала.
Философия Clapper заключается в том, чтобы каждый мог создавать видео с помощью GenAI-инструментов посредством интерактивного, итеративного и интуитивного процесса, без необходимости использования разных интерфейсов, навыков режиссуры или AI-инженерии.
В Clapper вы не редактируете последовательность видео- и аудиофайлов напрямую, а итерируете (с помощью вашего помощника ИИ) свою историю, используя высокоуровневые абстракции, такие как персонажи, места, погода, временной период, стиль и т. д.
Конечной целью проекта заявлен полностью режиссерский режим, с которым вы можете просто перевести видео в полноэкранный режим, удобно расположиться в режиссерском кресле (или на диване) и, произнося голосом команды своему AI-ассистенту для создания вашего фильма, насладитесь созданным лично Вами шедевром.
⚠️ Это альфа-версия инструмента, который разрабатывают 3 человека. Не стоит ожидать от этого открытого проекта революционных результатов.
Clapper поддерживает интеграцию по API с локальными системами (ComfyUI) и он-лайн сервисами:
HuggingFace, Replicate, ComfuICU, FalAI, ModelsLab, OpenAI, Groq, Google, Anthropic, Cohere, MistralAI, StabilityAI, ElevenLabs, KitsAI.
Проект написан на TypeScript. Необходимые условия перед установкой:
# Install the dependencies:
# --include=optional to make
# sure deps are installed
bun i
# build the app:
npm run build
# Running the web app:
bun run dev
# first time you go to localhost:3000
# Wait around 1 minute, the app will compile
cd packages/app
bun run electron:start
# You can also build Clapper:
cd packages/app
bun run electron:make
@ai_machinelearning_big_data
#AI #Storytelling #Clapper #Visialtool
Please open Telegram to view this post
VIEW IN TELEGRAM
Please open Telegram to view this post
VIEW IN TELEGRAM
Экосистема Fluх развивается очень быстро, каждый день появляются новые способы, решения, возможности и инструменты для работы с моделями Fluх онлайн и оффлайн.
Теперь у сообщества FLUX появился обновляемый и упорядоченный Awesome FLUX!
https://awesomeflux.com/
@ai_machinelearning_big_data
#AI #FLUX #ML #Awesome
Please open Telegram to view this post
VIEW IN TELEGRAM
Salesforce AI Research представила XGen-MM (BLIP-3) - коллекцию из 4 моделей на основе phi3-mini-instruct с улучшенным обучением и повышенной, согласно бенчмаркам претрейна, производительностью.
XGen-MM (BLIP-3) может использоваться в различных областях - от обработки естественного языка до компьютерного зрения. Он способен понимать сложные, мультимодальные входные данные, что делает его мощным инструментом для различных приложений, от виртуальных помощников до создания контента.
Набор моделей:
@ai_machinelearning_big_data
#AI #xGEN #LMM #ML
Please open Telegram to view this post
VIEW IN TELEGRAM
Please open Telegram to view this post
VIEW IN TELEGRAM
⚡️ Новостной дайджест
✔️ EX.CO представила систему рекомендаций видеоконтента на основе LLM для цифровых издателей.
Презентованная система позволяет издателям предоставлять аудитории наиболее релевантные видеоролики из банка видеоконтента в режиме реального времени, без ручного сопоставления текстовых данных с мультимедиа.
Система показала высокие результаты, достигнув 80% совпадения релевантности и 4-кратного увеличения вовлеченности аудитории по сравнению с отраслевыми стандартами. Среднее количество негативных взаимодействий с видеоплеером уменьшилось на 30-40%.
prnewswire.co.uk
✔️ Модель HeAR от Google DeepMind выявляет заболевания с помощью анализа звука.
Google разработал биоакустическую модель под названием Health Acoustic Representations (HeAR), предназначенную для обнаружения заболеваний через анализ звуков. Модель была обучена на 300 миллионах аудиофайлов, включая 100 миллионов звуков кашля.
Индийская компания Salcit Technologies использует HeAR в своем приложении Swaasa для анализа кашля с целью раннего выявления туберкулеза.
HeAR демонстрирует высокую эффективность при меньшем объеме обучающих данных. Модель также может обнаруживать другие заболевания, такие как хроническая обструктивная болезнь легких и, потенциально деменцию.
blockonomi.com
✔️ Henrik.ai: мультиконтекстный сервис с ИИ для разработчиков.
Neuralogics представила платформу искусственного интеллекта Henrik которая упрощает процесс разработки программного обеспечения. Пользователи могут создавать функциональные приложения всего лишь с помощью простого запроса.
Henrik.ai основан на концепции "мультиконтекстного интеллекта" которая использует сеть специально обученных AI-моделей для создания комплексных программных систем. Набор моделей позволяет сервису адаптироваться к различным контекстам и сценариям обеспечивая функциональность масштабируемость и безопасность.
Платформа также включает адаптивное обучение которое помогает сервису улучшаться на основе новых данных и взаимодействий с пользователями. Neuralogics акцентирует внимание на этичности и прозрачности решений.
devops.com
✔️ Новая система Парето от Recogni оптимизирует вычисления ИИ с минимальными потерями точности.
Компания Recogni Inc представила новую логарифмическую систему чисел под названием Pareto которая оптимизирует вычисления ИИ при минимизации потери точности. Эта система решает проблемы, связанные с высокими вычислительными требованиями генеративных моделей которые требуют petaFLOPS операций.
Система преобразует умножения в сложения, снижает потребление энергии, задержку и размер чипа, сохраняет высокий уровень точности и достигает высокой производительности при значительно меньшем потреблении энергии.
Эта разработка позиционирует Recogni как лидера в области проектирования чипов, особенно для генеративных приложений, предоставляя решение которое балансирует производительность и эффективность без ущерба для качества модели.
siliconangle.com
✔️ DeepBrain AI в сотрудничестве с Национальным полицейским агентством Кореи представила решение для обнаружения дипфейков.
Сотрудничество государственного органа и частой компании направлены на борьбу с растущей угрозой преступлений, связанных с подменой личности, которые становятся все более сложными и представляют значительные риски для общества.
Система включает два основных компонента: комплексное и голосовое обнаружение. Она анализирует поведенческие паттерны, такие как углы наклона головы и движения губ, для определения подлинности изображаемого лица. Процесс обнаружения занимает от 5 до 10 минут, после чего контент классифицируется как "настоящий" или "фальшивый".
Система основана на данных, собранных DeepBrain AI, включая один миллион корейских и 130 тысяч азиатских данных.
Продукт доступен как SaaS, а также в виде локальной версии для организаций.
globenewswire.com
@ai_machinelearning_big_data
#news #ai #ml
Презентованная система позволяет издателям предоставлять аудитории наиболее релевантные видеоролики из банка видеоконтента в режиме реального времени, без ручного сопоставления текстовых данных с мультимедиа.
Система показала высокие результаты, достигнув 80% совпадения релевантности и 4-кратного увеличения вовлеченности аудитории по сравнению с отраслевыми стандартами. Среднее количество негативных взаимодействий с видеоплеером уменьшилось на 30-40%.
prnewswire.co.uk
Google разработал биоакустическую модель под названием Health Acoustic Representations (HeAR), предназначенную для обнаружения заболеваний через анализ звуков. Модель была обучена на 300 миллионах аудиофайлов, включая 100 миллионов звуков кашля.
Индийская компания Salcit Technologies использует HeAR в своем приложении Swaasa для анализа кашля с целью раннего выявления туберкулеза.
HeAR демонстрирует высокую эффективность при меньшем объеме обучающих данных. Модель также может обнаруживать другие заболевания, такие как хроническая обструктивная болезнь легких и, потенциально деменцию.
blockonomi.com
Neuralogics представила платформу искусственного интеллекта Henrik которая упрощает процесс разработки программного обеспечения. Пользователи могут создавать функциональные приложения всего лишь с помощью простого запроса.
Henrik.ai основан на концепции "мультиконтекстного интеллекта" которая использует сеть специально обученных AI-моделей для создания комплексных программных систем. Набор моделей позволяет сервису адаптироваться к различным контекстам и сценариям обеспечивая функциональность масштабируемость и безопасность.
Платформа также включает адаптивное обучение которое помогает сервису улучшаться на основе новых данных и взаимодействий с пользователями. Neuralogics акцентирует внимание на этичности и прозрачности решений.
devops.com
Компания Recogni Inc представила новую логарифмическую систему чисел под названием Pareto которая оптимизирует вычисления ИИ при минимизации потери точности. Эта система решает проблемы, связанные с высокими вычислительными требованиями генеративных моделей которые требуют petaFLOPS операций.
Система преобразует умножения в сложения, снижает потребление энергии, задержку и размер чипа, сохраняет высокий уровень точности и достигает высокой производительности при значительно меньшем потреблении энергии.
Эта разработка позиционирует Recogni как лидера в области проектирования чипов, особенно для генеративных приложений, предоставляя решение которое балансирует производительность и эффективность без ущерба для качества модели.
siliconangle.com
Сотрудничество государственного органа и частой компании направлены на борьбу с растущей угрозой преступлений, связанных с подменой личности, которые становятся все более сложными и представляют значительные риски для общества.
Система включает два основных компонента: комплексное и голосовое обнаружение. Она анализирует поведенческие паттерны, такие как углы наклона головы и движения губ, для определения подлинности изображаемого лица. Процесс обнаружения занимает от 5 до 10 минут, после чего контент классифицируется как "настоящий" или "фальшивый".
Система основана на данных, собранных DeepBrain AI, включая один миллион корейских и 130 тысяч азиатских данных.
Продукт доступен как SaaS, а также в виде локальной версии для организаций.
globenewswire.com
@ai_machinelearning_big_data
#news #ai #ml
Please open Telegram to view this post
VIEW IN TELEGRAM
Представлены модели:
Phi-3.5-mini-instruct: 3.82B параметров, 128K контекст, улучшено понимание кода, математические операции, на 5 пунктов подросло знание русского языка (по бенчмарку Multilangual MMLU):
Phi-3.5-vision-instruct: 4.15B параметров, 128К контекст, улучшено описание графиков и таблиц, суммаризация по нескольким изображениям и видео, классификация художественных стилей по изображению:
Phi-3.5-MoE-instruct: 16x3.8B параметров, 6.6B активных параметров при использовании 2 агентов, 128К контекст, актуальность датасета обучения - октябрь 2023:
@data_analysis_ml
#AI #Phi #LLM #ML #Microsoft
Please open Telegram to view this post
VIEW IN TELEGRAM
Please open Telegram to view this post
VIEW IN TELEGRAM