ReaLogic-FT: Progressive Neuro-Symbolic Post-Training for Reasoner-Verifiable Logical Reasoning

Large language models often answer logical reasoning questions correctly, yet the reasoning they display is free-form text: no machine can confirm that each step follows from the premises or that the conclusion is supported. Making such reasoning verifiable faces two obstacles. Facts, rules, and inferences must be expressed in a formal language the model does not natively speak, and training on reference proofs ties it to a single derivation per problem, penalizing equally valid alternatives while giving no signal about logical soundness. We present **ReaLogic-FT**, a progressive post-training framework that removes both. The model first learns to translate natural-language statements into the description logic $\mathcal{A}\mathcal{LC}$, decidable yet expressive enough for the theories we retain, so that a reasoner can conclusively check every claimed inference. It then learns to compose such assertions into structured proofs ending in a verdict of *True*, *False*, or *Unknown*. A final reinforcement learning stage drops the reference proofs entirely: an off-the-shelf reasoner checks each candidate derivation step by step, and any proof grounded in the given theory and logically valid is rewarded. We build verifier-checkable versions of ProofWriter and ProntoQA, projecting each problem onto the supported logic and adding queries that can be neither proved nor refuted. Proof supervision raises joint answer-and-proof correctness by over 40 percentage points relative to few-shot prompting. HermiT-guided reinforcement learning then matches or improves the strong SFT initialization on every reported metric and outperforms its semantic-reward ablation in mean performance; these differences are small and not statistically significant, with the clearest gains on deeper ProofWriter instances. Every accepted proof step can be independently audited by a symbolic reasoner against the given formal theory.