Fine-Tuned Large Language Models for Logical Translation: Reducing Hallucinations with Lang2Logic
Muyu Pan, Dheeraj Kodakandla, Mahfuza Farooque
TL;DR
This work tackles the challenge of converting natural language into precise formal logic while mitigating LLM hallucinations. It introduces Lang2Logic, an end-to-end pipeline that maps English sentences to logical expressions, converts them to CNF via a Lark-based parser and SymPy, and then simplifies the CNF for SAT solving. A hallucination-identification and feedback mechanism uses NLP grammar rules to detect and correct errors, enabling fine-tuning that dramatically improves output reliability. The approach enables reliable, machine-processable logical representations from unstructured text, suitable for automated reasoning, specification debugging, and formal verification workflows.
Abstract
Recent advances in natural language processing (NLP), particularly large language models (LLMs), have motivated the automatic translation of natural language statements into formal logic without human intervention. This enables automated reasoning and facilitates debugging, finding loop invariants, and adhering to specifications in software systems. However, hallucinations-incorrect outputs generated by LLMs are challenging, particularly for logical translation tasks requiring precision. This work introduces a novel framework that inputs English sentences, converts them into logical expressions, and then translates them into Conjunctive Normal Form (CNF) for satisfiability solving. It employs classical NLP techniques with self-defined grammar, symbolic computation libraries, and a fine-tuned language model to reduce hallucinations. In the early experiments, we observed that the fine-tuned model, trained on different grammar settings, could intentionally correct the same types of hallucinations made by the original model. Thus, it provides reliable CNF generation.