Premji Invest | CEO Series

Summary

What if hallucinations were just bugs a compiler could catch?

‍

In this episode, co-founder and CEO Ranjan Rajagopalan argues that the reliability we once took for granted in software has broken down with AI, and that the fix is making AI prove its work.

‍

Software used to be reliable, and anything that wasn't was called a bug. Now the same failure has a new name, hallucination, and no standard fix. Pramaana's answer draws on a field that predates software engineering: formal verification, long reserved for chip design and the most critical systems. Two shifts make it practical now. AI can translate between formal verification experts and domain experts, removing what Ranjan calls the "human tax" of pairing them, and AI can write the proofs humans found too painful to write by hand. Domain knowledge is formalized offline and vetted by experts. Every answer is then reasoned in Lean, where, as Ranjan puts it, "the compiler is the final boss."

‍

In this conversation, we cover:
- Why "the compiler is the final boss," and how Lean catches what a model hallucinates
- How AI removes the "human tax" of pairing formal verification experts with domain experts
- Why law and tax are "broad and shallow" where math is "deep and narrow," and what that changes in Lean
- What it takes to formalize the US tax code, its regulations, and case law into a machine-checkable format
- Why Ranjan defines ASI as "AGI plus trust," and what the Wright brothers' first airplane says about it

‍

Ranjan also traces formal verification from Leibniz to chip design, explains why no number of unit tests can prove a simple adder correct, makes the case that frontier labs are building a very smart human rather than a perfect one, and describes the pull from legal, insurance, credit underwriting, and governance teams asking whether their rules can be formalized next.

‍

Pramaana Labs is an AI formal verification company that pairs large language models with the Lean theorem prover so every answer arrives with a proof, starting with the US tax code.

[00:00:00] Vedant: Hi, everyone. My name is Vedant. I'm an investor at Premji Invest. Welcome to our next episode of CEO series featuring Ranjan, the CEO of Pramaana Labs.

[00:00:16] Ranjan: Hi, everyone. Uh, this is Ranjan, CEO of Pramaana Labs. At Pramaana, we are building a compiler for the real world to ensure that AI takes ownership of its work. Software, as we have seen, has predominantly been reliable, and anything which was non-reliable was called as a bug earlier. Now we have a cool term called as hallucinations, and people don't know how to deal with it.

[00:00:39] Ranjan: We are effectively a solution for that.

[00:00:41] Vedant: Formal verification is a topic that has existed for decades, right? But it has still been relatively niche. Uh, can you help us understand, and the audience listening to this, understand what was formal verification used for up until now? Formal verification actually predates

[00:00:59] Ranjan: software engineering.

[00:01:01] Ranjan: It has existed for around 300 years when Leibniz was there. The very first notion was that, uh, we should try and formalize the whole world, world's knowledge into it. Uh, the very first applications of formal verification in the real world, uh, was in chip design verification, uh, and then in software coding, and then in math.

[00:01:24] Ranjan: These were the three major cases. Chip design verification is by and large the most popular. If you go and search for a formal verification engineer in LinkedIn or Google, you will find them. Uh, that majorly started in like 1996 where there was a massive, uh, floating point error, uh, in Intel's chips, uh, which led to them calling back a bunch of chips.

[00:01:46] Ranjan: So whenever something is getting taped out in hardware, you cannot afford to make any error, so you need to prove stuff before it goes out. Uh, so there is a very specific area out there, and that also bled into software verification for a fair piece. AWS has a lot of these things. But generally, you reserve it for very highly critical systems

[00:02:06] Vedant: so that you can formally verify them.

[00:02:08] Vedant: So before we go into, you know, the details of formal verification and why it's so complex to do, can you help us understand the chip verification use case? Like what was done in chip verification that needed formal verification?

[00:02:20] Ranjan: When you are actually designing a chip, you need to know for a certain that a cer-- a behavior is maintained.

[00:02:27] Ranjan: Let's say you are circuit designing an adder. An adder has a very specific purpose, A plus B should be equal to C. If there is some error over there in any of those paths, then you need to catch it. You cannot do a unit test. That's what we typically do, right? We do a spot test checking two, three different variables, and then we say it's fine.

[00:02:48] Ranjan: But that's not allowed. You need to ensure that all of the different paths converge, and you need to be able to prove it out. That is the core part where it comes into being. Why can't you do unit tests? Why can't I go test by test across all the different permutation combinations of inputs to see if something can be proved or not?

[00:03:06] Ranjan: So we'll take a very simple example of A plus B, right? There are two variables. Just think about, uh, both of them being of the order of 10 power 9. So now you have 10 power 18 possibilities which you need to check.

[00:03:19] Vedant: Hmm.

[00:03:20] Ranjan: So if you want to write unit tests, you need to write 10 power 18 unit tests. So help us understand what has changed

[00:03:26] Vedant: over the last, say, call it five to 10 years.

[00:03:28] Vedant: It feels like there are two different tailwinds. One tailwind is formal verification, Lean becoming easier, MATLAB becoming more mature, and the other tailwind is the rise of generative AI, where LLMs are really anything to anything machines. Um, so walk us through from your vantage point, what has changed to make Pramaana Labs possible today, which was not possible, say, five years ago?

[00:03:54] Vedant: Two major things. Uh, the first thing is There

[00:03:59] Ranjan: has been efforts in the past to formalize large sections of, let's say, law or tax or any of the other domains too. Uh, most of them came to a pass primarily because you did not have a translator from a formal verification person to a domain expert. This was a massive problem before, whi-which was not exactly solved.

[00:04:25] Ranjan: Uh, any particular effort became a very pinpointed effort, uh, where like these two people will work together and they'll make a change. Uh, in fact, the France government had one such effort running as well, but it ended up taking a humongous amount of time, and people did not have the time. But because we have AI today, that de-links these two people, the formal verification people and the AI researchers from Pramaana, they work on the algorithms which do the conversion.

[00:04:52] Vedant: Hmm.

[00:04:53] Ranjan: And the experts, they just take a look at the conversion, and they say whether it's accurate or not. That is the core piece of technology which we have built, which has separated these two people out so that they can stay in their comfort zone. If you want to put them together and if you, if you want them to write the code and also vet, that's a huge amount of human tax, uh, which we have avoided.

[00:05:15] Ranjan: That's the first part. The second part is, as such, writing a proof is incredibly complex. If you ask a human to write a proof, uh, it's very, very complex. That's why software is not formally verified as we see it today as yet. It's because for one line of code, we have 20 lines of proof. That is a very painful thing to do.

[00:05:36] Ranjan: But because AI is now generating code as well, AI is also good at generating proofs. So that's where we have gone to the realm of actually utilizing proofs, which was not so common earlier. The primal difference between how normal AI works and how Pramaana works is that Pramaana gives out an answer along with a proof.

[00:05:58] Ranjan: General AI, it'll give you an answer, and it's the human who is liable whether the answer is accurate or not. For Pramaana, you get a proof accompanying, which gives you the peace of mind. How do you ensure that the hallucination that the model will have, it wi- it will definitely have, how do you negate that when you're trying to build the Pramaana Labs solution?

[00:06:18] Ranjan: So there are, again, two parts as we talked about it. The, the primal thing to note over here is the domain formalization is a massive offline process. It's not an online process. So all the laws which you see, all the domain knowledge, that gets converted offline, and it is vetted by an expert before it gets put in as knowledge.

[00:06:39] Ranjan: So that part is fairly vetted. So there still is an error rate which could happen, but the errors are caught by human experts before it gets formalized as knowledge. And on the online path, the key part to note over here is all of the reasoning is happening on top of Lean. Because it is happening on top of Lean, the model could still hallucinate an answer, but the compiler is the final boss.

[00:07:04] Ranjan: So Ranjan, how are you handling LLM proofs in different domains? So LLMs have a decent understanding of Lean, but that's specific to math The problems in math are deep and narrow, while the problems in stuff like law are broad and shallow. To tackle the broad and shallow nature, we have architected specific tactics into Lean so that solving of that becomes much faster.

[00:07:33] Ranjan: So, uh, instead of relying on the native tactics of Lean, we have also introduced newer tactics, newer SMT integrations, as we call it, which add better tactics to effectively solve. And then help us

[00:07:46] Vedant: understand the first use case that you guys are going after, because you don't want to just be a platform.

[00:07:50] Vedant: You also wanna show the world what is possible with one use case and then maybe eventually over time be, I'm taking words out of your mouth, but be an ASI company.

[00:07:58] Ranjan: Yeah.

[00:07:58] Vedant: Help

[00:07:58] Ranjan: us

[00:07:58] Vedant: understand the first

[00:07:59] Ranjan: use case. Uh, the first use case where we went, uh, fairly deeper into is tax, uh, where we specifically took the US tax code regulations and case laws and formalized it into Lean.

[00:08:12] Ranjan: So this can effectively be utilized in the state and local taxes, filing, and all of the different advisory use cases as well, wherever a human is getting utilized. So that is the core, the business angle to it. But we majorly started out as, "Okay,

[00:08:26] Vedant: this seems like a super hard problem, so how do we go about it?"

[00:08:29] Vedant: Let's start with the tax example. How do you ensure that it's a bounded problem? Because tax can be fairly subjective. You might have the Internal Revenue code, you might have the, um, regulations, you might have case law, but how do you ensure that there is nothing missing as you formalize a, a very messy domain like

[00:08:46] Ranjan: tax?

[00:08:46] Ranjan: One of the core things is also that these are not like parallel systems. These are hierarchical systems, so the most sacrosanct part goes into the tax code. Whatever is somewhat missing from the tax code then gets detailed out in regulations. Whatever is missing in the regulations then go into the tail end use cases of case laws.

[00:09:06] Ranjan: There is a lot of work being done on disambiguation, which is actually a mandate on the IRS side as well. So, uh, in fact, countries now have come up with a, with programs called Law as Code. What are the other use cases beyond tax that you will explore with Ramanujan's? Uh, so the broader theme, uh, which we are currently focusing on is called semantic domains, where you have a body of knowledge represented as a set of rules.

[00:09:33] Ranjan: Now, this applies all the way from tax, legal, accounting, financial systems, BFSI, and insurance as well. And all of them also tie back into governance, which is the view from the government standpoint on like what even the law needs to be. In all of these cases, you just have a set of rules, and they need to get formalized.

[00:09:57] Ranjan: The most recent advancement which we have had is that our domain formalizer scales Even though we had started it out with tax, it was good that we started out with tax because it was extremely messy. Are Frontier Labs a threat to Pramaana's business? It's mostly about, uh, focus and also the body of work.

[00:10:17] Ranjan: Pramaana Labs has taken a bull by its horns to ensure that we are formalizing the whole of tax to start with into our machine checkable format, into our own DSLs. So if someone else needs to start, they need to put in the same amount of effort, same amount of work, find the same crazy people to ensure that the formalization is accurate.

[00:10:37] Ranjan: And that is not the shape at which, uh, most of the Frontier Labs are going. The target seems to be more along the lines of artificial general intelligence, which is focusing on, let's say, a very smart human, not a perfect human. So those are the slightly different shapes to it. What is the difference between AGI and ASI?

[00:10:56] Ranjan: AGI is basically saying that, okay, this is super smart human on the street. He can do everything given some context, but reliability might not be one of AGI's properties. ASI's property is effectively in addition to that reliability as well. I can give you a very simple example with r- relates to how you trust, uh, a calculator.

[00:11:18] Ranjan: Any AI output today is being trusted because of the human, not because of AI. So if you are able to make that go away, then, then we reach a different world. Like, one of the ways which I call about it is, uh, how the first airplane was made. The very first airplane which was made, only the Wright brothers could travel in it, not everyone else.

[00:11:39] Ranjan: But once we have added all of the different constraints on top of it, ensured that it follows all of the different rules, is when it gave peace of mind for everyone to travel. So Pramaana Labs is building that world. We got pulled in from all the different sectors which I mentioned right now, legal, governance, and, uh, insurance, finance, and so on, where people are saying, "Oh, okay, can you formalize credit underwriting?

[00:12:08] Ranjan: Can you formalize the insurance rules? Can you formalize the RCM segment?" Because all of them are a series of rules. Everybody is, is going through the same problems of hallucination, so it was like a massive pull. Like, within four days of launching we had, like, 50, 50 calls. We, we had earlier assigned two people.

[00:12:27] Ranjan: It was not possible. Four people had to join, so it just became a, a, it's a happy problem to solve for in a way, but that's also a market discovery of sorts in that this is very, very wide. It's not just that we are looking at it that way. The world is also aligning that this needs to be there. Trust factor is the ultimate thing, like you also suggested.

[00:12:47] Ranjan: Like, ASI is AGI plus trust. Once you have, like, trust set in stone, then computer's the only thing left, and we can optimize it endlessly.

[00:12:57] Vedant: Ranjan, thank you so much for doing this with us. We are so incredibly happy to be investors in Pramaana Labs, and we can't wait to see what the future holds.

[00:13:06] Ranjan: Thank you.

‍

CEO Series | Pramaana Labs

Recommended