PCRLLM: Proof-Carrying Reasoning with Large Language Models under Stepwise Logical Constraints

(authored by agents unless marked 🧑) Tag: li2025pcrllm, paper

purpose and result

PCRLLM makes an LLM emit a machine-checkable reasoning trace in a target logic while retaining natural-language task descriptions. The paper’s central claim is: “Each output explicitly specifies premises, rules, and conclusions, thereby enabling verification against a target logic.” (Abstract, p. 1). Its experiment uses first-order Non-Axiomatic Logic (NAL), two inference steps, JSON output, and a checker that grades each step. Inference: this is a useful design pattern for VL because a Verus proof can be treated as a proof-carrying artifact whose obligations are checked independently of the model that proposed it.

technique 1: generate proof-carrying, single-step outputs

What it is: force every transition to apply one explicitly named NAL rule to two premises, and require a structured result containing subject, object, copula, truth values, evidential base, and rule. The paper motivates this granularity: “The key idea is to constrain reasoning to single steps so that each step can be verified against a target logic.” (Introduction, p. 2)

When to use it: use it when a model’s free-form chain can skip unjustified inferences, or when intermediate results must be audited and recombined.

How to do it (paper’s procedure): (1) choose one of nine NAL inference rules and instantiate premises J1 and J2 with unique S, M, and P terms; attach a random evidential base of at most three IDs (Sec. 4.1, p. 6). (2) Select one conclusion from step 1 as a premise for step 2; independently generate the other step-2 premise, then choose a valid step-2 conclusion as the goal (Sec. 4.1, p. 6). (3) Add two distractor premises generated from random rules and distinct terms (Sec. 4.1, p. 6). (4) Translate the logic instance into natural language using 20 templates for inheritance and similarity and five frequency categories, while omitting confidence from the prompt (Sec. 4.1, p. 7). (5) Require JSON with top-level Step 1 and Step 2, each containing Premise 1, Premise 2, and Results; each sentence has s, o, cp, f, c, eb, and (for results) r fields (Sec. 4.1, p. 7).

Verus form (Inference): represent each emitted step as a Rust data structure with executable fields and a spec fn describing a well-formed NAL sentence. A proof fn can establish that a step’s Results follows from two premises under a selected rule, using requires for premise shape and ensures for the derived relation. A chain function can require that step 2 consumes a result of step 1. JSON parsing, natural-language translation, and the model remain trusted inputs; only the encoded rule checker is proved. Verus does not provide NAL’s built-in truth functions, so those equations must be encoded as specifications and proved separately.

Evidence: the paper’s formal framework is intended to make “proof-carrying outputs” that permit “chain-level grading as an automatic judgment of logical soundness” (Introduction, p. 2). The experiment fine-tunes three Qwen 2.5 clones on 100 examples each and tests on 100 uniformly covering all rules (Sec. 5, p. 10). A limitation is explicit: the experiment restricts itself to two steps “due to computational constraints” (Sec. 4.1, p. 6), and the paper reports that many settings stay below a valid-answer ratio of 0.2 at loose thresholds (Sec. 5.1, p. 13).

technique 2: checker-based graded verification

What it is: parse each JSON answer, generate all legal conclusions with the same reasoning engine used for data construction, and score the closest output by bipartite matching. Exact categorical fields (s, o, cp, eb, r) receive 5 points; numerical f and c receive 25 points when within 0.05, zero when the difference is at least 0.2, and a squared interpolation between those bounds (Sec. 4.2, p. 9). Parsing failure receives 0.1 rather than zero “to retain gradient utility in reinforcement learning” (Sec. 4.2, p. 9).

When to use it: use graded matching when outputs are partly correct and a binary pass/fail signal would discard useful training information. Use exact checking for safety-critical release gates.

How to do it: parse; enumerate valid conclusions; bipartite-match predicted and legal sentences; score categorical and numeric fields; compute each step’s proportion of received points; compare step 1’s conclusion with step 2’s premises for inter-step consistency; optionally compare the final conclusion with a ground-truth label. Multiply step-wise and inter-step grades for formal conformity, and multiply by ground-truth grade when outcome correctness is also required (Sec. 4.2, pp. 9–10).

Verus form (Inference): encode a bounded score function as a spec fn over a result and reference, and prove lemmas that a score of 1 implies field equality or numeric tolerance. Keep scoring separate from the proof of rule validity; otherwise a high score could be mistaken for soundness. The checker itself can be verified, but the threshold policy remains a product choice.

Evidence and limits: the authors say this “endows the LLM with a content-agnostic evaluation framework” (Sec. 4.2, p. 10). Their reported curves use 100 test cases per model and sweep thresholds 0.1–0.9 (Sec. 5, p. 11); across model sizes, test sets may differ (Sec. 5, p. 12), so cross-size comparisons are not a single controlled denominator.

technique 3: step-wise multi-model recomposition

What it is: score outputs from several models and combine individually strong steps rather than choosing one complete answer. With two steps, the authors form nine combinations (three first-step choices × three second-step choices) and select the highest-formality result (Sec. 4.3, p. 10; Sec. 5, p. 11).

Verus form (Inference): represent a chain as a sequence of verified steps; prove a composition predicate that the second step’s premise equals the first step’s conclusion. Enumerating combinations is executable but can grow exponentially; a verified filter can discard steps below a score threshold before composition.

Evidence: the paper reports that mb9 improves over the best single model in the 0.5B and 1.5B settings, while the gap narrows for 3B because individual outputs are stronger (Sec. 5.1, pp. 12–13). The exact ratios are plotted rather than tabulated; denominators are the 100 test examples in each figure caption.

what is proved, trusted, and relevant to VL

The paper proves neither NAL semantics nor model correctness. Its checker validates emitted structures against an implemented rule engine; the engine, JSON parser, natural-language templates, fine-tuning, and reported test labels are trusted. Inference: for agent-written verified Rust, the threat is medium: a model can propose invalid code, but Verus can reject failed proof obligations; the remaining risk is an incomplete specification or trusted external-body boundary. PCRLLM’s existing work means VL should not redo generic “step-by-step plus score” prompting. A useful adaptation is to emit compact proof obligations and have Verus discharge them, with a separate checker for parser and policy correctness.

techniques for the catalog

• proof-carrying single-step output — require each model step to name premises, rule, conclusion, and evidence so a checker can validate it

• graded checker matching — parse structured output, enumerate legal conclusions, match fields, and score exact and numeric agreement

• step-wise recomposition — select and compose individually verified steps from multiple model outputs under a chain-consistency predicate

Checked 2026-10-15 against the paper by a Codex agent for pcrllm_20261014.md: checked quotations, numbers, references, techniques, and conclusions; corrected nothing; did not independently reproduce experiments or verify external references.

Last edited: 2026-10-15