The Right Answer Is Not a Proof: Put Verification Inside the Reasoning Loop

TL;DR for operators

A model can produce a correct answer while taking a logically invalid route to get there. That distinction matters whenever downstream execution depends not only on the answer, but on whether the intermediate decisions are trustworthy.

Chen, Zhou, and Zhang test a lighter alternative to full theorem-proof generation: PRoSFI, which asks a 7B model to expose small, machine-readable reasoning steps that external formal tools can verify.¹ On ProverQA-Hard, outcome-only reinforcement learning reaches 91.31% answer accuracy but only 21.97% GPT Soundness. PRoSFI reaches 92.97% accuracy and 76.07% GPT Soundness. The practical lesson is not that every business workflow should be formalized. It is that when intermediate decisions can be expressed as checkable rules, adding a verification layer can provide a stronger reliability signal than final-answer accuracy alone.

The same verifier can also be used after training. As PRoSFI samples more candidate reasoning paths, verifier-based selection improves measured soundness; simple outcome-oriented majority voting does not show the same pattern. That makes verification a potential control surface for both learning and inference.

High accuracy can conceal weak reasoning

The paper’s sharpest result appears before the new method is even needed.

On ProverQA-Hard, the base Qwen2.5-7B-Instruct model starts at 46.0% final-answer accuracy. Outcome-only GRPO training raises that figure to 91.31%. If accuracy were a sufficient reliability measure, this would look close to a solved problem.

It is not. The same Outcome-CoT model reaches only 21.97% on the paper’s GPT Soundness measure, which asks whether the answer is correct and the reasoning path is judged valid.

That gap changes the engineering target. The problem is no longer simply to reward models for reaching the correct destination. It is to create a signal that distinguishes valid intermediate steps from invalid ones without forcing a modest language model to emit a complete formal proof.

This distinction is especially relevant when reasoning traces affect later actions. A wrong intermediate claim can contaminate a downstream calculation, tool call, or policy decision even when the final answer happens to match the benchmark target.

PRoSFI verifies small reasoning steps instead of full proofs

PRoSFI addresses that gap by inserting a structured layer between natural-language reasoning and a formal prover.

The model still produces an ordinary reasoning trace, but it also emits a sequence of lightweight records. Each record identifies dependencies, a formalized conclusion, and an inference rule, with fewer than five dependencies per step. External tools such as Lean4, Prover9, or Z3 then check the resulting sub-problems after generation.

That timing matters. Verification is not embedded inside every autoregressive token step. The model completes its generation first; checking can happen afterward. The paper therefore treats formal verification as a post-generation supervision layer rather than as a requirement for the model to conduct full theorem proving during rollout.

The reward makes the intended hierarchy explicit. A correct answer with every structured step verified receives 1.0. A correct answer with failed intermediate checks receives 0.3. A correctly formatted but wrong answer receives 0.1, and malformed or failed outputs receive zero.

This is a process reward: the model is trained not only on whether it got the answer right, but also on a machine-checkable property of how it reasoned.

Full Lean generation is the comparison that clarifies the design choice

The paper also trains a direct Lean-generation baseline under broadly matched reinforcement-learning logic. Its purpose is not to establish that Lean is ineffective. It tests whether requiring the model to generate a complete proof script produces a useful training signal under this setup.

The signal is weak. Direct Lean generation achieves a Reward Hit Rate of 13.77% on ProverQA-Hard and 4.35% on ProverQA-Extra. The paper also reports that compiled proofs can collapse into opaque one-line tactics that do not align cleanly with the accompanying natural-language reasoning.

Its task results are mixed rather than uniformly worse: on the Hard split, Direct Lean reaches 92.29% answer accuracy and 33.11% GPT Soundness, both above Outcome-CoT. On the Extra split, however, it falls to 83.15% accuracy and 10.45% GPT Soundness, below the outcome-only baseline.

The relevant comparison is therefore representational. PRoSFI asks the model to formalize small claims that are easier to verify and more closely connected to the visible reasoning trace, instead of asking a 7B model to master end-to-end proof-script generation.

The main result is a soundness gain with little accuracy trade-off

PRoSFI’s strongest evidence comes from the controlled ProverQA comparison.

Relative to Outcome-CoT, PRoSFI increases GPT Soundness by 54.1 percentage points on ProverQA-Hard and 44.2 points on ProverQA-Extra. The corresponding answer-accuracy changes are much smaller: +1.66 and +4.98 points.

That asymmetry is the central result. The method changes measured path validity far more than it changes final-answer accuracy.

ProverQA-Extra is best read as an out-of-distribution robustness test, not a second independent thesis. Its value is that PRoSFI’s advantage persists when the benchmark is made harder and synthesized beyond the main split.

The Knights-and-Knaves experiment extends the check to a second synthetic logic family. After training on 3- to 7-person instances, PRoSFI is evaluated from 2 to 8 people. On the hardest 8-person split, GPT Soundness rises from 47.94% to 80.94%, while accuracy moves from 94.25% to 97.38%. This supports limited cross-dataset generalization within deductive logic; it does not establish transfer to open-ended language reasoning.

Verification also changes what extra inference compute can buy

The paper’s test-time experiment adds a second operational consequence.

Sampling more reasoning paths is useful only if the system has a signal that can distinguish better candidates from worse ones. With PRoSFI, verifier-based selection improves measured soundness as the number of samples increases on both ProverQA-Hard and ProverQA-Extra. Outcome-CoT does not show the same benefit from additional majority-vote-style sampling.

The distinction is consequential for inference design. More samples are not automatically more reliable. Extra compute becomes more valuable when paired with a selector whose signal is aligned with the property being optimized.

The paper reinforces this point with a correlation analysis: PRoSFI Reward Hit is more strongly associated with GPT-assessed soundness than final-answer correctness is. That analysis is supporting evidence for the verifier signal, not proof that Reward Hit perfectly measures whole-chain validity.

Cognaptus inference: put a checkable layer where decisions can be formalized

For an operator building an automated reasoning workflow, the paper suggests a specific design pattern.

When intermediate decisions can be represented as explicit constraints, dependencies, or rules, keep the language model’s natural-language interface but require a parallel structured representation of the decisions that matter. Verify that structure independently. Then use the result in two places: as a training signal when post-training is available, and as a routing or selection signal when multiple candidate outputs are generated.

The affected decision is whether to spend engineering effort on a larger reasoning model, more sampling, full proof generation, or a smaller validation layer. Under the paper’s conditions, the lighter structured layer produces a much stronger process-quality signal than outcome-only reward and a more usable one than direct full-proof generation.

The ROI case therefore depends on formalizability. If the consequential intermediate states cannot be translated into reliable validators, PRoSFI’s mechanism has nothing to attach to.

The verification signal is not a full certificate

Three boundaries matter.

First, a PRoSFI Reward Hit does not guarantee that the entire natural-language chain is valid. The structured propositions may omit parts of the reasoning, leaving uncovered errors between verified steps.

Second, “GPT Soundness” is not itself a theorem-prover metric. The paper uses GPT-OSS-120B to judge reasoning-path validity and manually checks only 20 outputs; that check suggests the judge may be slightly too strict on some PRoSFI cases.

Third, the main evidence comes from synthetic logical reasoning and one Qwen2.5-7B-Instruct base model. The experiments are strong enough to show that the mechanism works in that setting, including OOD and cross-dataset tests. They are not enough to claim that the same soundness gains will appear in open-ended planning, analysis, or ordinary enterprise reasoning.

Reliability improves when the system can inspect the path

The paper’s contribution is not simply another reward function. It shows a workable middle layer between unconstrained chain-of-thought and complete formal theorem proving.

That middle layer changes what can be measured, what can be rewarded, and what additional inference samples can be selected for. In the tested logic settings, those changes produce substantially sounder reasoning without sacrificing strong final-answer accuracy.

For operational AI, the broader takeaway is conditional but concrete: when a workflow contains formalizable intermediate decisions, reliability controls should inspect those decisions directly rather than treating the final answer as sufficient evidence that the process was valid.

Cognaptus: Automate the Present, Incubate the Future.