Research map / Large language models / Agents, code and math
Divide and Translate: Compositional First-Order Logic Translation and Verification for Complex Logical Reasoning
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes CLOVER, which parses sentences into logical dependency structures, translates them compositionally into first-order logic, and selects formulas via SAT-based verification, reaching SOTA on seven logical reasoning benchmarks with gpt-4o.
Problem
LLMs struggle to translate complex natural language logic into first-order logic (FOL) for neurosymbolic solvers, causing translation errors that limit performance on complex logical reasoning tasks.
Approach
Decompose each sentence via a new logical dependency parsing into an atomic subsentence plus dependents, accumulate components, translate sequentially, and verify candidate formulas with an SAT solver (logical consistency and disproving by counter-interpretation).
Key results
- CLOVER reaches 62.8% on AR-LSAT vs 42.4% for Logic-LM with gpt-4o, and 75.4% on ZebraLogic vs 45.4%.
- CLOVER achieves 99.3% on Deduction and 96.7% on ProofWriter, outperforming Logic-LM on all seven tasks.
- Ablation: removing compositional translation drops AR-LSAT accuracy from 62.8 to 53.3 (direct translation without verification) and ZebraLogic from 75.4 to 45.4.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| compositional first-order logic translation (vs direct translation) (ablation) | CLOVER · AR-LSAT and ZebraLogic | accuracy: +1.7 AR-LSAT, +24.6 ZebraLogic (no verification) | Helped |
| adding SAT-based verification (logical consistency or disproving) to compositional translation (ablation) | CLOVER · AR-LSAT and ZebraLogic | accuracy: +6.9 AR-LSAT and +4.2 ZebraLogic (disproving vs random) | Helped |
| disproving by counter-interpretation vs logical consistency (ablation) | CLOVER · AR-LSAT and ZebraLogic | accuracy: +0.9 AR-LSAT, +1.2 ZebraLogic | Helped |
| CLOVER full method vs Logic-LM with gpt-4o | CLOVER · seven logical reasoning benchmarks | accuracy: AR-LSAT +20.4, ZebraLogic +30.0, Puzzle +19.5, Symbol +8.1, Deduction +4.0, FOLIO +3.4, ProofWriter +1.4 | Helped |
| syntax consistency verification instead of logical consistency (ablation) | CLOVER verification · AR-LSAT and ZebraLogic | accuracy: AR-LSAT 59.7 vs random 55.0 (+4.7); ZebraLogic 70.8 vs 70.0 (+0.8) | Mixed |
| LLM with instruction as verifier (ablation) | CLOVER verification · AR-LSAT and ZebraLogic | accuracy: 53.3 vs random 55.0 on AR-LSAT; 70.0 on ZebraLogic | No clear effect |
| CLOVER vs Logic-LM on execution-based metrics (program accuracy) | CLOVER · AR-LSAT | program accuracy: 17.3 -> 46.8 | Helped |
Surprising findings
- LLM-based verification with instructions gave no improvement over random selection on AR-LSAT and ZebraLogic.
- Logic-LM with gpt-4o shows lower translation accuracy than expected, with logic/syntax errors accounting for 53.7% of its errors.
Limitations
- Higher inference cost than baselines due to generating multiple logical dependency structures and formulas.
- Relies on Z3 SAT solver and manually designed few-shot exemplars; AR-LSAT needs satisfiability/validity selection.
- Only evaluated with GPT-family API models; open-source models not reported.
Experimental setup
Datasets: AR-LSAT ZebraLogic Puzzle (BIG-bench logic grid) Symbol (BIG-bench) Deduction (BIG-bench) FOLIO ProofWriter
Benchmarks: AR-LSAT ZebraLogic Puzzle Symbol Deduction FOLIO ProofWriter
Metrics: accuracy program accuracy execution rate execution accuracy
Baselines: Standard prompting CoT SymbCoT Logic-LM
Builds on: Logic-LM chain-of-thought prompting SymbCoT
Closest papers by meaning
- Learning to Reason via Mixture-of-Thought for Logical Reasoning (ICLR 2026 · similarity 0.87)
- ZebraLogic: On the Scaling Limits of LLMs for Logical Reasoning (ICML 2025 · similarity 0.87)
- Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation (ICLR 2025 · similarity 0.87)
- Reasoning-as-Logic-Units: Scaling Test-Time Reasoning in Large Language Models Through Logic Unit Alignment (ICML 2025 · similarity 0.87)
- On Learning Verifiers and Implications to Chain-of-Thought Reasoning (NeurIPS 2025 · similarity 0.87)
- Boule or Baguette? A Study on Task Topology, Length Generalization, and the Benefit of Reasoning Trace (NeurIPS 2026 · similarity 0.86)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.