Посевной раунд Pramaana Labs на $27 млн закрылся в среду. Помимо лид-инвестора Khosla Ventures, в сделке участвовали Accel, BoldCap, Nexus Venture Partners, Premji Invest и Unbound. Стартап основан Ранджаном Раджагопаланом, который формулирует проблему лаконично: «Самые сложные проблемы мира не являются нерешаемыми. Они просто не формализованы».
Проблема, которую берётся решать Pramaana, хорошо знакома корпоративным заказчикам ИИ. Пилотные проекты с языковыми моделями раз за разом упираются в одно: LLM выдают правдоподобные, но неверные ответы — так называемые галлюцинации. В большинстве сфер это неудобство. В налоговом праве, фармацевтике или кибербезопасности — потенциальная катастрофа. Именно поэтому Pramaana сосредоточилась на вертикалях с высокой ценой ошибки.
| Инвестор | Роль в раунде |
|---|---|
| Khosla Ventures | Лид-инвестор |
| Accel | Участник раунда |
| BoldCap | Участник раунда |
| Nexus Venture Partners | Участник раунда |
| Premji Invest | Участник раунда |
| Unbound | Участник раунда |
Технически система устроена как двухуровневая архитектура. Нижний уровень — обычный LLM, который понимает естественный язык и справляется с неструктурированными запросами. Поверх него работает детерминированный верификационный слой: он проверяет, не противоречит ли ответ модели формализованным правилам конкретной предметной области. Для этого Pramaana использует open-source язык LEAN, изначально созданный для верификации математических доказательств. Под каждую отрасль компания строит собственную систему правил на LEAN — с участием профильных экспертов.
Подход не лишён прецедентов. Раджагопалан ссылается на французский проект CATALA, который перевёл значительную часть налогового и социального законодательства Франции в исполняемый код. Pramaana идёт тем же путём, но строит коммерческий продукт и масштабирует метод на несколько отраслей одновременно. Для налогового направления компания привлекла бывшего комиссара IRS Дэнни Верфеля. Системы кибербезопасности и разработки лекарств курируют профессора IIT Delhi, IIT Madras и UC Berkeley.
Сочетание LLM с детерминированной верификацией — не уникальная идея сама по себе: похожую архитектуру используют несколько стартапов и исследовательских групп. Отличие Pramaana — в выборе инструмента верификации. LEAN обеспечивает математически строгую проверку, а не эвристическую фильтрацию. По словам CEO, налоговый кодекс по своей природе похож на математику: «У вас есть множество правил, которым нужно следовать. Как только вы получаете кодифицированную версию, рассуждения поверх неё становятся детерминированными». Это и есть ставка компании: там, где правила поддаются формализации, галлюцинации можно исключить структурно, а не статистически.
