Into The Limits of Logic: Alignment Methods for Formal Logical Reasoning (2025)

Abstract: We implement Large Language Model Alignment algorithms to formal logic reasoning tasks involving natural-language (NL) to first-order logic (FOL) translation, formal logic inference, and premise retranslation. These methodologies were implemented using task-specific preference datasets created based on the FOLIO datasets and LLM generations. Alignment was based on DPO, this algorithm was implemented and tested on off-the-shelf and pre-aligned models, showing promising results for higher quality NL-FOL parsing, as well as general alignment strategies. In addition, we introduce a new similarity metric ( LogicSim ) between LLM-generated responses and gold standard values, that measures logic-relevant information such as premise count and overlap between answers and expands evaluation of NL-FOL translation pipelines. Our results show that LLMs still struggle with logical inference, however alignment benefits semantic parsing and retranslation of results from formal logic to natural language.

## introduction reasoning using a formal logic language is one of the basis of mathematical thinking. being able to abstract a problem in natural language and express the distinct variables and relationships between them in logical terms helps mitigating ambiguity and unclear relationships. using these formal representations, a step-by-step inference procedure can be carried out in order to obtain a logically valid conclusion of the presented premises. this type of reasoning is crucial for, not only mathematics but, any discipline in need of an explainable decision making process. state-of-the-art large language models (llms) exhibit human-like reasoning capabilities for various tasks such as coding, general academic examination, and reading comprehension @xcite . however, formal logic and mathematical reasoning has proven to be an area of expertise where llms consistently underperform: the claude 3 series of models barely reach a 42% accuracy in the amc 12 (mathematical association of america, 2025), and a 61% on the math dataset @xcite , even with such scores claude outperforms models like gpt 4. given the connection between logic, mathematics, and human cognitive processes @xcite , improving an llm's performance in this area is an open research problem. not only is this interesting as a stand-alone problem, it has very positive implications for the explainability of llms. having a model that can correctly infer and explain step-bystep said process would benefit most current uses of llms. in this article we focus on an end-to-end inference process divided into three main steps. given a set of premises in natural language (nl) the first step is a translation of the premises from natural language to first-order logic (fol). the second step is an llm-based inference procedure based on the fol representations. the final step corresponds to a retranslation of the conclusion from fol to natural language. for each step we implement an llm alignment methodology focused on the corresponding task in order to improve a model's performance, as well as a corresponding evaluation. llm alignment methods are post-training strategies that modify a model's internal weights in order to generate text that caters with human selected responses for a wide range of downstream tasks. alignment strategies, based on reinforcement learning with human feedback @xcite , were originally implemented for auto-matic summarization @xcite . however, recent research uses these strategies to adjust an llm's behavior to generate safe and useful responses @xcite @xcite . interestingly, alignment methods have been shown to improve an llm's performance in tasks outside safety and harmfulness, making them an integral part of post training for newer releases of models @xcite . our approach differs from similar methodologies that work with the same nl-fol workflow by omitting the dependency on prompting, the use of an external solver, and self-verification. by integrating translation and inference capabilities into a model via alignment, we obtain a robust model capable of solving our problem on its own without the need of external tools. additionally, we present a novelty metric that measures logical similarity between two sets of premises based on information concerning predicates and logical connectors. this metric allows us to finely evaluate llms during the workflow, expanding our focus from the single truth value that nl-fol workflows are usually evaluated by. we tested our methodology around the folio dataset @xcite , a human created and annotated dataset focused on natural language to firstorder logic translation and inference, that is easily adaptable to our three step pipeline. evaluation was in accordance to folio and step-specific metrics. our results show that off-the-shelf llms can be easily adjusted to become efficient semantic parsers with a limited amount of information, even being able to follow particular prompt-structures aside from the logical benefit. pre-aligned models perform decently without any logic-based alignment, yet their performance falters after our alignment strategy is applied, suggesting that our methodology needs to be polished in order to work as an additional layer of post-training. ## experiments in this section we describe our end-to-end workflow with a working example, the creation of the preference datasets used for alignment, selected llm checkpoints, and experimental setup. ## results and evaluation