Certifying Multi-Step Logical Computation in Fixed-Parameter Transformers

A language model can answer a logical question correctly without necessarily executing the reasoning process that justifies the answer. We study conditions under which a fixed-parameter Transformer can be certified to perform finite-step Horn-rule deduction during inference. We first give sufficient conditions for consistent variable binding, showing that shared state reads together with attention-score separation ensure that repeated occurrences of a variable refer to the same entity across the premises of a rule. We then construct invariant neighborhoods of logical fact assignments using update errors at reference states and bounds on the corresponding Jacobians. These neighborhoods guarantee that derived facts remain available across successive reasoning steps, while local dependency structure can reduce reference-state verification to combinations of only the relevant facts. We further construct fixed-parameter Transformer templates using finite-temperature softmax, RMS normalization, and SiLU that internally enumerate substitutions, read both current and previously derived facts, and update the logical state. Rule templates are shared across substitutions, so the parameters and caches need not store an expanded list of ground rule instances. We give explicit bounds on representation size, parameter count, verification cost, and substitution-enumeration time, and show that the same parameters and invariant neighborhoods support every finite number of repeated scans. The resulting guarantees imply soundness and, under rule coverage, bounded completeness. Numerical experiments confirm stable logical-state execution over long repeated runs and illustrate the reduction in representation storage without eliminating substitution-enumeration cost.