Alignment will never be enough.
Alignment trains a language model to produce the answers people prefer. It shapes how the model tends to behave, but gives no way to check a given answer. We think AI needs what people built long ago for the same problem: a formal layer, where a result can be verified by someone else.
What alignment does, and what it cannot do.
In language models, alignment is the training that follows pre-training: instruction tuning, then reinforcement learning from human or AI feedback (RLHF, DPO and their variants).12 The model is rewarded for the answers raters prefer: helpful, polite, and within the rules it was given. It is what turned raw text predictors into usable assistants, and it keeps improving.
But alignment acts on tendencies, not on individual answers. It makes a good answer more likely without telling you whether this one is right. And because raters reward answers that look right, a model can learn to sound confident, or to agree with the person asking, when it should not, a problem known as sycophancy.3 A well-aligned model is more pleasant to work with, and it still cannot show that a figure is correct.
Trust does not work that way anywhere else. We do not trust an accounting department because its staff are well trained, but because of procedures: the audit, the second signature, accounts that have to balance.
Trust at scale rests on being able to check, not on how well a system was trained.
People already solved this. They invented formal systems.
Natural language is how we think aloud, and it is ambiguous by design. Every time the stakes rose, people built something stricter on top of it. Numbers and accounting, so a debt meant the same to both parties. Algebra, so a result could be re-derived by someone who did not trust its author. Law written down, logic, proof, and eventually programming languages.
None of these replaced intuition. A mathematician still guesses the theorem before proving it. What formal systems gave us is a way to communicate without having to be believed: the reasoning travels with the conclusion, and a stranger can check it.
Language models are in the position we were in before that step. Fluent, fast, often right, and with no way to hand over their reasoning in a form anyone can verify.
Formal systems are how people communicate without having to be believed.
AI needs its formal layer.
This is what we mean by neuro-symbolic AI. The neural part does what it is good at: understanding a question asked in ordinary words, in the context of a business. The symbolic part does what language cannot: it states the answer as a rule that can be read, verified, re-run and compared.
The formal layer gives the machine the instrument people built for themselves. A model that writes a rule in a logic language has to commit: to which orders count, over which period, on which column. The commitment can then be checked by a verifier, by the data, and by the person who owns the number.
A rule also lasts. A paragraph of generated explanation is gone with the conversation. A rule is kept, named, and built upon, the way mathematicians keep a lemma: a small result kept so that bigger arguments can stand on it. Kept in git, too, so that the history of a company's reasoning can be audited like the history of its code: who decided what, and when.
The model translates. The formal layer reasons. That is what makes the reasoning auditable.
What if models keep getting smarter?
They will, and that is the strongest argument for a formal layer. A more capable model is given larger tasks and more autonomy, and it produces more conclusions than anyone can review by reading. The gap between what a model can produce and what a person can check grows with every generation.
Reading the model's explanation is the first check to stop working. When a system reasons better than the person reviewing it, that person can no longer tell a sound argument from a convincing one. The only checks that keep up are those that do not depend on the intelligence of the checker: a verifier that applies fixed rules, a query that runs on the data, a counterexample that either exists or does not.
Mathematics has been through this already. Appel and Haken's 1976 proof of the four colour theorem rested on computer calculations too long to check by hand. In 2005, Georges Gonthier and Benjamin Werner verified it formally in the Coq proof assistant, so that only Coq's small kernel still has to be trusted.4 Samuel Ferguson and Thomas Hales proved the Kepler conjecture in 1998, but the full proof was not published until 2006, because its referees could not verify the computer part. The Flyspeck project then verified it formally in the HOL Light and Isabelle proof assistants, and its checks were completed in 2014.5 As proofs grew beyond what people could read, formal verification became more important.
Checking is also cheaper than finding. A verifier does not need to be as clever as the model; it only has to confirm, step by step, what the model claims. A smarter model therefore does not compete with the formal layer. It writes better rules, faster, and the layer turns each of them into a result anyone can rely on.
The more capable the model, the more its work needs a check that does not depend on trusting it.
What determinism and explainability buy.
In practice, they bring three benefits.
Trust
You cannot read a model's behaviour, but you can read a rule. When the same definition gives the same result whoever runs it, and shows what it rests on, you can put it in front of an auditor, a customer or a board.
Efficient processes
Work accumulates instead of being redone. Disagreements about a definition become visible instead of latent. Agents hand each other verified facts, not prose that the next one has to interpret again.
Lower costs
Reasoning that is done once is not paid for on every question. The computation runs where it is cheapest, in the database. And a modest model that writes a checked rule is worth more than a large one that guesses.
What we do not believe.
That a second model can be the judge of the first. It is one more opinion, with the same weaknesses. Verification has to come from something of a different nature than the thing being verified.
That guardrails added afterwards are enough. Filtering what a model said is not the same as constraining what it can assert. The check has to happen before the answer is given.
Where this leads.
To companies whose knowledge is no longer scattered across heads, dashboards and documents that disagree, but written once as definitions that run. To agents that share a memory made of verified rules, and can be swapped without losing what was learned. To AI you adopt the way you adopt any serious instrument: because you can see how it reaches its result.
We are building the pieces of that layer in the open, and the product that puts them to work.
Sources
- Ouyang et al., “Training language models to follow instructions with human feedback” arXiv:2203.02155, 2022. The InstructGPT paper, which set out alignment by reinforcement learning from human feedback.
- Rafailov et al., “Direct Preference Optimization: Your Language Model is Secretly a Reward Model” arXiv:2305.18290, 2023.
- Sharma et al., “Towards Understanding Sycophancy in Language Models” ICLR 2024, arXiv:2310.13548. Five assistants trained with human feedback all showed sycophancy, and human preference data favours answers that match the user's views.
- Georges Gonthier, “Formal Proof: The Four-Color Theorem” Notices of the American Mathematical Society 55(11), 2008, pp. 1382–1393.
- Hales et al., “A formal proof of the Kepler conjecture” Forum of Mathematics, Pi, vol. 5, 2017. The official account of the Flyspeck project, including the history of the 1998 proof and its review.
See what a formal layer does to one of your own questions.
In a free thirty-minute demo, we take a question your teams disagree on and show you SynaLemma's answer and the rule it used.