Стартап Pramaana Labs привлек $27 млн на формальную верификацию ИИ

Компания Pramaana Labs привлекла $27 млн (около 2,16 млрд рублей) начального финансирования от Khosla Ventures, чтобы внедрить формальную верификацию в системы искусственного интеллекта.

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

В среду Pramaana Labs объявила о привлечении $27 млн начального финансирования под руководством Khosla Ventures при участии Accel, BoldCap, Nexus Venture Partners, Premji Invest и Unbound.

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

«Это похоже на математику в том смысле, что существует множество правил, которым нужно следовать», — сказал Раджагопалан TechCrunch, описывая правила налогового кодекса. «Как только у вас есть кодифицированная версия, рассуждения на ее основе становятся детерминированными».

Система Pramaana по-прежнему работает на обычной большой языковой модели (LLM), что дает ей гибкость для ответов на вопросы на естественном языке и решения сложных задач, с которыми не справляются обычные компьютеры. Однако поверх этой LLM существует детерминированный слой, гарантирующий, что работа модели проверена.

Такое сочетание движка LLM с детерминированной верификацией является популярной схемой; уникальный подход Pramaana заключается в использовании инструментов формальной верификации, основанных на языке программирования LEAN с открытым исходным кодом, который используется для проверки математических доказательств. У этой работы есть реальные прецеденты; Раджагопалан указывает на французский проект CATALA, который формализует большую часть налоговой системы и системы пособий страны в исполняемый код.

Для каждого случая использования Pramaana будет строить собственную систему формальной верификации в стиле LEAN, контролируемую экспертами в предметной области. Для налогового законодательства компания работает с бывшим комиссаром IRS Дэнни Верфелем, в то время как профессора из IIT Delhi, IIT Madras и UC Berkeley контролируют системы кибербезопасности и открытия лекарств.

«Самые сложные проблемы в мире не являются неразрешимыми. Они не формализованы», — говорит Раджагопалан. «В каждой области, где ошибка может стоить человеку здоровья, денег или свободы, есть правила».

Теперь эти правила просто нужно кодифицировать.