Pramaana Labs secures $27 million to ensure the verifiability of AI.

      As companies find it challenging to transform AI pilots into reliable tools, a new startup believes the solution resembles a mathematical proof more than an enhanced chatbot. Pramaana Labs announced on Wednesday that it has secured $27 million in seed funding, led by Khosla Ventures, with participation from Accel, BoldCap, Nexus Venture Partners, Premji Invest, and Unbound.

      The company is targeting high-stakes sectors where incorrect answers can lead to significant costs: law, drug discovery, and tax preparation. Its argument is that these fields are not as chaotic as they appear. “The world’s hardest problems are not unsolvable. They are unformalised,” co-founder and CEO Ranjan Rajagopalan explained. “In every area where being wrong could impact someone’s health, finances, or freedom, there are rules.”

      Pramaana operates on a conventional large language model (LLM), which allows it the flexibility to address natural-language inquiries, but it adds a crucial layer on top. This layer utilizes formal verification, which involves proving that a system functions exactly as intended. Specifically, Pramaana employs LEAN, an open-source language that mathematicians use to verify proofs, to validate the model’s outputs and ensure deterministic reasoning rather than probabilistic.

      “It’s like math because you have a lot of rules to follow,” Rajagopalan told TechCrunch, referring to the tax code. “Once you have a codified version of it, the reasoning above becomes deterministic.”

      Combining an LLM with a verification layer is becoming a prevalent strategy to tackle AI reliability issues. Pramaana claims its unique aspect is the application of formal-proof tools, putting it closer to provable-guarantee research than typical safety measures.

      The challenge lies in the need to first codify the rules, which Pramaana is doing one domain at a time, with each area managed by domain experts. For tax, the company collaborates with former IRS commissioner Danny Werfel, while professors from IIT Delhi, IIT Madras, and UC Berkeley are supervising the cybersecurity and drug-discovery initiatives.

      There is a precedent for this approach; Rajagopalan cites France’s CATALA project, which has converted much of the country's tax and benefit legislation into executable code.

      At this stage, the development is still in progress ahead of the final product. Pramaana possesses the funding, the supporters, and a theory that the limitations of AI accuracy come down to how much of the world has been formally documented. The challenge remains in codifying these rules, which is the difficult part.