Las empresas enfrentan cada vez más desafíos para pasar de pruebas piloto de inteligencia artificial a sistemas confiables en su operación diaria. En este contexto, Pramaana Labs surge como una nueva apuesta que busca resolver el problema de la fiabilidad combinando herramientas de formalización matemática con la potencia de los modelos de lenguaje.
La compañía anunció una ronda de financiación semilla por 27 millones de dólares liderada por Khosla Ventures, con participación de Accel, BoldCap, Nexus Venture Partners, Premji Invest y Unbound. Este respaldo llega en un momento donde la confiabilidad se convirtió en prioridad para implementar IA en entornos reales.
Enfoque en verticales de alta sensibilidad
Pramaana se concentrará en áreas especialmente sensibles como el derecho, el descubrimiento de fármacos y la preparación de impuestos. En estos campos, un error puede generar costos elevados y se exige el máximo nivel de confiabilidad. La implementación de IA en estos sistemas requiere protecciones más robustas contra alucinaciones y fallos.
Según Ranjan Rajagopalan, cofundador y CEO de la empresa, estos dominios se adaptan bien a la formalización. “Es como la matemática en el sentido de que hay muchas reglas que hay que respetar”, explicó, refiriéndose al código tributario. Una vez codificadas esas reglas, el razonamiento encima se vuelve determinista.

El sistema de Pramaana utiliza un LLM convencional para mantener la flexibilidad y responder preguntas en lenguaje natural o resolver problemas complejos. Sin embargo, incorpora una capa determinista que verifica el trabajo del modelo.
Verificación formal con LEAN
Lo distintivo de su enfoque es el uso de herramientas de verificación formal, basadas en el lenguaje de programación open source LEAN, empleado para verificar pruebas matemáticas. Esta combinación de motor LLM con verificación determinista gana popularidad, pero Pramaana la potencia con formalización rigurosa.
Existe precedente en proyectos como CATALA de Francia, que formaliza gran parte del sistema tributario y de beneficios del país en código ejecutable. Para cada caso de uso, Pramaana construirá su propio sistema de verificación estilo LEAN, supervisado por expertos en el dominio.
En derecho tributario, colaboran con el ex comisionado del IRS Danny Werfel. Profesores de IIT Delhi, IIT Madras y UC Berkeley supervisan los sistemas de ciberseguridad y descubrimiento de fármacos.
Los problemas más difíciles del mundo no son irresolubles, sino que no están formalizados, afirma Rajagopalan. Cada dominio donde equivocarse puede costar salud, dinero o libertad tiene reglas que ahora necesitan ser codificadas de manera precisa.
Esta aproximación busca llevar la IA a niveles de confiabilidad matemática en campos donde los errores no son una opción. Al formalizar las reglas complejas de cada sector, Pramaana apunta a que los modelos generativos operen con garantías verificables, reduciendo riesgos en aplicaciones críticas.