Verifiable Intelligence

AI is very good at making plausible looking output. GitHub says more than half the code committed to its platform this year was written or heavily assisted by AI. More than 80% of lawyers use it at work. Roughly half of new articles on the web are mostly machine written.

We all know AI makes mistakes. It is not a fact engine. It is a plausible looking text engine. It is kind of like the weatherman. Good enough most days for the umbrella question. Not good enough when deciding to launch a rocket. When I speak at events I ask the room if they would trust their agent with their bank account. The no is nearly unanimous.

We know AI can produce output. We often do not know how to verify it. People call this the verification bottleneck. Coders cannot read thousands of generated lines so they bolt on tests. Lawyers are on the hook for every line so they check line by line. Verification is such a hassle that many professionals wonder why bother with it at all.

So how do we make sure AI is correct?

Here is what the sales pitch leaves out. Most of what AI produces can be verified automatically right now. Against logic. Against contracts. Against rules you wrote yourself. There are four ways with different levels of trust.

1. Make it show its work. This is the deep research mode every AI tool has now. The agent takes longer, reads more, and hands you citations. It is like a car salesman handing you the Carfax. Better than his word. But he printed it out. You could go check it yourself. With one car you would. With AI it is thousands of cars a day.
2. Get a second opinion. A second model grades the first one. Cheap and everywhere. It is a second opinion from a doctor who went to the same school and read the same books. You could go across town. Nobody does.
3. Taste the soup. Do not read the code. Run it. Tests, property checks, execution. If it passes it passes. This is how coders survive right now and it works because code does something. You cannot run a legal contract and you cannot compile a policy.
4. Fact check it. Formal verification. This is how the chip in your phone gets checked and it is why math bugs in silicon are rare. Neurosymbolic methods bring that to plain English. A model reads the rulebook and writes it out as rules a machine can enforce. Then a program called a solver stands at the door and checks every output against the list. The model has opinions. The solver does not. It has a list. And plain English rules are where most of the real decisions live.

Why is everyone not doing this?

Because the obvious version does not work yet. Not for most people and not at the scale they need.

Start with the solver. It is only as good as the rules the model wrote. If the model misreads one sentence of the policy, the solver will enforce the wrong rule with perfect rigor and nothing anywhere will look broken. We did not remove the trust. We moved it from the answer to the translation. The bouncer checks the list flawlessly. Nobody checked the list.

Then there is what the solver does when it is unsure. It says no. A solver only approves what it can prove and it cannot prove much. The best published guardrails confirm about one valid request in seven and send the rest back to a human. That is the correct trade when a wrong yes moves money. It is also a system that answers one question and punts six. Nobody building a chatbot wants that trade. They want volume.

Formal verification has the same problem from the other side. It works on the chip in your phone because a company spent years writing down what a chip is supposed to do. The reason? A faulty chip can cost hundreds of millions of dollars in damage. Preventing that is paramount. But nobody has written a formal proof for your HR policy. Why not? The cost was simply too high. And in a world of humans checking humans, it was not needed as much. The pitch of neurosymbolic AI is that a model writes the proof for you and then helps you check and sign off on it. Who controls that model and how you check its work become the next questions.

Neurosymbolic guardrails are not the answer for every problem. If you are generating marketing copy or summarizing meetings, plausible is fine and a bouncer at the door is overkill. But there is a whole category of work where plausible is a problem. Law. Healthcare. Research. Anything that moves money, saves lives, or has substantial real world outcomes. In those rooms a wrong yes is an incident and a confirmation question is just a normal day. This is where formal methods belong. This is where we focus first.

So lets talk about verification

There is an old asymmetry in math and it is the reason any succinct proof works. Finding an answer is hard. Checking one is easy. You cannot solve a sudoku at a glance but you can grade one in seconds. A math proof can take a career to write and an afternoon to read. Every system of trust runs on that gap. The auditor does not redo the books. The referee does not replay the game. Cryptography is built on the same idea. A signature takes a secret key to make and a glance to check. Zero knowledge proofs push it further. Verification is meant to be instant and cheap, and what it took to produce the answer stays hidden.

AI blew the traditional verification gap wide open and it can help close it too. When a model writes a thousand lines or a hundred page brief for pennies, and the only way to check it is to read all of it, people will wave it right through. That is the real risk of the verification bottleneck. Plausibly correct being enough to get passed, but not correct enough in for real world decisions.

Fortunately, the same machines that generatate cheap can make proofs cheap. If the model does the work and the model produces the proof, what is left for the human is the easy part. Checking. The room says no when I ask about the bank account because they assume confirming the agent followed their rules means reading everything it did. It does not have to. With cryptography and formal methods those checks can run across millions of decisions and can be verified in under one second.

Look at the four ways again and you will see none of them do this. The car dealer asks you to read Carfax. The first doctor asks you to trust the second doctor. Running the code only works when there is code to run. And the solver, the best of the lot, still redoes the full check every time. A million decisions means a million solver runs, and whoever runs them sees the policy, the facts, and the rule that fired. If you want a regulator to confirm your agent followed the rules, you hand over the rules. If you would rather not, you are back to asking them to take your word. None of them fixed the asymmetry. They move it around.

A zero knowledge proof is smaller than the work it proves. The party that did the work proves it once. Anyone checks it in a fraction of the time, and the proof is about the same size whether it covers one decision or a million. The checker never sees what was behind it. A company that will not publish its rulebook can still prove every action followed it. A regulator that will not take the company's word can still confirm it. Nobody reruns anything. Nobody trusts anybody. Checking is cheap again, which is what checking was always supposed to be.

Neurosymbolic methods give you the thing worth proving. A rulebook in logic a machine can enforce instead of a vibe their totally rad model had 😎. ZKP give you the receipt. Put them together and the output of an AI stops being a claim and becomes a fact that costs almost nothing to confirm, reveals nothing you did not choose to reveal, and requires trusting no one.

This is what I mean by Verifiable Intelligence. Intelligence you cannot verify is a rumor. It could be right. It sometimes is. You still cannot build on it. Intelligence you can verify is something else.

NASA keeps its own weather station because redoing the work is the only way they have to trust the forecast. Weather is chaos. A butterfly in Brazil and the launch scrubs. No proof will ever cover it, so they measure it again themselves.

AI with a solver behind it is not weather. The rules are written down. The logic is finite. The question of whether this output followed that rule has a yes or no answer and a machine can find it. Which means the check does not have to be redone. It can be proven once and handed to anyone.

That is the whole shift. For the first time machines that produce the answer can also hand you proof, and that proof is super cheap to check. You do not have to trust the model. You do not have to trust us. You do not have to trust anyone. Asked again whether I would trust my agent with my bank account.. don't trust verify.