Компания Pramaana Labs привлекла 27 миллионов долларов в рамках посевного раунда от Khosla Ventures для внедрения формальной верификации в искусственный интеллект.

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

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

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

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

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

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

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

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

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

Источник: techcrunch.com