Research map / Large language models / Reasoning and chain of thought

Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation

ICLR 2025 · Large language models › Reasoning and chain of thought · approach: Long CoT dynamics and efficiency · 0 citations (OpenAlex)

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 ProverGen, which pairs LLM story generation and translation with the Prover9 symbolic prover to build ProverQA, a 1,500-instance FOL reasoning benchmark, and shows that fine-tuning Llama3.1-8B-Instruct on a ProverQA training set improves ID and OOD performance.

Problem

Existing first-order logic reasoning benchmarks are either template-based (limited diversity and rules) or manually annotated (costly, small, contamination-prone), and often lack accessible reasoning chains.

Approach

A top-down generation pipeline: a symbolic prover (Prover9) computes truth values along a reasoning tree grown backward from the goal, while LLMs produce background stories and translate logic expressions into natural language, yielding scalable, diverse FOL problems with faithful step-by-step proofs.

Key results

• Even with CoT prompting, GPT-4o, Claude-3.5-Sonnet and Mistral-Large-Instruct barely exceed 50% on ProverQA-Hard (50.00, 56.40 and 52.20).
• Finetuning Llama3.1-8B-Instruct on ProverQA training data raises ProverQA Easy/Medium/Hard accuracy to 97.00/90.60/68.20 (+21.4/+44.0/+34.6) from the CoT baseline.
• ProverQA-finetuned Llama3.1-8B-Instruct gains an average of +7.5 points on OOD sets (ProntoQA, ProofWriter, FOLIO), versus -2.0 for ProofWriter-finetuned and -11.4 for FOLIO-finetuned.

Measured effects reported in the paper

Surprising findings

• Removing distractions and shuffling premises makes GPT-4o perform better on ProverQA, i.e., distractors and premise order substantially affect difficulty.
• Models finetuned on ProofWriter or FOLIO lose performance on most OOD sets, showing limited transfer from prior datasets.
• Five-shot prompting did not consistently improve over two-shot prompting.

Limitations

• Shortcut check on only 60 instances; the paper reports that models do not heavily rely on background knowledge, but the sample is small.
• Dataset release is planned rather than completed at submission time, and the authors state they will formally release ProverQA later.
• Hard-subset ProverQA problems remain difficult; the finetuning gain on ProverQA-Hard (to 68.20) is still limited.

Experimental setup

Datasets: ProverQA ProntoQA ProofWriter FOLIO WordNet

Benchmarks: ProverQA ProntoQA ProofWriter FOLIO

Metrics: accuracy

Baselines: GPT-4o Claude-3.5-Sonnet Llama3.1-70B-Instruct Mistral-Large-Instruct Mixtral-8x22B-Instruct Mistral-7B-Instruct Llama3.1-8B-Instruct

Builds on: ProntoQA ProofWriter FOLIO Prover9 chain-of-thought prompting

Closest papers by meaning

• ORACLE: Optimizing Reasoning Abilities of Large Language Models via Constraint-Led Synthetic Data Elicitation (AAAI 2026 · similarity 0.91)
• Reasoning-as-Logic-Units: Scaling Test-Time Reasoning in Large Language Models Through Logic Unit Alignment (ICML 2025 · similarity 0.91)
• Scaling Code-Assisted Chain-of-Thoughts and Instructions for Model Reasoning (NeurIPS 2025 · similarity 0.90)
• Enhancing Reasoning Capabilities of LLMs via Principled Synthetic Logic Corpus (NeurIPS 2024 · similarity 0.90)
• Exploring the Limits of Sub-Billion Language Model Reasoners with Open Training Recipes (ICLR 2026 · similarity 0.89)
• ZebraLogic: On the Scaling Limits of LLMs for Logical Reasoning (ICML 2025 · similarity 0.89)