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.

翻译：使用形式语言进行演绎逻辑推理与语言模型（LMs）高度契合，其中将自然语言（NL）翻译为一阶逻辑（FOL）并借助外部求解器，可构建一个可验证且因此可靠推理系统。然而，较小规模的LMs在此翻译任务上常面临困难，由于格式与翻译错误，频繁产生错误的符号输出。现有方法通常依赖自我迭代来纠正这些错误，但此类方法在很大程度上依赖于底层模型的能力。为解决此问题，我们首先对常见错误进行分类，并利用大型语言模型合成的数据对较小LMs进行微调。评估使用所定义错误类别进行。我们引入增量推理，将推理划分为谓词生成和FOL翻译两个阶段，从而提供对模型行为的更强控制，并通过谓词指标衡量以提升生成质量。此分解框架还支持使用针对谓词-元数错误的验证模块，以进一步提升性能。我们的研究在四个逻辑推理数据集上评估了三个模型系列。全面的微调、增量推理及验证模块降低了错误率，增加了谓词覆盖率，并提升了较小LMs的推理性能，使我们更接近开发可靠且易于访问的符号推理系统。