In this post, we explore the path to intelligent truth by meandering through an abstract logical village. We argue that choosing the rules and base truths of an argument is a search with no gradient to follow, and that current A.I. performs it badly. This offers an account of why A.I. hallucinates, why agents need human intervention, and why scaling the present approach may be an expensive route to AGI.
Computational proof works through derivation; starting from what it is given and taking one valid step after another. The Curry-Howard correspondence makes this precise, equating proofs with programs. But a derivation needs somewhere to start. The axioms of an argument are not derived within it; they are chosen. This post asks what it costs to choose well.
The Analogue
Let’s explore this by first visualising it. Imagine that propositions are represented by houses in a village. Each house is painted blue if it is a true proposition, and red if it is not. In classical logic, this is all you have; truth and falsity are simply asserted. To expand into constructive logic, we connect the houses by a series of one-way roads that allow you to travel from one to another. These roads are the constructed proof: you start at one house (proposition) and move your argument on using a set of rules (logic) until you reach your conclusion. The computer is essentially able to move from house to house via the roads, realising the colour of each house when it arrives.
In the analogy, a topos is akin to a village: a series of houses connected by roads. It is a self-contained geometric landscape following its own internal logic. However, in some way the road network, and the colour and placement of the houses, is abstract. The combination can be applicable to many ideas, not just the starting proposition. Ideas that are similarly structured, or that connect with similarly structured rules, can be interposed with each other. This is the nature of a topos: an abstraction that defines structure between propositions on a meta level.
The Computer
Now, there are some problems here. How does a computer know at which house to start?
Within a village, it follows roads: it starts at one house, travels, and arrives at another. The houses with no roads leading to them are the axioms, the self-evident starting points from which an argument is built. Nothing inside the village says which houses deserve to be starting points. That is settled before the first road is travelled.
This is not a limitation of computation as such. A program can happily manipulate classical proofs, and can search for new ones. The difficulty is subtler. Once the starting houses are fixed, the roads form a well-defined space to explore, with a kind of gradient to follow, each step either keeps you on a valid road or it does not. Before they are fixed, there is no such structure. The question is no longer “which road next?” but “which village?”, and the candidates are not laid out on any map.
The Human
This is where humans enter. The starting houses and the roads define the logical universe in which the village exists. A computer can learn the roads through training, taking small steps through the village and mimicking maps already laid out by humans. But the A.I. must be prompted to act: a human defines the starting house and, more essentially, selects the village. This is an essential part of intelligence. This is selecting the topos.
This is the act of picking the logical universe in which the proof exists, and what it can be constructed from. It is a search over candidate landscapes with no gradient to follow, and no guarantee of success for humans or machines alike. Humans seem to manage it remarkably well, by leaps. Machines currently manage it by trying villages until one fits, which is a different order of cost.
The process of training the machine discovers a set of pre-computed roads by which the computer can travel. Again, the topos is interchangeable: the houses may represent analogous propositions connected by the same road network. So a computer can adapt, using what it has learnt from one set and applying it to a different village; but this leads to problems.
The Hallucination
If we now swap out the propositions of the houses, and the road map is not identical, then the computer will arrive at houses that don’t exist, or produce contradictions. The road map still connects them, but the output is nonsensical; this is hallucination.
It is an artefact of knowing the connections between propositions, but not the topos itself. The two are intimately connected: the houses, and the roads. It can be improved by further training, crawling through more and more villages, but this is expensive and brittle, as it is just tunnel vision in an intricate landscape.
The Agent
We can now see why A.I. finds it difficult to be truly agentic, and why it relies on constant feedback from humans. The human must constantly reset the point that the agent is starting at, in different villages. The human must help the agent backtrack from dead ends. They constantly frame constraints: don’t follow that road. This is because the computer cannot see further than the point it is at, and the road it is on. It gets lost; it doesn’t know where to start. We have made some progress in automating this through frameworks, but it is still a perennial problem.
The AGI
This suggests that, for now, a human must remain in the loop. Selecting the topos means identifying the axioms that define it, and derivation within the topos cannot do that for you. A.I. can approximate the act by searching over candidate villages, but the search is expensive and fails where the candidates are poorly chosen.
This is a claim about cost, not possibility. We have not shown that no machine could do better, and the same limits on guaranteed success apply to us. The human leaps; the machine, for the moment, must wander. If AGI is reachable, it is unlikely to be by scaling the present approach alone.