
Deriving logic from a minimal systems representation
SapienTronic AI (previously called Minotaur AI) reasons by measuring rather than predicting, with no language model and no GPU. In this post we show it doing Aristotle’s logic. Given every standard three-term syllogism,…
以下正文同步自 Hacker News 最新,版权归原站所有,已转换为易读排版。
SapienTronic AI (previously called Minotaur AI) reasons by measuring rather than predicting, with no language model and no GPU. In this post we show it doing Aristotle’s logic. Given every standard three-term syllogism, it reproduced the known classifications without applying a single rule of inference. The representation of systems it runs on already contains the connectives of logic, so a logic puzzle can be built as a system and left to settle.
The machine does compute; what it never does is apply a rule of logic. Nobody tells it how to solve the puzzle, and it never works out a method of its own. It solves the problem without knowing how it solved it.
SapienTronic AI reasons about systems. In its representation, which the MINOS page sets out, a system is anything with something driving it, something constraining it, and its own way of holding the two together: a boiler, a production line, a market, a rulebook and the records of how it was applied. The two earlier posts, the introduction and the deep dive, showed the machine reasoning about systems of that kind.
This post is about logic. Logic is the oldest kind of reasoning there is, and Aristotle wrote the rules for it: statements, and rules for getting from one statement to the next. A system, by contrast, is a thing that runs. On the face of it the two have nothing to do with each other.
They meet at one point. MINOS joins the parts of a system together in three ways, and at their ends those three ways are and, or and not: the three words from which every statement in Aristotle’s logic can be built. So a logic puzzle can be built out of the same parts as a model of a boiler, and then settled like one.
So we built Aristotle’s own logic as a system. The standard syllogistic is finite: with three terms there are 256 possible forms of argument, and read in the two usual ways that makes 512 questions, every standard three-term syllogism under both readings. We put all 512 to the system. Its verdicts matched the known answers on every one, with no rule of inference anywhere in the machine. Every counterexample it found could be checked by hand, and the valid cases were confirmed separately by checking every possibility. It also did something we value even more: when it couldn’t decide a question, it said so, and said why.
This post explains what we did and what we think it means. The full account, with the history, the diagrams and an interactive version of the puzzle, is on the Logic Without Rules page, and the paper is on Zenodo.
There are two ways to know a thing. You can say it, in words or symbols, and reason about it by rules. Or you can build it, as a system, and learn what it does by letting it run.
Aristotle’s way is the first. Take the oldest example in the book: every man is mortal; Socrates is a man; so Socrates is mortal. Aristotle noticed that the argument is sound because of its shape, not because of what it’s about. Put every bird has feathers; a robin is a bird into the same shape and you get a robin has feathers, which is just as sound. He catalogued the shapes that work, and reasoning became a matter of putting your statements into one of those shapes and applying the rule.
That idea has held for two and a half thousand years, and it has grown a great deal. In the nineteenth century Frege turned the rules into an exact written notation, and modern logic began. In 1936 Turing described a machine that applies simple rules to symbols one step at a time, and that machine became the computer. Most programs are lists of steps to apply in order; the declarative and constraint languages that aren’t still hand their work to a solver that searches step by step. The expert systems of the 1970s were thousands of rules of the form if this, then that. A language model is trained on words and gives back words.
The medium keeps changing, from speech to symbols to code to tokens. The assumption underneath it stays the same: knowledge is something said, and reasoning is something done to what is said.
The engineer’s way is the second. A network of water pipes under pressure doesn’t work anything out. The water pushes and backs up until every junction balances, and the flow in each pipe is whatever that balance makes it. The engineer reads the answer off the meters. A circuit does the same: its currents and voltages settle into an arrangement consistent with Kirchhoff’s laws and the parts the circuit is made of, and nobody applies a rule to get there. To know something this way is to know its parts and how they act on one another, and to trust that what it does follows from how it’s built.
This way is as old as the other. Heraclitus, a century and a half before Aristotle, said that a thing is held together by the opposites it holds. A bow is a bow only while the stave and the string pull against each other; slacken either and you have a stick and a cord. That is a system in the engineer’s sense: a drive and a constraint held together, and what it does follows from how it holds them. Aristotle read Heraclitus as denying that a thing can’t be both one way and the other, and set him aside. In a sense, the tradition of knowledge in words began by ruling the systems view out of logic.
The two ways have rarely spoken to each other. Words can reason, but they aren’t the world. Systems are the world, but nobody trusted them to reason, for a reason we come to below. MINOS is built on the engineer’s side: it reads a tree, a market, a circuit and a lattice in the same three roles, as things that are driven, constrained and held together. What we found is that it carries Aristotle’s own logic inside it.
We’ll use one puzzle all the way through. A town has three guilds: lamplighters, wardens and keyholders. A person can belong to more than one. One person can answer to another. Four things are known:
Six questions can be asked about the town:
Try Q1. Clue 4 gives a lamplighter who answers to a keyholder. Clue 3 says anyone who does that is a warden. So that lamplighter is a warden: yes. You picked the two clues that mattered, put them in order and drew the conclusion. That’s a derivation: Aristotle’s way of reasoning. The skill is in choosing which rule to apply, to what, and when.
The system we built answers the same questions without any of that choosing. Why nobody expected that to work comes first.
The idea of letting a system settle to a logical answer isn’t new. Hopfield‘s networks of 1982 settle into states of low energy. Analog solvers for logical constraints followed, and more recently circuits whose resting states are solutions to Boolean problems. When one of these finds a solution, checking it is easy: test it against every constraint.
The hard question was always the other outcome. What do you conclude when the system fails to find a solution? A network that comes to rest in a state satisfying nothing hasn’t shown that no solution exists. It may have stuck in a shallow dip. It may be balanced halfway between two answers. And nothing about the state tells you which.
That is why logic stayed with words. A proof can be handed to someone who has never met its author and checked line by line, and a proof that there’s no solution is as checkable as any other. A settling machine that had found nothing had nothing of the kind to show.
An analog computer at NASA’s Lewis laboratory, 1949. The problem was wired into it; the machine settled; the answer was read off its instruments. Photo: NASA, public domain.
The analog computer makes the same point from the other side. For thirty years in the middle of the last century, engineers wired up circuits whose voltages obeyed the same equations as a bridge or a rocket, switched them on, and read the dials. It worked. The digital computer replaced it within a decade, for the usual reasons: it could be reprogrammed by changing a text rather than rewiring, it could store its results, it was as precise as you liked and it scaled. One further difference is the one that matters here. A digital computer can be programmed to keep a repeatable record of its calculations. An analog machine could record how its quantities changed, on a chart recorder or a plotter, but that record was not a proof that its answer was right. And when it failed to settle, watching it fail did not establish whether a solution existed.
So our question had two parts: can what a system settles to be checked, and can it say something useful when it fails?
MINOS describes a system in three roles, which the earlier posts covered: something drives it (Energy), something constrains it (Control), and the system has its own way of holding the two together (Logic). The smallest part is an element. Something reaches it; the element passes some of it on and holds the rest back; and those two shares are the only things about the element you can see from outside.
Because the two shares add up to the whole, an element sits somewhere on a line from all passed to all held. For logic, we read the two ends as true and false. An element at an end is a statement that has been settled. An element in between is a statement that hasn’t been settled yet, leaning one way or the other. Nothing about the element had to change for this reading to work.
Elements are joined in three ways. The MINOS paper left the question of joining open; we filled it in by looking at how real systems are put together, a reservoir fed by several streams, a circuit, a market.
Now look at the ends. A series chain is true only if every link is true: that’s and. A parallel set is true if any route is true: or. A transposed element is true where the original was false: not. Nobody chose these three joins in order to get the connectives. They were chosen to describe how reservoirs and circuits are built. The logic was already there, in the way systems are put together.
If the joins are the connectives, then a clue about the town can be built, out of elements, the way a model of a boiler is built.
The town becomes a board of cells, one for each fact that could be true: whether Ann is a lamplighter, whether Ann answers to Ben, and so on. Each clue becomes a law about the cells, made of and, or and not. In a town of fixed size, “every” is a long and across the people and “at least one” is a long or. Each clue is written once, as what it means. Nothing says how the clues are to be used; they are constraints on the town, like “water in equals water out” at a junction.
A question is put the way an engineer fixes the water in and out. To ask whether a claim follows, the system holds every clue true, holds the claim false, and lets the board settle. If it comes to rest in a town where every clue holds and the claim is false, it has found a counterexample, and the claim doesn’t follow. If it can’t find such a town, the question stays open until the absence of a counterexample is established some other way. Everything that follows depends on keeping those two outcomes apart.
This looks upside down at first. Logic is about statements; how can a thing be a statement? But the clue hasn’t been turned into a machine. The town has been built as a system, and the clue has become one of its laws, which is what it was to begin with. Modern solvers also produce a town in the end, as an assignment of true and false to every fact; they get there by searching over the statements, choosing a value and testing what follows, one step at a time. Here the town is built and left to find its own shape.
A settled board isn’t yet logic’s kind of answer. Before it counts, it’s checked. Each cell is read as true or false, so the board is now a plain picture of one town. The system works forward again from that picture alone, and every clue, and the denied claim, must come back as it was held. We call this the witness rule. A board that passes it is a counterexample in the logician’s own sense: a case where every premise is true and the conclusion false. Anyone can check it b
正文由 探How 从来源站点 RSS 同步,内容未经改写;遇到排版缺失或需要图片、视频时请以原文为准。