Pramaana Labs and Khosla: $27M to Secure AI

⚡

Key Takeaways

1Pramaana Labs has raised $27 million to integrate formal verification into AI, with support from Khosla Ventures.

2The startup targets sectors such as law and healthcare, where the reliability of AI is crucial to avoid costly errors.

3By leveraging the LEAN language, Pramaana aims to create deterministic systems to enhance the accuracy of LLMs.

💡Why it matters — This approach could transform AI into a more reliable tool in areas where precision is vital.

A Strategic Funding Round for Pramaana Labs

In a context where companies are seeking to reliably integrate artificial intelligence into their operations, the startup Pramaana Labs positions itself as a key player. It recently announced that it has raised $27 million in a seed funding round. This round was led by Khosla Ventures, with notable participation from investors such as Accel, BoldCap, Nexus Venture Partners, Premji Invest, and Unbound.

The Challenge of Reliability in Sensitive Sectors

Pramaana Labs aims to apply its innovations in fields where precision is non-negotiable, such as law, drug discovery, and tax preparation. In these sectors, a mistake can have significant financial or legal consequences. The challenge lies in deploying AI while minimizing the risks of errors and hallucinations, which requires more robust verification systems than those currently available.

Mathematical Formalization as a Solution

According to Ranjan Rajagopalan, co-founder and CEO of Pramaana, these sectors are particularly suited to mathematical formalization. He explains that, much like in mathematics, these fields are governed by numerous strict rules. Once these rules are codified, the reasoning that follows becomes deterministic, which helps reduce errors.

A Hybrid Technology for Greater Precision

The system developed by Pramaana relies on a conventional large language model (LLM) capable of processing natural language queries and solving complex problems. However, a deterministic layer is integrated above this LLM to verify and validate its results. This hybrid approach, combining LLM and deterministic verification, is becoming increasingly popular.

The Use of LEAN and the Example of the CATALA Project

Pramaana Labs stands out for its use of formal verification tools, notably the open-source programming language LEAN, which is commonly used to verify mathematical proofs. Rajagopalan mentions the CATALA project in France, which successfully formalized a large part of the tax system and social benefits into executable code, as an inspiring example of what can be achieved.

Collaborations with Recognized Experts

For each specific application, Pramaana develops a formal verification system inspired by LEAN, under the supervision of domain experts. For instance, for tax law, the company collaborates with Danny Werfel, former IRS commissioner. Additionally, professors from IIT Delhi, IIT Madras, and UC Berkeley contribute their expertise for cybersecurity and drug discovery systems.

Codifying Rules to Solve Complex Problems

Rajagopalan emphasizes that the world's most complex problems are not unsolvable, but simply not yet formalized. According to him, every field where a mistake can have serious consequences, whether financial, health-related, or legal, is governed by rules. Pramaana's mission is to transform these rules into code, thereby making AI more reliable and secure.