Improving Symbolic Translation of Language Models for Logical Reasoning

TL;DR

The paper addresses the challenge of small language models translating natural language to first-order logic for deductive reasoning. It proposes a two-stage incremental inference framework—predicate generation followed by FOL translation—coupled with a lightweight verifier to address arity and formatting issues, and it leverages large-LM–generated symbolic data to fine-tune smaller models. Across four datasets, the approach reduces NL-to-FOL translation errors, increases predicate coverage, and improves reasoning performance, including on out-of-distribution data. The work makes symbolic reasoning more accessible for resource-constrained models and lays groundwork for stronger verification in downstream symbolic tasks.

Abstract

The use of formal language for deductive logical reasoning aligns well with language models (LMs), where translating natural language (NL) into first-order logic (FOL) and employing an external solver results in a verifiable and therefore reliable reasoning system. However, smaller LMs often struggle with this translation task, frequently producing incorrect symbolic outputs due to formatting and translation errors. Existing approaches typically rely on self-iteration to correct these errors, but such methods depend heavily on the capabilities of the underlying model. To address this, we first categorize common errors and fine-tune smaller LMs using data synthesized by large language models. The evaluation is performed using the defined error categories. We introduce incremental inference, which divides inference into two stages, predicate generation and FOL translation, providing greater control over model behavior and enhancing generation quality as measured by predicate metrics. This decomposition framework also enables the use of a verification module that targets predicate-arity errors to further improve performance. Our study evaluates three families of models across four logical-reasoning datasets. The comprehensive fine-tuning, incremental inference, and verification modules reduce error rates, increase predicate coverage, and improve reasoning performance for smaller LMs, moving us closer to developing reliable and accessible symbolic-reasoning systems.

Figures (9)

• Figure 1: Framework used to improve symbolic translations. Standard inference can still exhibit formatting errors like repetitive loops. Incremental inference mitigates these by stopping predicate generation early and dividing the process into two stages. A verifier helps address arity error with a predicate "HaveLongVacation" come with arity of 0 and 1 introduced during incremental predicate generation.
• Figure 2: Heatmap of error types counts across datasets, models, and methods.
• Figure 3: Change in total errors with and without incremental inference across all models and datasets. Blue markers denote in-distribution datasets, while olive green markers denote out-of-distribution (OOD) datasets. Refer to Appendix \ref{['app:errordist']} for the numerical values corresponding to this plot.
• Figure 4: The gain from adding ICL verifier on top of Incremental inference. We use the Gemma-3-4B-Instruct as an ICL verifier with 3-shot examples that include arity perturbations from the respective training data.
• Figure 5: The comparison of reasoning accuracy achieved by using between different number of shots in the translation. The red horizontal lines are for reference: the dashed line reports the results under incremental decoding, and the solid line reports the results with the verification on top.