🎥 ReCamMaster — это передовая система генеративного рендеринга видео, разработанная центром визуальной генерации и взаимодействия компании Kuaishou (KwaiVGI). Она позволяет изменять траектории камеры в существующих видеороликах, создавая новые ракурсы сцены без необходимости повторной съемки.
Основные особенности ReCamMaster:
Изменение траектории камеры: Система позволяет перегенерировать видео с новыми движениями камеры, сохраняя исходное содержание и динамику сцены.
Использование предварительно обученных моделей: ReCamMaster использует возможности предварительно обученных текст-видео диффузионных моделей, что обеспечивает высокое качество генерируемых видео.
Создание обучающего набора данных: Для обучения модели был создан крупномасштабный синхронизированный видеодатасет с использованием Unreal Engine 5, включающий разнообразные сцены и движения камеры.
Применения ReCamMaster:
- Стабилизация видео: Система может сглаживать дрожание камеры в видеороликах, создавая более плавные и стабильные кадры.
- Суперразрешение и расширение сцены: ReCamMaster способна повышать разрешение видео и расширять границы сцены за пределы исходного кадра.
- Дополнение данных для ИИ: Система может генерировать видео с различными ракурсами, что полезно для обучения моделей искусственного интеллекта, особенно в области робототехники и автономного вождения.
🟡 Github: https://github.com/KwaiVGI/ReCamMaster
🟡 Paper: https://arxiv.org/abs/2503.11647
🟡 Project: https://jianhongbai.github.io/ReCamMaster/
Основные особенности ReCamMaster:
Изменение траектории камеры: Система позволяет перегенерировать видео с новыми движениями камеры, сохраняя исходное содержание и динамику сцены.
Использование предварительно обученных моделей: ReCamMaster использует возможности предварительно обученных текст-видео диффузионных моделей, что обеспечивает высокое качество генерируемых видео.
Создание обучающего набора данных: Для обучения модели был создан крупномасштабный синхронизированный видеодатасет с использованием Unreal Engine 5, включающий разнообразные сцены и движения камеры.
Применения ReCamMaster:
- Стабилизация видео: Система может сглаживать дрожание камеры в видеороликах, создавая более плавные и стабильные кадры.
- Суперразрешение и расширение сцены: ReCamMaster способна повышать разрешение видео и расширять границы сцены за пределы исходного кадра.
- Дополнение данных для ИИ: Система может генерировать видео с различными ракурсами, что полезно для обучения моделей искусственного интеллекта, особенно в области робототехники и автономного вождения.
Please open Telegram to view this post
VIEW IN TELEGRAM
Please open Telegram to view this post
VIEW IN TELEGRAM
👍8❤4🔥2
This media is not supported in your browser
VIEW IN TELEGRAM
🚀 OmniSVG: Унифицированная модель для генерации сложных векторных графиков
OmniSVG — новая модель, использующая предварительно обученные модели Vision-Language Models (VLMs) для энд-ту-энд генерации сложных и детализированных векторных изображений в формате SVG.
Ключевые особенности OmniSVG:
- Мультимодальность: Способность генерировать SVG на основе текстовых описаний, изображений или их комбинации.
- Эффективность: Преобразование команд и координат SVG в дискретные токены позволяет отделить структурную логику от геометрии, что обеспечивает более эффективное обучение.
- Гибкость: Генерация изображений различной сложности — от простых иконок до детализированных аниме-персонажей.
Вместе с моделью представлен MMSVG-2M — мультимодальный датасет, содержащий 2 миллиона богато аннотированных SVG-объектов, предназначенный для обучения и оценки моделей генерации векторной графики.
🟡 Проект: omnisvg.github.io
🟡 Репозиторий: github.com/OmniSVG/OmniSVG
🟡 Датасет: huggingface.co/OmniSVG
@data_analysis_ml
OmniSVG — новая модель, использующая предварительно обученные модели Vision-Language Models (VLMs) для энд-ту-энд генерации сложных и детализированных векторных изображений в формате SVG.
Ключевые особенности OmniSVG:
- Мультимодальность: Способность генерировать SVG на основе текстовых описаний, изображений или их комбинации.
- Эффективность: Преобразование команд и координат SVG в дискретные токены позволяет отделить структурную логику от геометрии, что обеспечивает более эффективное обучение.
- Гибкость: Генерация изображений различной сложности — от простых иконок до детализированных аниме-персонажей.
Вместе с моделью представлен MMSVG-2M — мультимодальный датасет, содержащий 2 миллиона богато аннотированных SVG-объектов, предназначенный для обучения и оценки моделей генерации векторной графики.
@data_analysis_ml
Please open Telegram to view this post
VIEW IN TELEGRAM
👍12❤5🔥5
🔭 Katib — облачное AutoML-решение для Kubernetes. Этот инструмент позволяет автоматизировать подбор гиперпараметров, раннюю остановку обучения и даже поиск нейросетевых архитектур, работая с любыми ML-фреймворками от TensorFlow и PyTorch до XGBoost.
Особенность проекта — интеграция с экосистемой Kubeflow и поддержка различных механизмов оркестрации, включая Argo Workflows и Tekton Pipelines. Проект активно развивается сообществом и уже используется в продакшн-средах.
🤖 GitHub
@data_analysis_ml
Особенность проекта — интеграция с экосистемой Kubeflow и поддержка различных механизмов оркестрации, включая Argo Workflows и Tekton Pipelines. Проект активно развивается сообществом и уже используется в продакшн-средах.
🤖 GitHub
@data_analysis_ml
👍10❤5🔥3
🌟 LMDeploy — высокооптимизированный инструментарий для работы с большими языковыми моделями.
Разработанный командами MMRazor и MMDeploy, LMDeploy проект предлагает комплексный подход к сжатию, развертыванию и обслуживанию LLM.
Благодаря персистентному батчингу, оптимизированным CUDA-ядрам и квантованию KV Cache, сервис демонстрирует до 1.8x более высокую пропускную способность по сравнению с vLLM.
Поддерживаются десятки моделей, включая Llama 3, Qwen, InternLM и Mixtral, а также мультимодальные решения (LLaVA, CogVLM).
🤖 GitHub
@bigdatai
Разработанный командами MMRazor и MMDeploy, LMDeploy проект предлагает комплексный подход к сжатию, развертыванию и обслуживанию LLM.
Благодаря персистентному батчингу, оптимизированным CUDA-ядрам и квантованию KV Cache, сервис демонстрирует до 1.8x более высокую пропускную способность по сравнению с vLLM.
Поддерживаются десятки моделей, включая Llama 3, Qwen, InternLM и Mixtral, а также мультимодальные решения (LLaVA, CogVLM).
🤖 GitHub
@bigdatai
👍6❤4🔥2
✔️ Проверьте свои знания: пройдите тест по продвинутому инструментарию работы с данными
Успешно ответите на 20 вопросов за 25 минут — сможете поступить на курс «Data Warehouse Analyst» от Otus.
На курсе вы освоите:
- Навыки построения ELT-pipelines: Airflow, Nifi, Airbyte
- Принципы работы аналитических СУБД: Redshift, Greenplum, Clickhouse
- Лучшие практики моделирования данных: dbt, Data Vault
- Визуализацию и BI: Metabase, Superset, DataLens
- Продвинутую аналитику: KPI, Funnels, Marketing Attribution, Cohort, RFM
- DevOps-практики: Continuous Integration, Github Actions
➡️ Начать тестирование: https://otus.pw/74Wgc/?erid=2W5zFH7SvQG
#реклама
О рекламодателе
Успешно ответите на 20 вопросов за 25 минут — сможете поступить на курс «Data Warehouse Analyst» от Otus.
На курсе вы освоите:
- Навыки построения ELT-pipelines: Airflow, Nifi, Airbyte
- Принципы работы аналитических СУБД: Redshift, Greenplum, Clickhouse
- Лучшие практики моделирования данных: dbt, Data Vault
- Визуализацию и BI: Metabase, Superset, DataLens
- Продвинутую аналитику: KPI, Funnels, Marketing Attribution, Cohort, RFM
- DevOps-практики: Continuous Integration, Github Actions
➡️ Начать тестирование: https://otus.pw/74Wgc/?erid=2W5zFH7SvQG
#реклама
О рекламодателе
🤖 Google запускает A2A — новый протокол общения между ИИ-агентами
Google представил Agent2Agent (A2A) — открытый стандарт для обмена задачами между ИИ-агентами в разных сервисах и компаниях.
Это что-то вроде MCP, но с упором на безопасность, мультимодальность и совместимость с корпоративной инфраструктурой.
🔑 Главное:
▪ A2A — task-first: агенты обмениваются не сообщениями, а задачами с жизненным циклом (create, update, cancel, complete).
▪ Автоопределение возможностей: каждый агент публикует JSON-«визитку» с описанием своих способностей (capability discovery).
▪ HTTP, SSE, JSON-RPC — всё работает на веб-стеке, легко встраивается в существующие API.
▪ Поддержка текста, аудио и видео — мультимодальность встроена по умолчанию.
▪ Security-first: в отличие от ранних протоколов (как MCP), здесь продумана авторизация и защита данных.
В теории — это мощный инструмент для автоматизации бизнес-процессов.
На практике — уже критикуют за перегруз и неясные перспективы. Но с ресурсами Google — у проекта есть шанс стать отраслевым стандартом.
📌 Отличие между MCP и A2A:
🧠 MCP (Multi-Agent Communication Protocol) — это:
➡️ Протокол, придуманный, чтобы LLM-агенты могли "болтать" друг с другом.
💬 Основан на сообщениях — один агент пишет другому что-то вроде чата, и тот отвечает.
⚙️ Подходит для простых сценариев: «Скажи это», «Спроси у другого», «Придумай план».
Но:
– Без жёсткой структуры
– Нет встроенной безопасности
– Не поддерживает длинные сложные процессы (например, запланировать и потом отчитаться)
– Не заточен под задачи типа "запусти и следи"
🧠 A2A (Agent2Agent) — это:
➡️ Google-версия MCP, но с упором на бизнес и инфраструктуру.
📦 Вместо чатов — структурированные задачи, у которых есть статусы: created, accepted, completed, failed, cancelled.
📛 Поддерживает авторизацию, описание возможностей агента, обратную связь, долгие процессы, аудио и видео.
Проще говоря:
– MCP — это «чат между ИИ»
– A2A — это «Jira для агентов» — задачи, статусы, ролевая модель, безопасность.
google.github.io/A2A
#Google #A2A #agents #AI #protocols #interop #infrastructure
Google представил Agent2Agent (A2A) — открытый стандарт для обмена задачами между ИИ-агентами в разных сервисах и компаниях.
Это что-то вроде MCP, но с упором на безопасность, мультимодальность и совместимость с корпоративной инфраструктурой.
🔑 Главное:
▪ A2A — task-first: агенты обмениваются не сообщениями, а задачами с жизненным циклом (create, update, cancel, complete).
▪ Автоопределение возможностей: каждый агент публикует JSON-«визитку» с описанием своих способностей (capability discovery).
▪ HTTP, SSE, JSON-RPC — всё работает на веб-стеке, легко встраивается в существующие API.
▪ Поддержка текста, аудио и видео — мультимодальность встроена по умолчанию.
▪ Security-first: в отличие от ранних протоколов (как MCP), здесь продумана авторизация и защита данных.
В теории — это мощный инструмент для автоматизации бизнес-процессов.
На практике — уже критикуют за перегруз и неясные перспективы. Но с ресурсами Google — у проекта есть шанс стать отраслевым стандартом.
📌 Отличие между MCP и A2A:
🧠 MCP (Multi-Agent Communication Protocol) — это:
➡️ Протокол, придуманный, чтобы LLM-агенты могли "болтать" друг с другом.
💬 Основан на сообщениях — один агент пишет другому что-то вроде чата, и тот отвечает.
⚙️ Подходит для простых сценариев: «Скажи это», «Спроси у другого», «Придумай план».
Но:
– Без жёсткой структуры
– Нет встроенной безопасности
– Не поддерживает длинные сложные процессы (например, запланировать и потом отчитаться)
– Не заточен под задачи типа "запусти и следи"
🧠 A2A (Agent2Agent) — это:
➡️ Google-версия MCP, но с упором на бизнес и инфраструктуру.
📦 Вместо чатов — структурированные задачи, у которых есть статусы: created, accepted, completed, failed, cancelled.
📛 Поддерживает авторизацию, описание возможностей агента, обратную связь, долгие процессы, аудио и видео.
Проще говоря:
– MCP — это «чат между ИИ»
– A2A — это «Jira для агентов» — задачи, статусы, ролевая модель, безопасность.
google.github.io/A2A
#Google #A2A #agents #AI #protocols #interop #infrastructure
👍12❤8🔥3😁2
Дружелюбная встреча для аналитиков от команды Международных проектов Яндекс Поиска.
Приходите в штаб-квартиру Яндекса "Красная Роза" 13 апреля — мы расскажем, как устроена команда Международных проектов Поиска, из чего в ней состоит аналитика и каким образом с этим связаны Яндекс Игры.
В финале встречи эксперты из Яндекса проведут для участников диагностику навыков аналитики и математической статистики — если пройдете успешно, мы засчитаем это как успешную техническую секцию при собеседовании в Яндекс.
Зарегистрироваться на Welcome Time для аналитиков можно здесь до 12 апреля
Приходите в штаб-квартиру Яндекса "Красная Роза" 13 апреля — мы расскажем, как устроена команда Международных проектов Поиска, из чего в ней состоит аналитика и каким образом с этим связаны Яндекс Игры.
В финале встречи эксперты из Яндекса проведут для участников диагностику навыков аналитики и математической статистики — если пройдете успешно, мы засчитаем это как успешную техническую секцию при собеседовании в Яндекс.
Зарегистрироваться на Welcome Time для аналитиков можно здесь до 12 апреля
👍4❤2
This media is not supported in your browser
VIEW IN TELEGRAM
reTermAI — это умный ассистент для zsh и bash, который подсказывает команды прямо в терминале на основе вашей истории.
Полезно, если часто забываешь синтаксис или хочешь ускорить работу с CLI.
🚀 Что умеет:
▪ ИИ-рекомендации команд по истории
▪ Поддержка частичного ввода
▪ Выбор LLM (можно подключить свой)
▪ Гибкая адаптация под рабочий процесс
▪ Совместим с zsh и bash
📦 Установил — и терминал стал умнее.
Отличный инструмент для девелоперов, админов и всех, кто живёт в консоли.
pip install reterm-ai🔗 Github
#terminal #cli #bash #zsh #LLM #opensource #reTermAI #ai
@data_analysis_ml
Please open Telegram to view this post
VIEW IN TELEGRAM
❤11👍5🔥4
🤖 InternVL 3 — новый мощный мульти-модальный ИИ от OpenGVLab!
✨ Доступны размеры 1B / 2B / 8B / 9B / 14B / 28B / 38B
📌 Что нового:
- Улучшено восприятие и логика по сравнению с InternVL 2.5
- Нативное мультимодальное обучение улучшает язык
- Построен на InternViT encoder + Qwen2.5VL decoder
- Улучшает даже Qwen2.5VL
🧠 Что умеет:
- Рассуждение в мультимодальном виде
- Работа с документами
- Поддержка ИИ агентов
🔓 MIT License
🔗 Подробнее
✨ Доступны размеры 1B / 2B / 8B / 9B / 14B / 28B / 38B
📌 Что нового:
- Улучшено восприятие и логика по сравнению с InternVL 2.5
- Нативное мультимодальное обучение улучшает язык
- Построен на InternViT encoder + Qwen2.5VL decoder
- Улучшает даже Qwen2.5VL
🧠 Что умеет:
- Рассуждение в мультимодальном виде
- Работа с документами
- Поддержка ИИ агентов
🔓 MIT License
🔗 Подробнее
👍9❤7🔥3😁1
🚀 Нативная поддержка Python в CUDA от NVIDIA!
Теперь можно писать CUDA-код напрямую на Python — без C++ и сторонних обёрток.
▪ Новый API от NVIDIA позволяет взять полный контроль над GPU из Python
▪ Поддержка cuNumeric, RAPIDS, Modulus, и др.
▪ Основано на CPython API — без прослоек
🎯 Что это меняет:
- Снижает барьер входа в GPU-разработку
- Упрощает создание ML и Data Science-проектов
- Открывает возможности для оптимизации
🧠 Python на GPU теперь без компромиссов!
🔗 Подробнее
Теперь можно писать CUDA-код напрямую на Python — без C++ и сторонних обёрток.
▪ Новый API от NVIDIA позволяет взять полный контроль над GPU из Python
▪ Поддержка cuNumeric, RAPIDS, Modulus, и др.
▪ Основано на CPython API — без прослоек
🎯 Что это меняет:
- Снижает барьер входа в GPU-разработку
- Упрощает создание ML и Data Science-проектов
- Открывает возможности для оптимизации
🧠 Python на GPU теперь без компромиссов!
🔗 Подробнее
🔥25👍15❤6
Как сократить расходы на инфраструктуру с GPU?
23 апреля в 12:00 Selectel проведет вебинар для DevOps- и Data-инженеров, техлидов и менеджеров ML-проектов.
Приходите, чтобы обсудить возможности доступных GPU-карт, узнать о кейсах подбора инфраструктуры с GPU и шести способах сократить на неё расходы.
Вебинар бесплатный. Посмотрите полную программу и зарегистрируйтесь по ссылке: https://slc.tl/gdx10
Чтобы не пропустить встречу и узнавать о других митапах, воркшопах и бесплатных курсах Selectel, подписывайтесь на @selectel_events
Реклама. АО «Селектел», ИНН 7810962785, ERID: 2VtzqvnomoF
23 апреля в 12:00 Selectel проведет вебинар для DevOps- и Data-инженеров, техлидов и менеджеров ML-проектов.
Приходите, чтобы обсудить возможности доступных GPU-карт, узнать о кейсах подбора инфраструктуры с GPU и шести способах сократить на неё расходы.
Вебинар бесплатный. Посмотрите полную программу и зарегистрируйтесь по ссылке: https://slc.tl/gdx10
Чтобы не пропустить встречу и узнавать о других митапах, воркшопах и бесплатных курсах Selectel, подписывайтесь на @selectel_events
Реклама. АО «Селектел», ИНН 7810962785, ERID: 2VtzqvnomoF
❤1👍1
🚀 DeepSeek открывает код своего inference-движка , но делает это с умом
Во время Open Source Week команда уже поделилась несколькими библиотеками — и получила мощный фидбек: коллаборации, обсуждения, багфиксы. Сегодня они идут дальше и отдают в open-source ядро своей inference-системы.
🧠 Inference engine DeepSeek построен поверх vLLM
💡 Раньше был внутренним, глубоко кастомизирован под DeepSeek-V3 / R1
⚠️ Но:
– Был основан на старом форке vLLM
– Жёстко зависел от приватной инфраструктуры DeepSeek
– И не имел ресурса на поддержку в
Вместо того чтобы выкладывать «сырой монолит», команда решила постепенно влить лучшие фичи в уже существующие open-source проекты:
✅ Делают фичи модульными
✅ выкладывают оптимизации
✅ Работа ведётся в синхроне с PyTorch и vLLM
https://github.com/deepseek-ai/open-infra-index/blob/main/OpenSourcing_DeepSeek_Inference_Engine/README.md
Во время Open Source Week команда уже поделилась несколькими библиотеками — и получила мощный фидбек: коллаборации, обсуждения, багфиксы. Сегодня они идут дальше и отдают в open-source ядро своей inference-системы.
🧠 Inference engine DeepSeek построен поверх vLLM
💡 Раньше был внутренним, глубоко кастомизирован под DeepSeek-V3 / R1
⚠️ Но:
– Был основан на старом форке vLLM
– Жёстко зависел от приватной инфраструктуры DeepSeek
– И не имел ресурса на поддержку в
Вместо того чтобы выкладывать «сырой монолит», команда решила постепенно влить лучшие фичи в уже существующие open-source проекты:
✅ Делают фичи модульными
✅ выкладывают оптимизации
✅ Работа ведётся в синхроне с PyTorch и vLLM
https://github.com/deepseek-ai/open-infra-index/blob/main/OpenSourcing_DeepSeek_Inference_Engine/README.md
👍15❤7🔥5
🧠 DeDoDe — новый подход к локальному сопоставлению признаков
Проект DeDoDe ("Detect, Don't Describe — Describe, Don't Detect") разделяет процессы детектирования и описания ключевых точек на изображении, обеспечивая высокую точность и гибкость при сопоставлении.
📌 Особенности:
- Детектор обучается на 3D-устойчивости точек
- Дескриптор обучается отдельно на задаче сопоставления
- Поддерживает архитектурную гибкость и повторное использование
- Открытый код на Python, PyTorch, доступен в репозитории
📄 Статья (3DV 2024): arXiv 2308.08479
🆕 Обновление v2: arXiv 2404.08928
🔗 Репозиторий: github.com/Parskatt/DeDoDe
@data_analysis_ml
Проект DeDoDe ("Detect, Don't Describe — Describe, Don't Detect") разделяет процессы детектирования и описания ключевых точек на изображении, обеспечивая высокую точность и гибкость при сопоставлении.
📌 Особенности:
- Детектор обучается на 3D-устойчивости точек
- Дескриптор обучается отдельно на задаче сопоставления
- Поддерживает архитектурную гибкость и повторное использование
- Открытый код на Python, PyTorch, доступен в репозитории
📄 Статья (3DV 2024): arXiv 2308.08479
🆕 Обновление v2: arXiv 2404.08928
🔗 Репозиторий: github.com/Parskatt/DeDoDe
@data_analysis_ml
🔥11❤6👍4
🔥На прошлой неделе СЕО провайдера Cloud․ru Евгений Колбин анонсировал внедрение бесплатного AI-помощника в облачной платформе Cloud․ru Evolution на ежегодной конференции GoCloud
А еще — сразу несколько новых сервисов для Big Data и AI!
- Evolution Managed ArenadataDB, доступный из облака Cloud․ru. Архитектура MPP помогает быстрее и эффективнее обрабатывать данные, в том числе в критически важных системах. Из преимуществ: быстрая и эффективная обработка данных, анализ и прогнозирование клиентской базы, сбор финансовой и управленческой отчетности. Сервис подойдет крупному бизнесу, компаниям среднего сегмента из ритейла, банковского сектора, сферы производства.
- Набор новых платформенных сервисов для работы с big data в публичном облаке Cloud․ru Evolution, который станет доступен в мае этого года. С его помощью компании смогут обрабатывать и анализировать данные, экономить время и ресурсы на обслуживание нужной IT-инфраструктуры и сфокусироваться на росте бизнеса. Готовые инструменты подойдут для AI/ML-задач, легко разворачиваются без помощи специалиста с опытом работы с большими данными.
- Cloud․ru Evolution AI Factory для быстрой разработки и внедрения AI-агентов в облаке. Собранный в одном месте набор готовых AI/ML-инструментов и технологий предоставит несколько новых возможностей: от обучения моделей до запуска мультиагентных систем. Запуск запланирован на лето 2025.
- Cloud․ru Evolution Stack AI-bundle. Это первое в России гибридное облако с поддержкой искусственного интеллекта, которое поможет быстрее запускать и масштабировать AI-сервисы в контуре компании.
А еще — сразу несколько новых сервисов для Big Data и AI!
- Evolution Managed ArenadataDB, доступный из облака Cloud․ru. Архитектура MPP помогает быстрее и эффективнее обрабатывать данные, в том числе в критически важных системах. Из преимуществ: быстрая и эффективная обработка данных, анализ и прогнозирование клиентской базы, сбор финансовой и управленческой отчетности. Сервис подойдет крупному бизнесу, компаниям среднего сегмента из ритейла, банковского сектора, сферы производства.
- Набор новых платформенных сервисов для работы с big data в публичном облаке Cloud․ru Evolution, который станет доступен в мае этого года. С его помощью компании смогут обрабатывать и анализировать данные, экономить время и ресурсы на обслуживание нужной IT-инфраструктуры и сфокусироваться на росте бизнеса. Готовые инструменты подойдут для AI/ML-задач, легко разворачиваются без помощи специалиста с опытом работы с большими данными.
- Cloud․ru Evolution AI Factory для быстрой разработки и внедрения AI-агентов в облаке. Собранный в одном месте набор готовых AI/ML-инструментов и технологий предоставит несколько новых возможностей: от обучения моделей до запуска мультиагентных систем. Запуск запланирован на лето 2025.
- Cloud․ru Evolution Stack AI-bundle. Это первое в России гибридное облако с поддержкой искусственного интеллекта, которое поможет быстрее запускать и масштабировать AI-сервисы в контуре компании.
👍5🔥3❤2
🧠🔍 Kimina-Prover-Preview — мощный инструмент от MoonshotAI для автоматического построения доказательств в логике первого порядка с использованием LLM.
➡️ Что это?
Kimina — это "LLM-aided theorem prover", который комбинирует эвристический поиск с языковыми моделями, чтобы строить формальные доказательства по заданной цели и предпосылкам.
💡 Особенности:
▪ Поддержка логики первого порядка (FOL)
▪ Использует LLM (через API OpenAI, Claude и др.) для генерации обоснований
▪ Интеграция с Lean для проверки корректности
▪ Поддерживает кастомные промпты и множественные режимы поиска
🧪 Как работает:
Формулируется цель и список предпосылок
LLM предлагает следующий логический шаг
Инструмент проверяет, валиден ли шаг с точки зрения формальной логики
Если успешно — продолжается доказательство
🛠 Установка:
📎 GitHub: github.com/MoonshotAI/Kimina-Prover-Preview
➡️ Что это?
Kimina — это "LLM-aided theorem prover", который комбинирует эвристический поиск с языковыми моделями, чтобы строить формальные доказательства по заданной цели и предпосылкам.
💡 Особенности:
▪ Поддержка логики первого порядка (FOL)
▪ Использует LLM (через API OpenAI, Claude и др.) для генерации обоснований
▪ Интеграция с Lean для проверки корректности
▪ Поддерживает кастомные промпты и множественные режимы поиска
🧪 Как работает:
Формулируется цель и список предпосылок
LLM предлагает следующий логический шаг
Инструмент проверяет, валиден ли шаг с точки зрения формальной логики
Если успешно — продолжается доказательство
🛠 Установка:
git clone https://github.com/MoonshotAI/Kimina-Prover-Preview.git
cd Kimina-Prover-Preview
pip install -r requirements.txt📎 GitHub: github.com/MoonshotAI/Kimina-Prover-Preview
❤7👍6🔥2