Pramaana Labs raises $27 million to formally verify AI in critical sectors

Companies are increasingly facing challenges in transitioning from pilot tests of artificial intelligence to reliable systems in their daily operations. In this context, Pramaana Labs emerges as a new venture aimed at solving the reliability problem by combining mathematical formalization tools with the power of language models.

The company announced a seed funding round of $27 million led by Khosla Ventures, with participation from Accel, BoldCap, Nexus Venture Partners, Premji Invest, and Unbound. This backing comes at a time when reliability has become a priority for implementing AI in real-world environments.

Focus on high-sensitivity verticals

Pramaana will concentrate on particularly sensitive areas such as law, drug discovery, and tax preparation. In these fields, a mistake can incur high costs, and the highest level of reliability is required. Implementing AI in these systems necessitates more robust protections against hallucinations and failures.

According to Ranjan Rajagopalan, co-founder and CEO of the company, these domains lend themselves well to formalization. “It’s like mathematics in the sense that there are many rules that must be followed,” he explained, referring to the tax code. Once those rules are codified, the reasoning becomes deterministic.

Pramaana's system uses a conventional LLM to maintain flexibility and respond to natural language questions or solve complex problems. However, it incorporates a deterministic layer that verifies the model's work.

Formal verification with LEAN

What sets their approach apart is the use of formal verification tools based on the open-source programming language LEAN, used to verify mathematical proofs. This combination of LLM engine with deterministic verification is gaining popularity, but Pramaana enhances it with rigorous formalization.

There is precedent in projects like CATALA from France, which formalizes a large part of the country's tax and benefits system into executable code. For each use case, Pramaana will build its own LEAN-style verification system, supervised by domain experts.

In tax law, they collaborate with former IRS commissioner Danny Werfel. Professors from IIT Delhi, IIT Madras, and UC Berkeley oversee the cybersecurity and drug discovery systems.

The world's toughest problems are not unsolvable, but rather unformalized, claims Rajagopalan. Every domain where a mistake can cost health, money, or freedom has rules that now need to be precisely codified.

This approach aims to bring AI to levels of mathematical reliability in fields where errors are not an option. By formalizing the complex rules of each sector, Pramaana aims for generative models to operate with verifiable guarantees, reducing risks in critical applications.