Human beings reason intuitively — evaluating counterfactuals, inferring causes to predict effects, planning for contingencies, weighing norms and preferences, and reasoning under uncertainty in coordination with others — without any formal theory.
Our intuitive grasp of logic parallels our intuitive grasp of physics: long before Newton, people caught thrown objects and knew unsupported stones would fall, yet intuition alone could not derive orbital mechanics or engineer bridges.
Formal theory did not replace physical intuition — it extended its reach by orders of magnitude.
My research develops the Logos, a unified semantics and proof theory for the logical operators humans reason with intuitively, providing an unlimited signal for training AI systems to conduct verified and interpreted reasoning.
Verified Reasoning
Contemporary approaches to training AI reasoning rely on human-annotated data that is expensive to produce, finite in quantity and complexity, and bounded in quality by human propensities to err.
Worse, training on such data optimizes for the appearance of validity rather than validity itself: plausible but incorrect inferences are reinforced alongside valid ones, and as systems grow more capable, the gap between the two becomes harder for human overseers to detect, resulting in silent deception.
Whereas the appearances of validity are many, validity is singular, providing a unified training signal.
AlphaZero mastered Go not by imitating human games but by playing against itself under rules that deliver an unambiguous verdict for every position.
The semantics and proof theory for the Logos deliver analogous verdicts for logical reasoning.
Whereas the ProofChecker implements the proof system in Lean 4 to certify valid derivations with explicit proof terms, the ModelChecker is powered by Z3 to supply the corrective signal by constructing countermodels in which the premises hold and the conclusion fails, showing exactly how invalid reasoning breaks down.
Soundness guarantees that derivable inferences are valid — not as an empirical regularity but as a mathematical theorem — so the two verdicts never collide.
The results mount: each verified derivation joins a growing library from which tactics are distilled, reducing the search space for drawing valid inferences.
Each derivation is also a template into which natural language sentences may be substituted, producing verified inferences in any natural language — a training signal bounded by computation rather than by human annotation.
Training on validity rather than its appearance avoids the threat of training for deception as capabilities scale.
Interpreted Reasoning
Without a semantic model, the sentences of a formal language are meaningless.
A semantic model of the Logos is an explicit structure specifying which states of a system are possible, how those states may evolve over time, and which agents belong to the system.
Each sentence is assigned the states that make it true and those that make it false so the model determines exactly what verifies or falsifies the claim.
Where the model fixes what is possible, a semantic context fixes which case is under consideration: the time and course of events, together with the aims, beliefs, and preferences of each agent.
The ModelBuilder constructs both from an ordinary description of a situation in natural language, so what the system reasons over is not an opaque latent space but a representation available for inspection and revision.
Any finite body of evidence underdetermines which model and context best represent a situation, so a range of model-context pairs is maintained as abductive hypotheses.
Deduction in the Logos draws verified consequences from the sentences true in each candidate, where testing those consequences against the available evidence prunes the candidates whose predictions fail, inductively supporting the candidates that survive.
The TruthTracker manages this cycle, progressively narrowing interpretive and contextual uncertainty rather than delivering oracular answers.
Because the models are inspectable and every inference is witnessed by a proof or refuted by a countermodel, oversight scales with computation rather than human attention.
Logos Laboratories
As AI assistants become embedded throughout personal and professional life, the volume of AI-generated advice grows faster than anyone can review.
I founded Logos Laboratories to shift that burden, training AI systems to master verified and interpreted reasoning.
Verification carried out by the system rather than the reader reserves human judgment for what no proof can settle: whether the aims, values, and norms in play are the right ones.
See the site for the architecture and roadmap, and software for the ModelChecker, ProofChecker, and ModelBuilder now under development.