Pramaana Labs levanta $27M de rodada de sementes de Khosla Ventures para trazer a verificação formal para a inteligência artificial

À medida que as empresas enfrentam dificuldades para transformar programas piloto de IA em partes funcionais de seus negócios, a confiabilidade passou a ocupar o centro das atenções. Uma nova startup espera resolver esse problema recorrendo às ferramentas da formalização matemática, combinando um dos sistemas mais confiáveis da ciência da computação com um de seus mais caóticos.

Na quarta-feira, a Pramaana Labs anunciou um financiamento seed de US$ 27 milhões, liderado pela Khosla Ventures, com participação da Accel, Boldcap, Nexus Venture Partners, Premji Invest e Unbound.

A Pramaana se concentrará em setores altamente sensíveis, como direito, descoberta de medicamentos e preparação de impostos — áreas em que erros podem ser extremamente caros e a confiabilidade é essencial. Implantar IA nesses sistemas exigirá proteções mais robustas contra alucinações e erros do que as que temos atualmente. Mas, na visão do cofundador e CEO da Pramaana, Ranjan Rajagopalan, esses setores também são particularmente adequados à formalização.

“É como a matemática, no sentido de que há muitas regras que precisam ser seguidas”, disse Rajagopalan ao TechCrunch, descrevendo as leis tributárias. “Uma vez que você tem uma versão codificada disso, o raciocínio sobre ela começa a se tornar determinístico.”

O sistema da Pramaana ainda roda sobre um modelo de linguagem convencional (LLM), o que lhe dá flexibilidade para responder perguntas em linguagem natural e enfrentar problemas complexos que computadores tradicionais não conseguem resolver. Porém, há uma camada determinística sobre esse LLM que verifica se as respostas estão corretas.

Essa combinação de um mecanismo baseado em LLM com verificação determinística já é bastante utilizada. A abordagem diferenciada da Pramaana está no uso de ferramentas de verificação formal, inspiradas na linguagem de programação open source LEAN, usada para validar provas matemáticas. Há precedentes importantes nesse tipo de trabalho; Rajagopalan cita o projeto francês CATALA, que formaliza grande parte do sistema tributário e de benefícios do país em código executável.

Para cada aplicação, a Pramaana desenvolverá seu próprio sistema de verificação formal no estilo LEAN, supervisionado por especialistas do domínio. No caso de leis tributárias, a empresa está trabalhando com o ex-comissário do IRS Danny Werfel, enquanto professores do IIT Delhi, IIT Madras e da UC Berkeley supervisionam os sistemas voltados para cibersegurança e descoberta de medicamentos.

“Os problemas mais difíceis do mundo não são insolúveis. Eles não estão formalizados”, afirma Rajagopalan. “Todo domínio em que errar pode custar a saúde, o dinheiro ou a liberdade de alguém possui regras.”

Agora, essas regras só precisam ser codificadas.