Imandra Inc., компания, занимающаяся искусственным интеллектом и революционизирующая автоматизированные логические рассуждения, объявила о выпуске ImandraX, своей последней разработки в области нейросимволического ИИ. Этот знаковый выпуск представляет передовые возможности в области автоматизации доказательств, генерации контрпримеров и процедур принятия решений, устанавливая новый отраслевой стандарт для логического анализа, управляемого ИИ.
Поскольку системы ИИ все чаще используются в критически важных приложениях в таких отраслях, как финансы, оборона, здравоохранение и автономные системы, спрос на надежные, объяснимые и математически строгие рассуждения никогда не был выше. ImandraX расширяет границы ИИ, интегрируя мощные автоматизированные рассуждения с ИИ-агентами, платформами верификации и моделями принятия решений в реальном мире.
Imandra Inc.: пионер логических рассуждений на основе ИИ
Imandra Inc. — глобальная компания, занимающаяся искусственным интеллектом и являющаяся пионером платформ Reasoning-as-a-Service® для автоматизированных логических рассуждений в финансовой, оборонной и критически важных для безопасности отраслях. Ее передовые решения на базе ИИ включают Imandra Markets® и Imandra Connectivity®, которые предоставляют строгую формальную верификацию, автоматизацию проектирования и инструменты обеспечения соответствия для критически важных приложений. Основанная на глубоких достижениях в области автоматизированных рассуждений, Imandra позволяет компаниям уверенно применять логические, точные и поддающиеся аудиту аналитические данные, управляемые ИИ.
Imandra стремится привнести строгость и управляемость в самые важные алгоритмы в мире. Компания создала облачную систему автоматизированных рассуждений, позволяющую организациям использовать математическую логику для рассуждений ИИ. Благодаря сильному акценту на разработке надежного и объяснимого ИИ, технология Imandra пользуется доверием исследователей, корпораций и государственных учреждений по всему миру.
Повышение планки в области рассуждений ИИ
Денис Игнатович, соучредитель и со-генеральный директор Imandra Inc., заявляет, что ImandraX — это преобразующий шаг в превращении продвинутых символических рассуждений в основную часть рабочих процессов ИИ. По его словам, оснащая ИИ-агентов мощными автоматизированными логическими рассуждениями и возможностями формальной верификации, компания расширяет границы того, чего могут достичь интеллектуальные системы.
Доктор Грант Пассморе, соучредитель Imandra Inc., добавляет, что ImandraX — это кульминация многолетних исследований и реального развертывания в некоторых из самых требовательных отраслей, включая финансы, оборону и ИИ. Он отмечает, что клиенты и партнеры компании полагаются на автоматизированные рассуждения Imandra для обеспечения безопасности и надежности критически важных систем, от финансовых бирж до автономных агентов. Он уверен, что с ImandraX компания не просто делает строгие рассуждения доступными, но и делает их незаменимыми для следующего поколения принятия решений на основе ИИ.
Ключевые инновации в ImandraX
ImandraX представляет несколько революционных возможностей, в том числе:
- Прорывы в автоматизации доказательств – Усовершенствование логических рассуждений путем внедрения новых методов для смешанных дискретных и непрерывных рекурсивных функций над типами данных. Эта инновация позволяет создать первую формальную модель и верификацию нового стандарта IEEE P3109 для малых (<16 бит) двоичных форматов с плавающей запятой, что необходимо для квантования и дистилляции нейронных сетей.
- Верификация безопасности нейронных сетей – обеспечивает первую формально верифицированную программу проверки доказательств для верификации свойств безопасности нейронных сетей, используя проверку моделей с ограниченным порядком и индукцию, чтобы гарантировать, что модели ИИ работают безопасно и в соответствии с предназначением.
- Декомпозиция областей пространства состояний – обеспечивает более чем 4-кратное ускорение задач декомпозиции областей, значительно повышая эффективность для пользователей в финансовой сфере при тестировании FIX-соединений и других критически важных приложениях.
- Улучшения для разработчиков – недавно представленный плагин VS Code обеспечивает параллельную разработку доказательств, позволяя выполнять параллельные задания в облаке рассуждений Imandra и оптимизируя рабочий процесс формальной верификации.
- Бесшовная интеграция с ИИ – ImandraX легко интегрируется с новым Python API Imandra, обеспечивая плавное внедрение в платформы ИИ-агентов, подготавливая почву для следующей волны нейросимволических агентов рассуждения ИИ.
Решение самых сложных логических задач ИИ
Денис Игнатович утверждает, что ImandraX основывается на многолетнем крупномасштабном промышленном применении автоматизированных рассуждений. Он отмечает, что версия X включает в себя новые алгоритмы рассуждений, революционные архитектурные особенности и бесшовную интеграцию с агентным ИИ, включая библиотеку Langgraph.
Нейронные сети и модели принятия решений, управляемые ИИ, должны справляться с целым рядом проблем, включая объяснимость, проверяемость и безопасность. Многие современные модели ИИ, особенно те, которые используются в глубоком обучении, функционируют как «черные ящики», что затрудняет понимание или проверку процессов принятия решений. Эта непрозрачность представляет собой серьезный риск в отраслях с высокими ставками, таких как финансы, здравоохранение и автономные системы, где решения ИИ могут иметь серьезные последствия в реальном мире.
Для отраслей, зависящих от нейронных сетей, обеспечение надежности и безопасности имеет решающее значение. Игнатович объясняет, что нейронные сети все чаще используются в критически важных для безопасности отраслях, поэтому очень важно убедиться, что они ведут себя так, как задумано, и устойчивы к зашумленным входным данным. Он подчеркивает, что способность ImandraX рассуждать о числовых вычислениях и ее общая инфраструктура формальной верификации позволяют ей проверять свойства нейронных сетей, а также проверять правильность доказательств, сгенерированных сторонними средствами доказательства теорем.
Почему это важно для финансов, обороны и автономных систем
Такие отрасли, как финансы, оборона и автономные системы, работают в средах, где точность, надежность и соответствие нормативным требованиям имеют первостепенное значение. Нормативные стандарты в этих областях постоянно развиваются, требуя, чтобы решения, управляемые ИИ, соответствовали строгим требованиям надзора. Несоблюдение этих правил может привести к юридическим последствиям, финансовым потерям и угрозам безопасности.
Игнатович уточняет, что эти отрасли должны соблюдать строгие нормативные требования и требования безопасности, но их сложность выросла далеко за пределы того, что люди могут полностью понять. Он добавляет, что автоматизация доказательств и декомпозиция областей пространства состояний Imandra в сочетании с интеграцией LLM позволяют разработчикам и инженерам глубоко анализировать поведение системы, обеспечивать соответствие нормативным требованиям и тщательно тестировать системы, управляемые ИИ.
На финансовых рынках алгоритмы ИИ отвечают за принятие торговых решений в режиме реального времени, обнаружение мошенничества и управление рисками. Даже незначительные расхождения могут иметь серьезные последствия, что делает формальную верификацию и автоматизированные рассуждения অপরিмыми для поддержания целостности системы. Аналогичным образом, в обороне автономные системы должны работать в строгих рамках, гарантируя, что решения, управляемые ИИ, соответствуют целям миссии и протоколам безопасности.
Автономные системы, включая беспилотные автомобили и дроны, зависят от моделей ИИ, которые должны ориентироваться в непредсказуемых средах, обеспечивая при этом безопасность пассажиров и соблюдение нормативных требований. Обеспечение надежного поведения этих систем, управляемых ИИ, в любых возможных условиях требует строгих методологий тестирования, которые традиционные методы не могут обеспечить. ImandraX предлагает автоматизированную логическую верификацию, которая позволяет проводить тщательное тестирование на основе сценариев, снижая риски, связанные с непредсказуемостью ИИ.
Будущее нейросимволического ИИ и принятия решений на основе ИИ
Игнатович подчеркивает, что в компании рассматривают нейросимволические подходы как следующий большой шаг в эволюции ИИ. Он отмечает, что традиционным статистическим моделям, таким как LLM, не хватает фундаментальных логических рассуждений. ImandraX, по его словам, устраняет этот пробел, предлагая непревзойденную автоматизацию для анализа сложных алгоритмов — одного из ключевых применений ИИ сегодня.