Trust. The hard currency of AI
Recently, I came across this article “Pramaana Labs raises $27M seed round from Khosla Ventures to bring formal verification to AI”.
What caught my attention was the ‘formal verification’ part.
This is something which is missing from the large Language Models (LLMs) because:
they are language models not knowledge models
it is almost impossible to assess the accuracy of the information which the LLM was trained on.
When the LLM’s output is not what we expected, we have a term for it — ‘AI hallucination’.
Pramana is not unique in what they are trying to achieve. Probably is another one which got money from investors for a similar project.
What makes Pranama approach interesting is the method they want to use: an open source programming language called LEAN.
What does LEAN do differently? It verifies mathematical and logical claims. It doesn’t tell you if the information is accurate. But it can verify if a story based on certain assumptions holds together. As an example — you might get multiple recollections about an event, say a car accident. Multiple witnesses, multiple stories, conflicting facts. Translating this into a set of statements and trying to run through LEAN will identify — not the truth — the consistency.
Pramaana decided to apply this approach for industries which already have formal rules in place — tax law and cybersecurity. It can help to find if the tax law is consistent and there are no conflicting rules and when submitting financials for audits, if all the rules are properly followed.
Imagine in today’s world, where various news organizations, government agencies or individuals are flooding the Internet with a never-ending stream of information, one could assess the sources and identify where the inconsistency is. Or, perhaps you could assess where they are repeating the same information without verifying it.
In my work, I’ve had many conversations about how to build a system which would identify which information is ‘true’ and which one is ‘false’. In my opinion, having access to transparent information is far better where the accuracy will surface and misinformation will be much harder to spread. (I even wrote an article about it for Forbes in 2021. Ahead of my time, I know.)
The idea of using a programming language to assess logical consistency was new to me and I thought that this would be a great opportunity to engage AI to learn more. I asked the first question in a Google search field and before I knew it I was engaged in dialog with Gemini.
I was asking questions about the language, its core features and how to integrate with other tools. With every answer the excitement was growing. Before I knew the dialog went from how to use it in content accuracy verification to designing the workflow. And suddenly Gemini suggested that it is an awesome idea for a startup and if I want to get an investor pitch deck. Gemini got really excited.
You should always be concerned when the machine gets excited. I told Gemini to export the conversation into a text file, uploaded the file to Claude (Anthropic) and told it to provide analysis.
Well, let’s talk about disappointment! Claude was not excited.
It started with: ‘I read through it. It’s a polished, well-structured plan with a genuinely sharp narrative — but there are a few load-bearing assumptions that I’d want stress-tested hard before any of it goes in front of an investor. Here’s my honest take, strongest points first.’ You know what you are getting when you hear the words ‘my honest take’. BTW: I am always baffled by this expression. Why do you have to add the word ‘honest’? If you don’t, what are you saying then?
Anyway, I got the ‘honest take’ on the market — timing is real, technology — is LEAN even the right tool for this job? Is this even a solvable problem? The hard problem is the formalization, not the proving — and it’s circular. I mentioned just a few here, though the list was actually two pages long. The dialog was long and it covered the market players, their strength; fit within various industries, whether it should be B2C or B2B play, etc. All in all, it was fascinating.
In the end, what troubled me was not that this problem is very difficult to solve — that’s actually an exciting challenge. The thing that really bothered me? That I was dealing with two systems with access to almost identical information, which, with utter confidence, were providing completely different sets of recommendations.
You might recall my post ‘Search engines becoming summary engines’. This now can be expanded from ‘summary’ to ‘opinion’. Not only these summaries are based on unvalidated information, they are presented as an opinion produced by algorithms which are transparent as a sheet of lead.
The recurrent pattern? The eternal question ‘who and what to trust?’ is pressing as ever. Technology makes it even more difficult. Trust me.