Truth by Construction

Grammar, Logic and Meaning

Prover models for large language models (LLMs) include DeepSeek-R1-Prover, described here as the pioneer, followed by OpenAI o3-pro and GPT-5-Thinking. These models use Chain-of-Thought (CoT) and reinforcement learning on hard mathematical problems. This approach has produced results, including with smaller models from Z.ai and Moonshot AI, but has limitations that can reduce accuracy and efficiency.

This training approach asks LLMs to learn three distinct tasks:

• Grammar
• Logic
• Meaning/Purpose/Creativity ?

A failure may come from a syntax error, a logical inconsistency (what Wittgenstein would call unsinnig¹), or a limitation of the model's reasoning.

Companies such as .txt (dottxt.co) develop regex-based sampling to constrain grammar during inference. The post reports improvements to tool integration and reliability, and reduced compute costs in some applications; this does not address logic.

Regex-based sampling covers simple patterns, and context-free constraints can go futher, up to data specifications like JSON, but none of them solves logic.

Proposition 7 (P7)

Proposition 7 is a work-in-progress constrained-generation system intended to combine typed programming, proof construction, reasoning and natural language².

Philosophy

Philosophy asks questions. Mathematics is when we can determine whether the answers are true or false.

Intelligence is best understood as the capacity to ask good questions, in other words, to make interesting choices. "Interesting" is not the same as "true". We call this ability taste: a coherent model of what is beautiful, and worth looking into.³

Some of what we find interesting is also absurd: we can call it mysticism⁴. Mysticism is cool, and we dedicate a lot of time to it, through art, music, literature, and even love, but it's not something machines can/should do. Nevertheless, we cannot work without it, because finding beauty in a theorem needs the same taste system as finding beauty in a painting, or a poem.

Mathematical work involves choosing what to prove and when, not only constructing proofs.

The proposal is to optimize for taste while constraining outputs to true statements.

Humans naturally think with vague language, often outrunning strict truth conditions, and it makes sense in a messy world.

"In the real world it is more important that a proposition be interesting than that it be true."

— A.N. Whitehead

In formal reasoning, the tradeoff is different. Our thinking systems must balance taste with formality: know which questions should be asked while respecting which questions can be asked. With constrained generation we want to restrict search space to formally valid outputs in a given formal system, and use the broad priors of LLMs as approximations of taste, allowing them to pick which path to explore.

In this setup, the formal layer enforces truth within a formal system, while open-ended association remains in latent representations and a toggleable free-form reasoning. In prelimiary experiments, we've alredy demonstrated that formal constraints can reduce drastically the need for CoT and thus the compute cost.

System Overview

• Constraint Engine: unified grammar and typing/proof rules that produce only valid moves/ASTs within a formal system.
• Syntax independence: the formally constrained sampler is made to be syntax independent and work over runtime-specified context grammars with attached typing rules.
• Constrained pretrained LLM: ranks valid moves, expressed as tokens.
• Mode-switching sampler: the constraint engine can dynamically switch it's formal core, based on parameters like entropy, in order to avoid getting stuck. We can combine free-form text reasoning with formally valid output, for better exploration possibilities.

Constraint Engine

The engine is comprised of three parts:

• A meta-engine that inteprets rules to parse code into partial ASTs
• Rule files, written in a custom DSL inspired by the EBNF notation for grammars, and the natural deduction style for typing rules.
• A completion engine that unifies partial ASTs with rule conclusions to produce valid next tokens.

STLC Example:

Identifier ::= /[a-z][a-zA-Z0-9]*/
Variable(dec) ::= Identifier[x]
Lambda(lambda) ::= 'λ' Identifier[x] ':' Type[τ] '.' Expression[e]
Application(app) ::= Expression[e1] Expression[e2]

BaseType ::= Identifier[τ]
FunctionType ::= Type[τ1] '->' Type[τ2]
Type ::= BaseType | FunctionType | '(' Type ')'

Expression ::= Variable | Lambda | Application | '(' Expression ')'

x ∈ Γ
----------- (dec)
Γ ⊢ Γ(x)

Γ[x:τ1] ⊢ e : τ2
----------------------- (lambda)
Γ ⊢ τ1 → τ2

Γ ⊢ e1 : τ1 → τ2,   Γ ⊢ e2 : τ1
-------------------------------- (app)
Γ ⊢ τ2

Meta Typing

The rule file itself is parsed and checked before being admitted, and "executed" as a constraint engine on the input.

Adding features can be done by supplying new constructor symbols alongside rules that relate them. If the meta checker accepts the file, the engine can generate with them without code changes. The system never executes object rules at meta time, it simulates them structurally and uses their inference mecanisms to provide completions, passed as constraints to the model. It's some approximation of abstract interpretation. Notably, this means that the system must have persistent states, unlike CFG approaches like what's done in Outlines, adding more complexity to the sampling system. In practical terms, this means we maintain a context registry in the type evaluation tasks. Specific rules allowing variable shadowing and mutability can be defined, opening the door to other languages than "pure" functionals.

Sampling constraints can be dynamic, and most adapted to the problem you're working with. This means we can easily switch from constraining in one language to another, on the fly.⁵ It also means that we can choose the best formal framework for the task at hand. We could even have algorithms that adapt the language to the problem, improving efficiency and expressiveness tradeoffs.

Generation loop:

1. Parse input into a Partial AST, with open branches on right-completeable nodes.
2. Unify with rule conclusions and produce a typed tree
3. Silently drop branch rules whose instantiated premises fail
4. Emit syntactic completions from the Partial AST
5. Pass the completion through the typing system to ensure they dont lead to unwell-typed trees
6. Rank the completion using the LLM logits
7. Sample and produce a token

A Paradox

In this project we take the opiniated wager of young Wittgenstein, or at least some (Carnap inspired) generalization of it. Assuming that there is no "sayable" things outside of the space of constrained reasoning can be a risky take. This is why this project can be seen as an experiment, more than an engineering solution. Our primary goal is to study the behavior of constrained reasoning and measure its effects on creativity, entropy and overall intelligence.

Architecture

Practical uses

While our purpose is scientific, we see many practical applications of this work, as in money making opportunities :

• Practitioners: Use constraints to eliminate invalid states; devote model capacity to style and strategy.
• Decision-makers: Expect better efficiency (less wasted compute) and better interpretability and traceability of the process.
• Researchers: Treat interesting-ness as a learnable value function over valid moves; compare signals (structural, graph, human preference).

Implementation

A reference prototype for the P7 system is currently being developped, mainly by me, with collaboration and feedback from Niels Müdler @ ETHZ

The code is available freely on github/

References

• Wittgenstein, L. (1921). Tractatus Logico-Philosophicus.
• Martin-Löf, P. (1984). Intuitionistic Type Theory.
• Girard, J.-Y. (1972). Interprétation fonctionnelle... (System F / cut elimination).
• Muendler, N., Antonov, N., & Vechev, M. (2025). Type-aware constraint generation for LLM code synthesis (ETH Zurich).
• Willard, B., & Louf, R. (2023). Efficient guided generation for large language models.
• Polikarpova, Kuraj, & Solar-Lezama (2016). Refinement type synthesis.
• Knuth, D. E. (1968). Semantics of context-free languages.

Notes