Pramaana Labs founder Ranjan Rajagopalan on using formal verification to make AI provably accurate in tax and legal domains

Speaker 2: Endorsement.

Speaker 1: Yeah. Not just a pretty face. So anyways, I think more on the horizon and it's not you know, a lot of I I don't know. I feel like some people don't don't like this but I think it's fine.

Speaker 2: It's fine. It's fine. You heard it here first. Jordy Hayes. It's fine. You know what else is fine?

Speaker 1: Get used

Speaker 2: to The New York Stock Exchange. Than Wanna change the world, raise capital at the New York Stock Exchange. Our next guest might be there soon with Primana Labs. We have Ranjan, who's the cofounder in the waiting room. Let's bring him into the TBPN UltraDome. Welcome to the show. How are you doing? Thank you so much for taking the time.

Speaker 12: Doing great, John. Shadi.

Speaker 2: Pleased to be here. First time on the show. Please introduce the company. We heard a little bit about it from Vinod, but I wanna hear it from you.

Speaker 1: Yeah. Bravo by the way of getting being able to get Vinod to just like personally pitch Yeah. Your company for fifteen minutes on It's on Internet a it's a good, it's a good sales

Speaker 2: It's a sales.

Speaker 1: Hack. Good pitch.

Speaker 12: Thank you. Thank you so much. At Pramana, we we try to make AI more provably accurate. The current frontier of AI focuses on recall, which is more along the lines of how do you make more answers come up. Yeah. But we are trying to focus on very specific mission critical domains like tax, legal, health care, and governance, where a wrong answer could be catastrophic. Mhmm. You wouldn't want AI diagnosing you wrong and ending up in a catastrophic situation. So that's where we focus on. And the technology underneath it is formal verification. Yeah. I would like you guys to dive a little bit deeper and I can get more technical as it is.

Speaker 2: Yeah. I I I'm just wondering about the actual, like, rollout of this. Like, people are using AI tools for health care now. They've been using WebMD. People have been misdiagnosed with cancer for by random internet posts for like decades. You go to WebMD, you're like I have a headache and it's like you got brain cancer and then you freak out, go to the doctor and they're like what are you talking about? Take an Advil. But so like who exactly is is not adopting AI right now because of the hallucination problem?

Speaker 12: One, two major examples currently are like big four firms

Speaker 1: Okay.

Speaker 12: Which are tackling tax and legal cases. You would have heard about the Australian government suing one of the big fours Mhmm. Stating that there is a hallucination which ended up happening. And AI can actually make a plus on the fly. Yeah. If it wants to suit a particular situation, it can make up loss on the flight Mhmm. Which can lead to catastrophic situations. And another thing which we have noticed is also that insurance providers major insurance providers of US have also moved away from insuring AI outputs. So there is a very specific class they have introduced to say that we will not ensure if AI is behind whatever you have said. So those are some things which have come out specific to domains like tax, legal, and health care. Yeah. For health care, we can even see the models themselves typically stating that you need to go to a doctor to verify. We will we will be absolved of the responsibility.

Speaker 5: Yeah. How much Yeah.

Speaker 1: Imagine your CPA being like, great. I just I just finished your your return. It's 99% chance it's accurate.

Speaker 2: I mean

Speaker 1: There's 99% chance.

Speaker 2: The steel man here is like that is That's how I my feel about my lawyer and my like I love I love the people I work with but like humans do hallucinate and so if you give me something that's doesn't even need to be superhuman, something that's gonna just sit alongside that person, I'm pretty happy to buy, but I understand that I would buy more if I could be more sure. And so I understand that. What I'm what I'm confused about is like how are you thinking about building new foundation model, new LLM, new AI technology that bakes formalization into the actual workflow versus like we were talking to Doctor. Carr from Palantir last week about the idea of like you've built this ontology, you have your ground truth, you have your system of record and then you can have the LLMs hallucinate all over the place because at a certain point they're going to run into the ontology and that's going to be the formal, the formalization process. Like is there something is it is an extension of that two systems running side by side checking each other? Or is it more of an entirely new system?

Speaker 12: So it would be a couple of systems interlocking with each other. Mhmm. We actually have four layers in the stack. Mhmm. I can go through an example of how it happens. If you end up asking whether a particular transaction is taxable in Illinois Yeah. You have the first thing which we do is actually a fair bit offline. For tax specifically, we are formalizing The US tax code. Mhmm. So we are taking a very formal domain, but expressed in English today, we are converting that into lean, which is a proving language. Interesting. When we so when we do that, we get it ratified by experts. So our work is deeply involved in formalizing specified domains and ensuring that we get it ratified by the experts themselves too. In that case, we you we do use a lot of LLMs because the current knowledge base is already not formalized. It is present in English. And once we have the whole knowledge base, whenever a question pops up, we convert it into a series of constraints. Mhmm. You will notice Vinod also talking about how humans are not great at specifications. So we ensure that we ask the right set of questions so that ultimately we can give you a reliable answer. Post that, we have a solver and prover working in tandem to ultimately give you an answer along with the proof of correctness. Mhmm. So the key difference between an ontology based approach and a lean based approach is that a lean based approach is intrinsically verifiable. Your answer comes with a proof of correctness. The proof is something which a mathematician trusts. That's supposed to give you more confidence in a way. And like you suggested, you're right in saying that even, like, best humans might make mistakes. But if you actually have a mathematical proof encoded in Lean, you can choose to trust. And that's the frontier which we are aiming for, and it involves, like, fair bit of work between formal formal verification experts who are a deep part of who we are at Pramala Labs.

Speaker 2: Interesting.

Speaker 12: Working along with CPAs, frontier CPAs, frontier lawyers, and frontier doctors.

Speaker 2: Yeah. How are are models getting better at interacting with lean? I've seen a lot of progress in frontier math and the different really hard problems are getting solved. Sometimes they don't use lean and that's sort of a flex. Sometimes they do use Lean and they perform even better then. But is that getting just table stakes now? Because I think your average white collar worker doesn't know how to interact with Lean.

Speaker 12: Absolutely. So the models are getting better at proving with lean. Mhmm. But we are building more foundation models along the lines of formalization in the first place. If you say something in English, how do you convert that into a construct in lean? That's where our focus is on. Mhmm. If you think about it, lean is a system which has been around for the last twelve years. Mhmm. It has taken humanity around nine years to formalize a significant portion of math. We are taking that same technology, and we are we are trying to blitz through tax, legal, and health care. That's right. Where we are identifying what is the core knowledge base

Speaker 2: Yeah.

Speaker 12: And then we are converting it into lean, where you can reason on top of it provably.

Speaker 2: That's very cool.

Speaker 1: What were you doing before this?

Speaker 12: I was a machine learning engineer at Google, primarily focusing on Google Maps. Interestingly, I dropped arrows over there because, I was focusing on getting addresses and phone numbers accurately in Google Maps. Sure. If you think about it, Google Maps is like a very, very messy real world domain. Mhmm. And we have been able to make it trustable. A lot of people do trust Google Maps to a very large extent. Yeah. I intend to bring the same level of rigor to multiple other domains along the way. Yes.

Speaker 2: Very cool. Well, congratulations. Thank you so much for taking the time to come on the to

Speaker 1: meet you.

Speaker 2: We'll talk to you soon. Have a good one.

Speaker 8: Thank you so much.

Speaker 5: Yeah. Cheers.

Speaker 2: Let me tell you about Codex. Codex is a powerful work for workspace for getting work done with AI agents whether you're writing code, analyzing data, creating content or automating business workflows. Codex helps you move projects forward from start to finish.

Speaker 1: That's right.

Speaker 2: So there's a bitter feud going on.

Speaker 1: There was a there was a good comment over on the X Chat Yes. He said, we're on the topic of celebrity brands. He said, flip it on its head, Jordy. Brands by average Joe's like a painter or the owner of a lawn care company instead of celebrities. I think there could actually be something here. I think he's joking. But imagine as a brand, you're trying to differentiate. You hire an actor

Speaker 2: Yep.

Speaker 1: That's just playing the role of an average Joe. Hey, this is average Joe electrolytes.

Speaker 2: Right? Yeah.

Speaker 1: I'm not a I'm not a I'm not a professional athlete. I'm just a normal guy. Yeah. I'm just painting houses. Yeah. Right? Yeah. I'm just painting houses. I get a little dehydrated. I take my average Joe Relatable. It's relatable.

Speaker 2: I like it. I like it.

Speaker 1: The average Joe I do brand meta. Steve is calling it.

Speaker 2: I enjoy it as an idea. I enjoy it as a joke. I do think that there is a version of this, which is if you walk through an marijuana or Whole Foods and you pick up random CPG products and you look on the back, there's often what's called like the love language or whatever. So it's like a couple paragraphs of text. A good example is is it Dots Pretzels or there's some sort of like pretzel twist that's very popular right now. It's a little spicy. It has the the name of the founder and it and it tells the story of like an average Joe. The Buzzball, for example. That is an average Joe brand. It was not a celebrity brand.

Speaker 1: Disagree. Explain. There's nothing average about that founder. One of the most elite entrepreneurs.

Speaker 2: After she started the company.

Speaker 1: I'm gonna make the case that she was always elite. Always good. The buzz the buzz ball woke it up.

Speaker 2: Maybe. Maybe. But there are a lot of brands

Speaker 9: Yeah.

Speaker 2: That their whole origin story is like I was just a normal person. I had a problem for myself. I was going for, you know, olive oil and I smashed the bottle so I made a squeezy bottle. Like there's all these stories that aren't celebrity brands at least at the start and they have, you know, rags to riches stories that are told sort of quietly on the back of the packaging and then slowly over time eventually Unilever buys the company and takes that off

Speaker 1: I just like thinking of it as like a from the marketing lens a brand that is like doesn't have this like heartwarming story. Yeah. It was just like, yeah, we just hired a guy to be like, yeah.

Speaker 5: Just be

Speaker 2: the guy. Just be the

Speaker 7: average Just

Speaker 2: be an elite snowboarder like Nima. Starts to Salt and Stone, you know. He wasn't a celebrity before, although he was a fantastic team boarder.

Speaker 1: Anyway. Before we bring in our next guest, Markie, let's put pull up this video. Somebody put up fake tech ads. Going on here?

Speaker 2: I don't I love ads, but I hate fraud. So I don't know how to feel about this. This is gonna be peculiar.

Speaker 7: I don't

Speaker 1: think there's anything wrong here.

Speaker 2: With fake tech ads? That's real ad space. That could have been sold, Jordy. You're destroying shareholder value by running fake ads. We would never do that. We did do that early in the days. If you go back to the archive, Doctor. Squatch had that feel. Oh, Vince Vaughn. Vince Vaughn running a

Speaker 1: We have the video here.

Speaker 2: Okay. No. No. No. I know exactly where they're going with this. We put the q in q one one seven seven seven. This is hilarious. What if Texas is upside down?

Speaker 1: I mean, this is this is actually how this is how actually how normal people view

Speaker 2: What if the drizzler was purple? Firefly.

Speaker 1: You pay it.

Speaker 2: We pay you. You pay us, we pay you. Fireflow. Wow. What does this say?

Speaker 1: Dennis can tell you.

Speaker 2: Dennis can tell you. Brain

Speaker 1: I like ziplink is now

Speaker 2: They put up a lot of these. Wow. They really went hard. Who is behind this? This has to be a tech insider or someone making

Speaker 1: ziplink is now frugal. The cloud based online safety you know and love now in the palm of your hand.

Speaker 2: They put up so many of these. This is such a great stunt. Is this a if this is a if this is a launching campaign, a launch campaign for a tech brand marketing firm, it's genius. And whoever's behind this should actually be calling every tech company and saying