Pramaana Labs залучила $27 млн від Khosla Ventures для верифікації AI Pramaana Labs отримала $27 млн від Khosla Ventures для формальної верифікації AI

Ключові деталі:

• Новий стартап Pramaana Labs залучив 27 мільйонів доларів початкового фінансування для вирішення проблеми надійності ШІ у корпоративному секторі.
• Компанія використовує методи математичної формалізації, зокрема мову програмування LEAN, для верифікації результатів роботи великих мовних моделей (LLM).
• Pramaana Labs зосереджується на критично важливих галузях, таких як юриспруденція, розробка ліків та податкова справа, де помилки ШІ можуть мати серйозні наслідки.

Підприємства активно шукають шляхи інтеграції пілотних проєктів зі штучним інтелектом у свої бізнес-процеси, і на передній план виходить питання надійності. Новий стартап прагне вирішити цю проблему, використовуючи інструменти математичної формалізації, поєднуючи одну з найбільш стабільних систем комп’ютерних наук з однією з найхаотичніших.

У середу компанія Pramaana Labs оголосила про залучення 27 мільйонів доларів початкового фінансування під керівництвом Khosla Ventures, з участю Accel, BoldCap, Nexus Venture Partners, Premji Invest та Unbound.

Pramaana зосередиться на високочутливих галузях, таких як юриспруденція, розробка ліків та підготовка податкової звітності — сферах, де помилки можуть коштувати дорого, а надійність є надзвичайно важливою. Впровадження ШІ в ці системи вимагатиме сильніших механізмів захисту від “галюцинацій” та помилок, ніж ті, що існують наразі. Однак, на думку співзасновника та CEO Pramaana Ранджана Раягопалана, ці галузі також мають унікальні особливості, що сприяють формалізації.

«Це схоже на математику в тому сенсі, що є багато правил, яких потрібно дотримуватися», — пояснив Раягопалан, описуючи норми податкового законодавства. «Коли ви маєте кодифіковану версію, логічні висновки на її основі стають детермінованими».

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

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

Для кожного випадку використання Pramaana розроблятиме власну систему формальної верифікації у стилі LEAN, яка буде контролюватися експертами у відповідній галузі. Наприклад, у сфері податкового законодавства компанія співпрацює з колишнім комісаром Податкової служби США Денні Верфелом, а професори з IIT Delhi, IIT Madras та UC Berkeley наглядають за системами кібербезпеки та розробки ліків.

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

Тепер ці правила потрібно лише кодифікувати.

За матеріалами: techcrunch.com