# Divide and Translate: Compositional First-Order Logic Translation and Verification for Complex Logical Reasoning

arXiv: https://arxiv.org/abs/2410.08047 · HTML: https://mlsanity.com/paper/2410.08047/

## Key facts

- Cited by 27 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 21 of its 38 references that are in the map.
- First posted on arXiv 10 Oct 2024.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 21 of 21)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Self-Refine: Iterative Refinement with Self-Feedback](https://mlsanity.com/paper/2303.17651/) (2023)
- [Beyond the Imitation Game: Quantifying and extrapolating the capabilities of language models](https://mlsanity.com/paper/2206.04615/) (2022)
- [Least-to-Most Prompting Enables Complex Reasoning in Large Language Models](https://mlsanity.com/paper/2205.10625/) (2022)
- [LaMDA: Language Models for Dialog Applications](https://mlsanity.com/paper/2201.08239/) (2022)
- [Measuring and Narrowing the Compositionality Gap in Language Models](https://mlsanity.com/paper/2210.03350/) (2022)
- [Teaching Large Language Models to Self-Debug](https://mlsanity.com/paper/2304.05128/) (2023)
- [Decomposed Prompting: A Modular Approach for Solving Complex Tasks](https://mlsanity.com/paper/2210.02406/) (2022)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language](https://mlsanity.com/paper/2012.13048/) (2020)
- [LEVER: Learning to Verify Language-to-Code Generation with Execution](https://mlsanity.com/paper/2302.08468/) (2023)
- [FOLIO: Natural Language Reasoning with First-Order Logic](https://mlsanity.com/paper/2209.00840/) (2022)
- [Large Language Models are Versatile Decomposers: Decompose Evidence and Questions for Table-based Reasoning](https://mlsanity.com/paper/2301.13808/) (2023)
- [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://mlsanity.com/paper/2310.15164/) (2023)
- [SatLM: Satisfiability-Aided Language Models Using Declarative Prompting](https://mlsanity.com/paper/2305.09656/) (2023)
- [Faithful Logical Reasoning via Symbolic Chain-of-Thought](https://mlsanity.com/paper/2405.18357/) (2024)
- [Compositional Semantic Parsing with Large Language Models](https://mlsanity.com/paper/2209.15003/) (2022)
- [LOGIC-LM++: Multi-Step Refinement for Symbolic Formulations](https://mlsanity.com/paper/2407.02514/) (2024)

## Built on by (most cited first, 27 of 27)

- [ZebraLogic: On the Scaling Limits of LLMs for Logical Reasoning](https://mlsanity.com/paper/2502.01100/) (2025)
- [Logical Reasoning in Large Language Models: A Survey](https://mlsanity.com/paper/2502.09100/) (2025)
- [Empowering LLMs with Logical Reasoning: A Comprehensive Survey](https://mlsanity.com/paper/2502.15652/) (2025)
- [SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas](https://mlsanity.com/paper/2505.14615/) (2025)
- [Semantic-Aware Logical Reasoning via a Semiotic Framework](https://mlsanity.com/paper/2509.24765/) (2025)
- [Logical Phase Transitions: Understanding Collapse in LLM Logical Reasoning](https://mlsanity.com/paper/2601.02902/) (2026)
- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [Learning to Reason via Mixture-of-Thought for Logical Reasoning](https://mlsanity.com/paper/2505.15817/) (2025)
- [Dissecting Logical Reasoning in LLMs: A Fine-Grained Evaluation and Supervision Study](https://mlsanity.com/paper/2506.04810/) (2025)
- [A Neurosymbolic Approach to Natural Language Formalization and Verification](https://mlsanity.com/paper/2511.09008/) (2025)
- [Towards a Common Framework for Autoformalization](https://mlsanity.com/paper/2509.09810/) (2025)
- [MuSLR: Multimodal Symbolic Logical Reasoning](https://mlsanity.com/paper/2509.25851/) (2025)
- [Entailment-Preserving First-order Logic Representations in Natural Language Entailment](https://mlsanity.com/paper/2502.16757/) (2025)
- [Are LLMs Stable Formal Logic Translators in Logical Reasoning Across Linguistically Diversified Texts?](https://mlsanity.com/paper/2506.04575/) (2025)
- [Know Your Limits : On the Faithfulness of LLMs as Solvers and Autoformalizers in Legal Reasoning](https://mlsanity.com/paper/2606.16118/) (2026)
- [Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction](https://mlsanity.com/paper/2602.04892/) (2026)
- [Fixing FOLIO and MALLS: Verified Annotations and an LLM-assisted Framework to Focus Human Relabeling](https://mlsanity.com/paper/2606.02837/) (2026)
- [Semiotic logical hexagon theory for LLM logical reasoning](https://mlsanity.com/paper/2607.21933/) (2026)
- [Stratified Consistency Distillation for Natural Language Formalization](https://mlsanity.com/paper/2608.30258/) (2026)
- [From Policy to Logic for Efficient and Interpretable Coverage Assessment](https://mlsanity.com/paper/2601.01266/) (2026)
- [FloCA: Towards Faithful and Logically Consistent Flowchart Reasoning](https://mlsanity.com/paper/2602.14035/) (2026)
- [Neurosymbolic Language Reasoning as Satisfiability Modulo Theory](https://mlsanity.com/paper/2602.18095/) (2026)
- [GenPlanner: From Noise to Plans -- Emergent Reasoning in Flow Matching and Diffusion Models](https://mlsanity.com/paper/2602.18812/) (2026)
- [Technical Report -- A Context-Sensitive Multi-Level Similarity Framework for First-Order Logic Arguments: An Axiomatic Study](https://mlsanity.com/paper/2604.12534/) (2026)
- [Instruct, Not Answer: Using Instruction Privileges in On-Policy Context Distillation](https://mlsanity.com/paper/2609.32201/) (2026)
- [Explaining Textual Entailment with Lexical Entailments: Using LLMs to Supply Lexical Relations for Formal Proofs](https://mlsanity.com/paper/2609.32491/) (2026)
- [Quizzing the Translation: A Prover-Grounded Evaluation Metric for NLrightarrowFOL](https://mlsanity.com/paper/2609.33612/) (2026)

## Abstract (arXiv)

Complex logical reasoning tasks require a long sequence of reasoning, which a large language model (LLM) with chain-of-thought prompting still falls short. To alleviate this issue, neurosymbolic approaches incorporate a symbolic solver. Specifically, an LLM only translates a natural language problem into a satisfiability (SAT) problem that consists of first-order logic formulas, and a sound symbolic solver returns a mathematically correct solution. However, we discover that LLMs have difficulties to capture complex logical semantics hidden in the natural language during translation. To resolve this limitation, we propose a Compositional First-Order Logic Translation. An LLM first parses a natural language sentence into newly defined logical dependency structures that consist of an atomic subsentence and its dependents, then sequentially translate the parsed subsentences. Since multiple logical dependency structures and sequential translations are possible for a single sentence, we also introduce two Verification algorithms to ensure more reliable results. We utilize an SAT solver to rigorously compare semantics of generated first-order logic formulas and select the most probable one. We evaluate the proposed method, dubbed CLOVER, on seven logical reasoning benchmarks and show that it outperforms the previous neurosymbolic approaches and achieves new state-of-the-art results.