02:14:00 路 John Coogan, Jordi Hays, Vinod Khosla, S5, Farza Majeed
[02:14:00] S1: I'd say they're less in my face. I I say we're on the decline. Top celebrity brand. [02:14:07] S0: No. I'm quoting John Feeney. No. I think it's just getting it's getting easier and easier to start a business. I think you'll see more celebrity brands. I don't necessarily think you'll see more breakout [02:14:15] S1: brands. Yeah. Okay. So your claim is is quantity is increasing. I think [02:14:18] S0: it's probably getting harder. [02:14:19] S1: Quality is decreasing. [02:14:21] S0: Quality More distribution. Yeah. Yeah. Greater greater I mean, there's gonna be some breakout celebrity brands. Yep. There's gonna be big exits. Yep. There's gonna be as many failures as ever. Right? I mean, my favorite example was like Travis Scott, a few years ago, launched a RTD, like, canned cocktail thing. Shut down, I think, within a year. Like Yeah. Maybe maybe maybe more. And so I I think you're just gonna see more and more and more. [02:14:52] S1: Would you put the Johnny Knoxville Neo Cloud in the in the bucket of celebrity brands? [02:15:00] S0: That is something I would like to see. Less Yeah. [02:15:02] S9: Less C [02:15:03] S1: K Y two k. [02:15:04] S0: Less beverage, more neo clouds. [02:15:06] S1: More [02:15:06] S0: neo. I wanna see Johnny Knoxville levered up. [02:15:10] S5: Yeah. [02:15:11] S0: Right? Yeah. I wanna see him [02:15:12] S1: Racking GPUs himself. [02:15:13] S6: Yeah. I want [02:15:14] S1: him like operationally involved too. [02:15:16] S0: Not just like Not just a pretty face. [02:15:18] S1: Endorsement.
02:15:18 路 John Coogan, Jordi Hays, Ranjan Rajagopalan
[02:15:18] S1: Endorsement. [02:15:18] S0: 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. [02:15:30] S1: It's fine. It's fine. You heard it here first. Jordy Hayes. It's fine. You know what else is fine? [02:15:36] S0: Get used [02:15:36] S1: 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. [02:15:53] S11: Doing great, John. Shadi. [02:15:55] S1: 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. [02:16:02] S0: 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 [02:16:13] S1: It's a sales. [02:16:13] S0: Hack. Good pitch.
02:16:13 路 Jordi Hays, Ranjan Rajagopalan, John Coogan
[02:16:13] S0: Hack. Good pitch. [02:16:15] S11: 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. [02:16:58] S1: 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? [02:17:32] S11: One, two major examples currently are like big four firms [02:17:37] S0: Okay.
02:17:37 路 Jordi Hays, Ranjan Rajagopalan, Jeremy Strong, John Coogan
[02:17:37] S0: Okay. [02:17:37] S11: 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. [02:18:31] S4: Yeah. How much Yeah. [02:18:32] S0: Imagine your CPA being like, great. I just I just finished your your return. It's 99% chance it's accurate. [02:18:42] S1: I mean [02:18:42] S0: There's 99% chance.
02:18:42 路 Jordi Hays, John Coogan
[02:18:42] S0: There's 99% chance. [02:18:43] S1: 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?
02:19:50 路 Ranjan Rajagopalan
[02:19:50] S11: 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.