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

Зачем нужна математическая проверка нейросети?

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

Система устроена так: обычная LLM отвечает на вопрос пользователя на естественном языке, а поверх неё работает формальная верификация, проверяющая ответ по строгим правилам. За основу взят открытый язык программирования LEAN, который математики используют для машинной проверки доказательств теорем. По сути, каждый ответ нейросети проходит экзамен по формальной логике.

Раунд возглавил Khosla Ventures, участвовали Accel, BoldCap, Nexus Venture Partners, Premji Invest и Unbound. Стартап сосредоточится на трёх вертикалях, где цена ошибки максимальна:

• Налоговое право. Консультант проекта по этому направлению Дэнни Верфель, бывший комиссар IRS (Налоговая служба США).
• Фармацевтика и поиск лекарств. Систему курируют профессора IIT Delhi, IIT Madras и UC Berkeley.
• Кибербезопасность. Те же академические команды из Индии и Калифорнии.

Для каждой области Pramaana строит собственную LEAN-подобную систему верификации при участии экспертов предметной области.

Почему рынку нужен именно такой подход?

Сочетание LLM с детерминированной проверкой само по себе не новость: несколько компаний уже встраивают «ограждения» вокруг нейросетей. Отличие Pramaana в том, что компания берёт инструменты из формальной верификации, проверенные десятилетиями в математике и критичном софте, и переносит их на выходы языковых моделей.

Сооснователь и генеральный директор Pramaana Labs Ранджан Раджагопалан ссылается на французский проект CATALA, который уже формализовал значительную часть налогового и социального законодательства Франции в исполняемый код. Это реальный прецедент: правила, записанные на формальном языке, можно проверять автоматически и без двусмысленности.

Самые сложные проблемы мира не нерешаемы. Они не формализованы. В каждой области, где ошибка может стоить кому-то здоровья, денег или свободы, есть правила. : Ранджан Раджагопалан, сооснователь и CEO Pramaana Labs

Что это значит для вас?

Для российской аудитории параллель прямая. Налоговый кодекс РФ, судебная практика, регламенты клинических испытаний Минздрава, всё это массивные своды формализуемых правил. Французский CATALA показал, что национальное налоговое законодательство можно перевести в исполняемый код. Российские налоговые правила ничуть не менее «кодифицируемы»: ФНС уже автоматизирует проверки, и слой формальной верификации поверх ИИ-помощника мог бы снизить число ошибок в декларациях и консультациях.

• Авторам Дзена и копирайтерам. Пока Pramaana далека от контента, но сам принцип, детерминированная проверка поверх LLM, появится и в привычных инструментах. Следите за обновлениями ChatGPT, YandexGPT и GigaChat: «проверка фактов» в них со временем будет опираться на похожие идеи.
• Маркетологам. Если клиент из юридической, налоговой или медицинской сферы, аргумент «наш ИИ-ассистент верифицирован формально» станет конкурентным преимуществом. Учитывайте это при позиционировании ИИ-продуктов.
• Предпринимателям в РФ и СНГ. Pramaana пока работает с американским и индийским рынками, продукта для России нет. Но подход CATALA открыт, а язык LEAN бесплатен. Если ваш бизнес завязан на сложные правила (бухгалтерия, комплаенс, фарма), имеет смысл уже сейчас изучить, как формализовать ваши регламенты, не дожидаясь, пока это сделает зарубежный стартап.

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

По материалам TechCrunch AI