Paper deep dive

LogicGraph : Benchmarking Multi-Path Logical Reasoning via Neuro-Symbolic Generation and Verification

Yanrui Wu, Lingling Zhang, Xinyu Zhang, Jiayu Chang, Pengyu Li, Xu Jiang, Jingtao Hu, Jun Liu

Year: 2026Venue: arXiv preprintArea: cs.AIType: PreprintEmbeddings: 87

Intelligence

Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 90%

Last extracted: 7/20/2026, 1:29:38 PM

Summary

The paper introduces LogicGraph, a benchmark for evaluating multi-path logical reasoning in Large Language Models (LLMs). It addresses the limitation of existing benchmarks that focus on convergent reasoning by providing a dataset with high-depth, multi-path reasoning problems generated via a neuro-symbolic framework. The authors propose a reference-free evaluation framework using a symbolic solver (Prover9) to verify generated proofs, revealing that current LLMs struggle with divergent thinking and fail to explore alternative logical paths as complexity increases.

Entities (8)

LogicGraph · benchmark · 98%Prover9 · softwaretool · 95%Convergent Thinking · concept · 92%Divergent Thinking · concept · 92%LLM · model-type · 90%Deepseek-V3.2-Exp · model · 85%Gemini-3-pro · model · 85%GPT-5.1 · model · 85%

Relation Signals (6)

LogicGraph → evaluates → Multi-Path Logical Reasoning

confidence 95% · LogicGraph, the first benchmark aimed to systematically evaluate multi-path logical reasoning

LogicGraph → containsfeature → High-Depth Multi-Path Reasoning

confidence 92% · This pipeline yields solver-verified reasoning problems formalized by high-depth multi-path reasoning

Prover9 → usedby → LogicGraph Evaluation

confidence 90% · verifies them using a symbolic solver (Prover9)

LogicGraph → usesmethod → Neuro-Symbolic Framework

confidence 90% · constructed via a neuro-symbolic framework that leverages backward logic generation and semantic instantiation

LLMs → exhibitslimitation → Early Commitment to Single Route

confidence 88% · models tend to commit early to a single route and fail to explore alternatives

LogicGraph → revealsgap → Divergence Gap

confidence 85% · LogicGraph exposes this divergence gap and provides actionable insights

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

Abstract:Evaluations of large language models (LLMs) primarily emphasize convergent logical reasoning, where success is defined by producing a single correct proof. However, many real-world reasoning problems admit multiple valid derivations, requiring models to explore diverse logical paths rather than committing to one route. To address this limitation, we introduce LogicGraph, the first benchmark aimed to systematically evaluate multi-path logical reasoning, constructed via a neuro-symbolic framework that leverages backward logic generation and semantic instantiation. This pipeline yields solver-verified reasoning problems formalized by high-depth multi-path reasoning and inherent logical distractions, where each instance is associated with an exhaustive set of minimal proofs. We further propose a reference-free evaluation framework to rigorously assess model performance in both convergent and divergent regimes. Experiments on state-of-the-art language models reveal a common limitation: models tend to commit early to a single route and fail to explore alternatives, and the coverage gap grows substantially with reasoning depth. LogicGraph exposes this divergence gap and provides actionable insights to motivate future improvements. Our code and data will be released at this https URL.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

85,740 characters extracted from source content.

Expand or collapse full text

LogicGraph : Benchmarking Multi-Path Logical Reasoning via Neuro-Symbolic Generation and Verification Yanrui Wu 1,4 , Lingling Zhang 1,4 * , Xinyu Zhang 1,4 , Jiayu Chang 2 , Pengyu Li 1,4 , Xu Jiang 3 ,Jingtao Hu 1 ,Jun Liu 1,5 1 School of Computer Science and Technology, Xi’an Jiaotong University 2 Department of Electrical Engineering, Stanford University 3 School of Computer Science and Technology, Tiangong University 4 Ministry of Education Key Laboratory of Intelligent Networks and Network Security, China 5 Shaanxi Province Key Laboratory of Big Data Knowledge Engineering, China yanrui.wu@stu.xjtu.edu.cn, zhanglling@xjtu.edu.cn Abstract Evaluations of large language models (LLMs) primarily emphasize convergent logical reason- ing, where success is defined by producing a single correct proof. However, many real-world reasoning problems admit multiple valid deriva- tions, requiring models to explore diverse logi- cal paths rather than committing to one route. To address this limitation, we introduceLogic- Graph, the first benchmark aimed to system- atically evaluate multi-path logical reasoning, constructed via a neuro-symbolic framework that leverages backward logic generation and semantic instantiation. This pipeline yields solver-verified reasoning problems formalized by high-depth multi-path reasoning and inher- ent logical distractions, where each instance is associated with an exhaustive set of mini- mal proofs. We further propose a reference- free evaluation framework to rigorously assess model performance in both convergent and di- vergent regimes. Experiments on state-of-the- art language models reveal a common limita- tion: models tend to commit early to a sin- gle route and fail to explore alternatives, and the coverage gap grows substantially with rea- soning depth. LogicGraph exposes this diver- gence gap and provides actionable insights to motivate future improvements. Our code and data will be released athttps://github.com/ kkkkarry/LogicGraph. 1 Introduction Logical reasoning is central to general intelligence, enabling systems to derive valid conclusions from given premises (Kaufman et al., 2011). However, most existing benchmarks for evaluating LLM rea- soning (Han et al., 2024; Xu et al., 2025; Huang et al., 2025; Fu et al., 2025) primarily emphasize convergentthinking—assessing whether a model can reach a correct final conclusion for a given problem. This emphasis leaves underexplored what * Corresponding author P3: escorting(Noah, Emma). Goal: Emma can enter the Museum Collection Vault. Context (Premises): P1: Emma enters the correct PIN at the vault keypad. P2: Emma’s fingerprint matches the vault reader. P3: Noah (security) is escorting Emma to the vault. P4: If Emma’s PIN is correct, then Emma is verified. P5: If Emma’s fingerprint matches, then Emma is verified. P6: If Emma is verified, then Emma can enter the Museum Collection Vault. P7: If Noah is escorting Emma, then Emma can enter the Museum Collection Vault. Museum Collection Vault P6: verified(Emma) -> can_enter(Emma, museum_collection_vault). P1: pin_ok(Emma). P4: pin_ok(Emma) -> verified(Emma). verified(Emma). P2: fingerprint_match(Emma). P5: fingerprint_match(Emma) -> verified(Emma). Noah Emma escorting P7: escorting(Noah, Emma) -> can_enter(Emma, museum_collection_vault). verified(Emma) Figure 1: Illustration of the multi-path reasoning chal- lenge. In the real world, the same conclusion may be entailed via multiple derivation paths. Guilford termsdivergentthinking (Guilford, 1967): the ability to actively generate multiple plausible alternatives for the same conclusion in a problem. In real-world scenarios, reasoning is rarely lin- ear; agents may reach the same conclusion through multiple valid lines of argument and often benefit from exploring alternatives (Yao et al., 2023; Besta et al., 2024). Consider the access-control scenario in Figure 1. The conclusion “Emma can enter the Vault” can be entailed via distinct mechanisms, e.g., through PIN verification (P1, P4, P6), biometrics (P2, P5, P6), or a security escort (P3, P7), illustrat- ing that multiple derivation paths may support the same claim. To bridge this gap between real-world reasoning demands and current benchmark objec- tives, we formulate the multi-path logical reasoning task: given premises and a conclusion, the goal is to enumerate the distinct logically valid derivation paths that entail the conclusion, rather than merely outputting a binary label. However, establishing a benchmark for multi- path reasoning faces three fundamental challenges: (i) Scalable Constructionof exhaustive ground- arXiv:2602.21044v1 [cs.AI] 24 Feb 2026 Benchmark Symbolic Notation Distraction Depth (avg.) Paths (range) Reuse Ratio (range) Task Type Stepwise Evaluation ProofWriter✗2.211.0Binary✗ FOLIO✓✗3.411.0Binary✗ ProntoQA✓✗–Binary✗ RuleTaker✗2.411.0Binary✗ LogicBench✗–Binary/MCQA✗ LogicNLI✗–Ternary✗ Multi-LogiEval✗2.5111.0Binary✗ ProverQA✓4.7311.0Ternary✗ LogicGraph✓6.012∼191.0∼1.9Proof Gen.✓ Table 1: Comparison of LogicGraph (ours) with existing logical reasoning datasets across key characteristics. Distraction refers to the simultaneous occurrence of logical and semantic distraction. truth derivation paths;(i) Reliable Evaluationof open-ended generation; and(i) Cognitive Assess- mentof exploration versus mere correctness. To address these challenges, we introduce LogicGraph, the first benchmark and evaluation framework de- signed for multi-path logical reasoning. Construction via Reverse Logic DAGs.Manu- ally annotating every valid reasoning path in com- plex text is prohibitively error-prone. To guarantee exhaustive ground truth, we employ a backward construction paradigm (Al-Ajlan, 2015). We syn- thesize premises from the conclusion upwards us- ing fundamental argument forms, creating a sym- bolic logic Directed Acyclic Graph (DAG) that is subsequently verbalized. This DAG-based con- struction yields three characteristics of LogicGraph: high-depth multi-path reasoning (with 2–19 valid paths per query and an average depth of 6.01), infer- ence node reuse, and inherent logical distractions. See Table 1 for more details. Neuro-Symbolic Evaluation.Evaluating diver- gent outputs is difficult because traditional string matching is brittle and LLM-as-a-Judge approaches suffer from hallucination (Wang et al., 2025; Szy- manski et al., 2025). We propose areference-free neuro-symbolicevaluator that translates generated natural language steps into formal logic and veri- fies them using a symbolic solver (Prover9). This pipeline rigorously verifies both local step valid- ity and global proof reachability, achieving high agreement with human experts (98.80% Step Ac- curacy and 95.22% Proof Accuracy), thus ensuring a reliable metric for open-ended reasoning. Cognitive Assessment & Insights.Moving be- yond aggregate accuracy metrics, we conduct a dual-faceted analysis ofConvergentandDivergent thinking capabilities. We evaluate a diverse suite of state-of-the-art LLMs on LogicGraph, encom- passing both general-purpose models, such as GPT- 5.1 (OpenAI, 2025a), and reasoning-oriented mod- els, such as Gemini-3-Pro (Deepmind, 2025c). Our results reveal a significant performance gap: while current models demonstrate competence inCon- vergentmetrics, theirDivergentthinking capabili- ties remain significantly constrained, characterized by a sharp decline in solution coverage as logical complexity increases. Although reasoning-oriented models generally outperform general models, the best model fails to achieve reliable exploratory rea- soning. Furthermore, a fine-grained error analysis indicates that failures are predominantly “result- oriented”; models frequently hallucinate interme- diate lemmas to artificially force connections to target conclusions. These insights underscore the substantial gap between current model capabilities and the requirements for divergent thinking. 2 Related Work 2.1 Logical Reasoning Datasets for LLMs Logical reasoning evaluation for LLMs has moved from exam-style comprehension toward bench- marks that scale difficulty and require longer multi-step deductions.Early datasets such as LogiQA (Liu et al., 2020), AR-LSAT (Zhong et al., 2021), and ReClor (Yu et al., 2020) are derived from standardized tests. To better control reasoning depth and reduce linguistic confounds, synthetic benchmarks like RuleTaker (Clark et al., 2020) and ProofWriter (Tafjord et al., 2021) were introduced, and more recent resources provide explicit logi- cal forms or harder multi-step settings (Tian et al., 2021; Saparov and He, 2022; Morishita et al., 2023; Han et al., 2024; Parmar et al., 2024; Chen et al., 2025). However, most benchmarks score only the final answer, leaving the multi-path nature of logi- cal derivation underexplored. 2.2 Symbolic Prover Augmented LLMs Symbolic provers (e.g., Z3 (De Moura and Bjørner, 2008) and proof assistants such as Lean (De Moura et al., 2015)) offer trusted verification of formal statements, motivating neuro-symbolic pipelines that couple LLMs with prover checking. Prior work typically uses LLMs to translate natural lan- guage into executable logical forms and delegate solving/verification to external engines (Pan et al., 2023; Deng et al., 2024; Shen et al., 2025; Xu et al., 2024; Wang et al., 2024a). Provers are exploited for data generation and filtering to ensure logical con- sistency of synthesized corpora (Qi et al., 2025). 3 Task Formulation We formulate the reasoning task as finding all valid justifications for a goal hypothesisGgiven a set of premisesP=p 1 ,p 2 ,...,p n . We refer to each distinct justification as aderivation path. Formally, a derivation path is defined as amini- mal supportset. A setS⊆Pis a minimal support forG, denoted byMinSup(S,G), if and only if (i) SentailsG, (i) no proper subset ofSentailsG: S⊢Gand∀S ′ ⊊S:S ′ ⊬G.(1) The task is to enumerate all such setsSthat satisfyMinSup(S,G). As shown in Figure 1, S escort =P3,P7is a minimal support forG: re- moving eitherP3orP7breaks entailment. Other minimal supports correspond to alternative routes (e.g., PIN- or fingerprint-based). 4 Automatic Dataset Generation Pipeline To ensure both logical rigor and linguistic diversity, we design a three-stage automated pipeline. Stage 1 constructs a symbolic directed acyclic graph to serve as a verifiable reasoning skeleton; Stage 2 translates this symbolic structure into coherent nat- ural language contexts to simulate real-world com- plexity; Stage 3 employs a symbolic solver to verify the validity and consistency of the generated data, filtering out invalid samples. 4.1 Symbolic Logic DAG Generation To mitigate logical inconsistencies in directly gen- erated reasoning texts, we first construct a symbolic directed acyclic graph (Logic DAG) that specifies the ground-truth reasoning structure independent of natural language. As shown in Figure 2(a), we build this graph via backward construction from a target conclusion, which will later be used for semantic instantiation. Graph Primitives: Inference Node & Family. A reasoning path is a sequence ofinference nodes, each being a rule instance(Γ⇒φ)that derives conclusionφfrom alocalpremise setΓ(hereΓis distinct from the global given premise poolPin Section 3). We further group paths intofamiliesif they share the same set of inference nodes. Bottom-Up Construction.We begin by sam- pling a conclusion node. Then, for each current nodeN, we (i) sample a form from a predefined set of fundamental forms (Johnson, 1999) (e.g., Modus Ponens; formal definitions in Appendix A.1), and (i) generate its parent premises. For example, to de- riveQvia Modus Ponens, we create node (P→Q) and nodeP, and recursively expand the newly cre- ated premise nodes. Multi-path Generation.To generate multiple reasoning paths, we first build a reasoning chain to a sampled depth, then pick an intermediate con- clusion on the chain and expand it upward again using the same bottom-up procedure. Repeating this step produces a Logic DAG in which the goal is supported by multiple distinct premise sets. To ensure the ground-truth solution set is exhaustive, we assign a fresh atomic identifier to each newly introduced premise unless it is explicitly shared through an existing node, thereby avoiding unin- tended premise sharing and implicit extra paths. 4.2 Semantic Instantiation Although the Logic DAG ensures validity, it is not semantically rich enough for LLM evaluation. We thus transform each Logic DAG into a natural- language test case through an intermediate Prover9 form, which also enables downstream verification. Following prior work, we define 32 abstract en- tity types (e.g.,Person,Job) (Rosch and Mervis, 1975; Wang et al., 2024b). For each DAG, we sample a domain background, use Deepseek-V3.2- Exp to instantiate abstract symbols into domain- specific Prover9 predicates (e.g., convert A1 to pin_ok(Emma)), and then verbalize the instantiated formulas into a coherent narrative while preserving all logical relations and avoiding unsupported facts. (a) Logic Directed Acyclic Graph Generation Goal Context Random Sample Argument Forms (b) Semantic Instantiation Prover9 Expression Natural Language A1: pin_ok(Emma). A1 -> A2: pin_ok(Emma) -> verified(Emma). "solution_id": 1, "steps": [ "rule_applied": "MP", "premises_used": [ "(A1)", "(A1 -> A2)" ], "conclusion": "A2" , ... , "solution_id": 2... ... solution n solution n-1 solution 1 solution m+1 solution m+2 A1: Emma enters the correct PIN at the vault keypad. A1 -> A2: If Emma’s PIN is correct, then Emma is verified. solution m ... (c) Solver-based Filtering B A -> B MP Inference Node: premisesconclusion. Argument Form ... family m: sol m; m+1; m+2 family n: sol n-1; sol n family 1: sol 1 Logic DAG Person, Animal, Plant, Food, Job, Disease, Drug... Story Background Access control [Person, Job] Failed LLMs [Person, Job] Logic DAG . . . . . . Bottom-up ConstructionTop-down Reasoning Family: Solutions with shared inference nodes. Seven Fundamental Argument Forms MP DS DECD HS MT RAA All Passed pStepwise entailment validation pGlobal derivability validation pContextual consistency check Figure 2: LogicGraph generation pipeline. (a) Logic DAG generation (Section 4.1) builds a goal-to-premise directed acyclic graph by sampling argument forms, yielding multiple valid reasoning paths; paths that share intermediate inference nodes are grouped intofamilies. (b) Semantic instantiation (Section 4.2) translates the DAG into Prover9 formulas and renders the corresponding steps into natural language by instantiating abstract entities and scenario context with LLMs. (c) Solver-based Filtering (Section 4.3) uses Prover9 to validate each instance. 4.3 Solver-based Filtering Multi-path reasoning requires verification to ensure both edge-level (stepwise) soundness and graph- level consistency. Based on the Prover9 expres- sions produced in Sec. 4.2, we validate every sam- ple with Prover9 and discard any sample that fails one of the following checks: (i) Stepwise Entail- ment. For each inference step (i.e., each edge in the Logic DAG), Prover9 verifies that the correspond- ing premises entail the derived statement, ensuring that every deduction is logically valid. (i) Global Derivability. Prover9 confirms that all intermediate statements are derivable from the given premises and earlier derivations, and that the target goal is derivable from the full set of derivations, ensur- ing the graph is globally connected. (i) Contex- tual Consistency. The union of all premises across multiple paths must be satisfiable (e.g., avoiding simultaneousFact(X)and¬Fact(X)), ensuring no contradictions exist within the global context. 4.4 Dataset Characteristics Based on the automatic generation pipeline de- scribed above, LogicGraph is scalable and ro- bust against contamination. Using this dynamic pipeline, we curated a statistically robust bench- mark of 900 instances via stratified sampling. We further divide the dataset into three difficulty tiers according to the number of valid derivation paths (n):Small(2≤n≤4),Medium(5≤n≤7), and Large(n≥8), with 300 instances per tier. As illustrated in Table 1, LogicGraph exhibits three structural propertiesinduced by graph-based generationthat distinguish it from prior reasoning benchmarks:(1) Multi-path High-depth.Unlike predominantly shallow and single-path datasets, each LogicGraph query admits 2–19validproof paths with an average depth of 6.01. This requires not only long-chain deduction but also exploration over multiple proof trajectories.(2) Inference Node Reuse.Unlike chain-style proofs where inter- mediate conclusions are path-specific, LogicGraph allows intermediate inference nodes to be shared across branches (Reuse Ratio: 1.0–1.9). Conse- quently, models must identify and reuse shared subproofs rather than solving each path indepen- dently.(3) Inherent Logical Distractions.Beyond static semantic noise or dead-end facts, LogicGraph introduces structural distractions from the DAG it- self: a premise can be crucial for one valid path yet distracting for another. Models must selectively activate the premises supporting a target trajectory from logically valid but competing evidence. LLM response solution 1 solution m ... Stage 1: Pre-processing & Auto-Formalization LLM Extract all solutions from response Stage 2: Symbolic Verification Stage 3: Hierarchical Error Taxonomy Test Process solution 2 Complete references in solution Convert natural language solution into symbolic format Step 1: Step 2: ✅ ✅ Local Validity Global Validity Information Omission Fact Hallucination Semantic Misinterpretation Semantic Comprehension Rule Misapplication Invalid Deduction Logical Execution Insufficient Premise pass fail pass fail formulas(assumptions) % All premises used in the solution. end_of_list. formulas(goals). % goal. end_of_list (1) Based on Premise1 and Premise4, we can conclude that Emma is verified. (2) Then, combining that result with Premise6, it follows that Emma can enter the Museum Collection Vault. formulas(assumptions). pin_ok(Emma). pin_ok(Emma) -> verified(Emma). end_of_list. formulas(goals). verified(Emma). end_of_list. Premises Based on the ，give as many distinct proof paths for the as possible. Goal Symbolic Solver Figure 3: Three-stage evaluation pipeline for LLM-generated multi-path proofs: (1) pre-processing and auto- formalization extract candidate solutions, resolve references, and translate natural-language steps into a symbolic representation (Prover9-style); (2) a solver is then used to validate local (stepwise) and global validity; (3) failures are annotated along two independent, non-exclusive error axes: semantic comprehension and logical execution. 5Neuro-Symbolic Evaluation Framework The rapid advancement of LLMs in complex reasoning necessitates a more rigorous evalua- tion paradigm. Current evaluation methods often rely on LLM-as-a-Judge. Yet this purely neural paradigm inherits the same weaknesses it aims to diagnose—hallucinations, weak formal grounding, and systematic biases in self-correction—making it easy to miss subtle logical fallacies (Szymanski et al., 2025; Wang et al., 2025; Feng et al., 2025). Conversely, traditional symbolic solvers provide deterministic verification but remain too rigid to handle the informal reasoning traces. To overcome these limitations, we integrate an LLM as a flexible formal translator and a symbolic solver as a rigorous verifier (Bhuyan et al., 2024). In the following sections, we detail the evaluation pipeline, define the metrics, and present a meta- evaluation to validate the framework’s reliability. 5.1 The Evaluation Pipeline As illustrated in Figure 3, our framework evaluates the logical validity of the entire reasoning process via a three-stage pipeline. Stage 1: Pre-processing & Auto-Formalization. To support symbolic verification, we disentangle distinct derivation paths from the model output and reconstruct implicit dependencies (e.g., “From the previous step. . . ”) into an explicit chain. An LLM then translates each NL step into Prover9 syn- tax. To ensure fidelity, we use in-context examples aligning Prover9 expressions from the data synthe- sis stage with their corresponding NL descriptions. Stage 2: Symbolic Verification.We employ Prover9 to verify the reasoning chain at two lev- els: (i)Local Validitychecks whether each stepS t logically follows from its cited premisesP t (i.e., P t ⊢S t ), (i)Global Validityensures whether the final conclusionGcan be derived solely from the subset of premises explicitly used in the solution. Together, these checks ensure grounded proofs and flag hallucinated steps. Stage 3: Hierarchical Error Taxonomy.To pin- point where and why models fail, we propose a two-dimensional error taxonomy (Table 2): Semantic Comprehension.Faithfulness to the pro- vided context, for example, when the model hallu- cinates a relationship not stated in the premises. Logical Execution.Validity of derivation steps, such as applying an incorrect rule or producing a non-sequitur conclusion. DimensionError TypeDefinition Semantic MisinterpretationIncorrectly understood the meaning of facts or rules. Information OmissionIgnored necessary premises or constraints explicitly stated in the context. Semantic Comprehension Fact HallucinationUsed external or fabricated premises not present in the input. Invalid DeductionThe conclusion does not logically follow from the cited premises. Rule MisapplicationApplied a rule that doesn’t match the current premises. Logical Execution Insufficient PremiseCited relevant premises but incomplete for deriving the conclusion. Table 2: The proposed hierarchical error taxonomy. The taxonomy distinguishes between failures in processing input information (Comprehension) and failures in the reasoning process (Execution). 5.2 Cognitive Evaluation Metrics To capture the multifaceted nature of LLM rea- soning, we adopt a two-axis evaluation protocol inspired by Guilford’s Structure of Intellect (Guil- ford, 1967), evaluating convergent and divergent thinking beyond outcome accuracy. Convergent Thinking assesses the model’s abil- ity to derive a single correct conclusion through valid logical steps. We quantify this via three pri- mary dimensions: (i)Success Rate, the proportion of test cases with at least one valid proof path; (i) Precision, the ratio of valid solutions to total gener- ations, reflecting hallucination resistance; and (i) Shortest Path Finding Rate, the percentage of so- lutions matching the minimum ground-truth step count, which measures reasoning conciseness. Divergent Thinking evaluates creativity and flex- ibility in discovering multiple distinct paths. This is measured by: (i)Diversity (Solution Recall), de- fined asR sol =|S Model ∩S GT |/|S GT |, which quan- tifies the coverage of the solution space; (i)Versa- tility (Family Recall), which reflects the agility to switch between distinct reasoning strategies; and (i)Originality, which highlights the ability to identify rare paths by calculating the inverse fre- quency of a solution’s discovery across all models. EvaluatorReferenceAcc(S)Acc(P) LLM-as-a-Judge Baselines Deepseek-V3.2-ExpRequired77.2571.46 Deepseek-V3.2-T ∗ Required87.1983.59 Gemini-3-ProRequired86.1183.91 Neuro-Symbolic Ours(Gemini)None97.5794.85 Ours(Deepseek)None98.8095.22 Table 3: Meta-evaluation results comparing agreement with human annotators. Acc(S) and Acc(P) denote per- step and overall proof validity, respectively. 5.3 Evaluator Reliability Validation To validate our framework, we measure agreement with expert human judgments on proof validity and compare against reference-based LLM-as-a-Judge baselines. As shown in Table 3, our reference- free neuro-symbolic evaluator (with Prover9) is robust across backbone LLMs: both the Gemini- 2.5-Flash and DeepSeek-V3.2-Exp versions outper- form reference-based LLM-as-a-Judge baselines, with DeepSeek-V3.2-Exp achieving the highest agreement. This suggests symbolic verification re- duces false positives from fluent-but-invalid traces. 6 Experiments 6.1 Experimental Setting We conduct comprehensive experiments on Logic- Graph to evaluate model performance across vary- ing degrees of logical complexity. Baselines.We evaluate several SOTA LLMs on LogicGraph,including both proprietary APIs and open-weight releases, including GLM- 4.6 (ZhipuAI, 2025), GPT-5.1 (OpenAI, 2025a), Claude-Sonnet-4.5 (Anthropic, 2025), o3/o4- mini (OpenAI, 2025c), Gemini 2.5/3 (Deepmind, 2025a,b,c), as well as open source models such as GPT-OSS-120B (OpenAI, 2025b), Qwen3-235B- A22B (and its Thinking variant) (Yang et al., 2025), QwQ-32B (Team, 2025b), and DeepSeek- V3.2-Exp (and its Thinking variant) (DeepSeek-AI, 2025). For all models, we use a unified prompting protocol that encourages the model to produce as many independent and verifiable solution paths as possible under a fixed structured answer template; prompt templates are given in Appendix E. Evaluation Flow.Following the evaluation re- sults in Sec. 5.1, and considering the accuracy–cost trade-off in deployment, we select DeepSeek-V3.2- Exp as the default backbone model for our experi- ments; see Appendix F for the detailed prompt. 6.2 Main Results Table 4 presents the comparative analysis of Gen- eral and Reasoning-Oriented models on Logic- Model Convergent(↑)Divergent(↑) Token Eff. (Overall)↓SR Avg; S/M/L Prec. Avg; S/M/L SPF Avg; S/M/L Div. Avg; S/M/L Vers. Avg; S/M/L Orig. Avg; S/M/L General Models GLM-4.6 21.11 19.67/21.00/22.67 8.47 11.20/7.62/6.58 14.00 15.00/13.00/14.00 6.19 9.83/5.30/3.45 9.66 13.50/8.35/7.14 2.64 1.85/2.71/3.36 7274.96 GPT-OSS-120B 12.22 13.67/11.33/11.67 9.97 12.07/8.06/9.79 7.89 9.67/8.67/5.33 3.09 5.75/2.12/1.41 5.50 9.75/3.76/2.99 1.21 1.48/1.06/1.08 27120.45 GPT-5.1 21.56 19.67/20.67/24.33 9.69 10.94/8.76/9.37 13.56 14.00/13.67/13.00 5.98 8.86/5.02/4.07 9.96 13.11/8.39/8.39 3.20 1.94/3.03/4.63 7096.54 Qwen3-235B-A22B 29.56 30.67/27.67/30.33 13.89 17.47/12.69/11.52 17.33 20.67/17.00/14.33 8.23 13.28/6.60/4.80 14.65 21.67/12.14/10.14 4.02 3.49/3.46/5.11 7401.54 Claude-Sonnet-4.5 53.11 52.00/51.67/55.67 36.05 39.60/34.09/34.47 29.22 31.33/30.67/25.67 12.88 19.94/10.97/7.74 25.42 37.00/21.96/17.31 8.26 7.24/7.83/9.7 3431.10 Deepseek-V3.2-Exp 61.00 57.33/61.67/64.00 52.04 49.34/49.90/56.89 34.44 33.67/35.33/34.33 16.54 25.39/14.51/9.71 31.38 43.67/28.64/21.84 10.20 8.48/10.32/11.79 3397.51 Reasoning-Oriented Models o3 58.33 54.33/55.00/65.67 50.79 47.77/47.39/57.22 39.44 43.00/38.33/37.00 17.94 28.28/14.70/10.84 30.02 41.33/25.71/23.01 9.31 7.51/8.50/11.991 9446.91 o4-mini 57.78 56.67/57.33/59.33 51.38 48.99/49.40/55.76 33.67 38.00/32.33/30.67 16.17 25.14/14.04/9.34 29.20 40.42/27.21/19.97 8.64 7.77/8.84/9.31 6903.90 QwQ-32B 50.89 48.00/49.00/55.67 25.91 27.66/24.25/25.81 35.44 34.33/37.33/34.67 16.20 23.81/14.48/10.32 27.38 34.97/25.13/22.04 7.64 6.06/7.53/9.32 12228.78 Qwen3-235B-A22B-T ∗ 91.22 85.00/93.33/95.33 76.89 73.08/78.49/79.11 70.22 68.00/75.33/67.33 45.83 59.42/45.42/32.64 69.12 76.67/69.28/61.42 21.61 16.05/21.98/26.79 5940.66 Kimi-K2-T ∗ 72.22 69.67/74.67/72.33 48.20 46.51/50.67/47.42 51.44 56.00/54.33/44.00 29.04 42.06/27.68/17.37 44.94 58.08/44.52/32.22 13.29 10.71/14.40/14.77 13764.23 Claude-Sonnet-4.5-T ∗ 61.67 61.67/59.67/63.67 47.82 50.58/46.05/46.82 34.22 40.00/34.00/28.67 15.66 25.47/13.07/8.43 30.15 45.31/26.23/18.92 9.72 8.63/9.43/11.1 3476.57 Deepseek-V3.2-Exp-T ∗ 88.00 82.00/89.33/92.67 76.96 71.02/77.83/82.04 66.33 67.33/69.67/62.00 39.76 53.81/39.22/26.25 61.02 70.67/61.32/51.07 18.72 14.47/18.97/22.71 5582.40 Gemini-2.5-Flash 85.56 82.00/85.00/89.67 67.04 63.82/67.16/70.14 65.89 67.00/66.33/64.33 41.35 53.28/40.43/30.33 61.43 69.61/60.44/54.24 20.34 14.97/19.49/26.56 6835.60 Gemini-2.5-Pro 87.78 82.67/88.67/92.00 73.38 72.20/72.90/75.03 72.78 72.67/75.67/70.00 51.07 60.56/53.11/39.53 69.13 74.50/69.83/63.07 23.77 16.17/24.33/30.81 4414.16 Gemini-3-Pro-Preview 96.11 93.00/98.00/97.33 90.10 89.11/91.89/89.31 80.33 80.00/82.67/78.33 59.60 70.03/60.30/48.47 79.44 83.03/79.99/75.30 29.31 20.96/30.3/36.67 1302.15 Table 4: Comprehensive model comparison on the LogicGraph, covering convergent metrics (Success Rate/Precision/Short Path Finding Rate), divergent metrics (Diversity/Versatility/Originality), and overall To- ken Efficiency (↓) across Small/Medium/Large. In each cell,Avg(over Small/Medium/Large) is bolded; the second line reports Small/Medium/Large in order. -T ∗ denotes Thinking. Graph. We synthesize the experimental results into three key observations: Reasoning-oriented models achieve stronger performance without extra cost.Overall, reasoning-oriented models outperform general models on convergent metrics, indicating that stronger inference is essential for logic tasks. No- tably, Gemini-3-Pro-Preview establishes a new state-of-the-art on all metrics, while also exhibiting the highest token efficiency, suggesting that im- proved reasoning reduces wasted generation on in- correct branches and reaches valid reasoning paths more directly. Top models remain concentrated on a narrow subset of valid reasoning paths.Despite near- saturated Success Rates for top models, divergent metrics remain markedly lower, revealing a gap between finding one valid reasoning path and enu- merating many. This indicates that current models tend to concentrate on a limited subset of high- probability paths rather than systematically explor- ing diverse alternatives. Multiplicity: Models can switch strategies, but cannot enumerate many valid paths.As the number of valid reasoning paths increases from Small to Large, both Versatility and Diversity de- cline across models. However, Versatility is typ- ically more robust than Diversity, indicating that models can still reach multiple high-level strategies but increasingly fail to exhaustively list the many concrete variants implied by each strategy. 6.3 Depth-Induced Performance Degradation As shown in figure 4, as reasoning depth increases, both success rate and precision decline steadily, in- dicating that errors accumulate and amplify across multi-hop chains. Reasoning models remain more robust in the mid-to-high step ranges, while general 2-3456789-10 Average Step Length (Steps) 0 20 40 60 80 100 Success Rate (%) Success Rate 2-3456789-10 Average Step Length (Steps) 0 20 40 60 80 100 Precision (%) Precision 2-3456789-10 Average Step Length (Steps) 0 20 40 60 80 100 Shortest Path Finding Rate (%) Shortest Path Finding Rate 2-3456789-10 Average Step Length (Steps) 0 20 40 60 80 100 Diversity (%) Diversity 2-3456789-10 Average Step Length (Steps) 0 20 40 60 80 100 Versatility (%) Versatility 2-3456789-10 Average Step Length (Steps) 0 20 40 60 80 100 Originality (%) Originality claude-sonnet-4-5-20250929 claude-sonnet-4-5-20250929-thinking Deepseek-V3.2-Exp Deepseek-V3.2-Exp-Thinking gemini-2.5-flash gemini-2.5-pro gemini-3-pro-preview glm-4.6 gpt-5.1 gpt-oss-120b o3 o4-mini kimi-k2-thinking qwen3-235b-a22b qwq-32b qwen3-235b-a22b-thinking-2507 Figure 4: Performance dynamics of LLMs across varying reasoning depths. Solid lines represent Reasoning-oriented LLMs; dashed lines represent General-purpose LLMs. Gemini-3 Pro DS-V3.2 (T) o4-mini Claude-4.5 DS-V3.2 GPT-5.1 QwQ-32B Qwen3-235B 0 20 40 60 80 Error Rate (% of Total Questions) Error Types Semantic Misinterpretation Information Omission Fact Hallucination Invalid Deduction Rule Misapplication Insufficient Premise Figure 5: Comparative Analysis of Error Type: Seman- tic Comprehension vs. Logical Execution. models degrade more sharply, suggesting reasoning optimization strengthens cross-hop consistency and error tolerance. Beyond correctness, Diversity and Versatility often drop earlier and faster, implying that deeper puzzles drive models toward narrower reasoning patterns and explore fewer alternatives. 6.4 Analysis of Error Categories Figure 5 presents the error types distribution across representative models (Appendix B provides results for all evaluated models), while most models main- tain relatively low error rates in semantic compre- hension, they exhibit a pronounced spike in logical execution errors, particularly invalid deduction and insufficient premise. This suggests that in proof tasks, LLMs may generate result-oriented fabrica- tions. When a valid logical chain from premises to conclusion is unavailable, they tend to invent •Gemini-3-Pro •o3 solution1 solution2 solution3 •Qwen3-235b solution1 solution1 solution2 solution3~6 Success Rate: 100% Precision: 100% SPF: 100% (GT1) (GT1) (GT3) ❌ Success Rate: 100% Precision: 100% SPF: 100% Success Rate: 100% Precision: 2/6=33.3% SPF: 100% Diversity: 3/4=75% Versatility: 3/3=100% Originality: 1/2+1/4+1/3=1.58 Diversity: 1/4=25% Versatility: 1/3=33.3% Originality: 1/4=0.25 Diversity: 1/4=25% Versatility: 2/3=66.7% Originality: 1/4+1/3=0.58 ✅ ✅ ✅ ✅ ✅ ✅ (GT1) (GT3) (GT4) Covergent MetricDivergent Metric •Qwen3-235b-T* solution1 solution2 solution3 ✅ ✅ (GT1) (GT4) solution4 ✅ (GT2) Diversity: 4/4=100% Versatility: 3/3=100% Originality: 1/2+1/4+1/3+1=2.08 Success Rate: 100% Precision: 100% SPF: 100% ✅ (GT3) Figure 6: Model performance on case (Figure 8). GT represents the ground truth paths. intermediate lemmas or make unjustified leaps to produce a superficially complete proof. 6.5 Case Study Figure 6 shows why we need Divergent Metrics beyond standard scores. Further analysis uncov- ers hidden reasoning flaws even when answers are correct; see Appendix C.1 for more details. 7 Conclusion We develop a neuro-symbolic generation and solver-verification pipeline for constructing high- depth multi-path logical reasoning problems. Based on it, we build LogicGraph, the first bench- mark where each instance comes with an exhaus- tive set of minimal proofs and logical distractions. Evaluations of state-of-the-art LLMs reveal a clear limitation: models often fixate on one route and increasingly miss alternatives as depth grows. Log- icGraph offers a testbed to drive future models toward more flexible, comprehensive reasoning. Limitations While LogicGraph represents a significant step to- wards evaluating complex reasoning, we acknowl- edge the following limitations: Synthetic-to-Real Gap.Although we employ ad- vanced LLMs to render symbolic logic into natural language narratives, the dataset remains syntheti- cally constructed. Real-world reasoning often in- volves ambiguity, fuzzy logic, and probabilistic inference, which are strictly controlled in our cur- rent discrete logic framework. The clean logical separation in our benchmark may not fully reflect the noisy information retrieval challenges found in the real world. Computational Cost.The multi-path problems neuro-symbolic verification process is computa- tionally intensive compared to simple multiple- choice evaluations. This may pose challenges for rapid, low-resource model evaluation. Ethical Statement LogicGraph is a fully synthetic benchmark built from abstract entities and explicit logic rules, so it contains no personally identifiable information or copyright-protected text, eliminating risks related to data privacy or intellectual property infringe- ment. A remaining concern is that LLM-based sur- face realization can introduce latent social biases; we reduce this risk by using constrained templates and distributing instances across multiple neutral domains to avoid skewed coverage. We also ac- knowledge the environmental cost of multi-path reasoning and neuro-symbolic verification, which can be more computationally intensive than stan- dard evaluations; future work will prioritize more efficient pipelines to reduce the associated carbon footprint. Although stronger reasoning may be repurposed in dual-use settings, the benchmark’s abstract, formal scope limits direct harmful applica- bility. We will release the LogicGraph benchmark artifacts, including dataset instances, generation scripts, and evaluation code, under a permissive open-source license to facilitate reuse and repro- ducibility. References Ajlan Al-Ajlan. 2015. The comparison between forward and backward chaining.International Journal of Machine Learning and Computing, 5(2):106–113. Anthropic. 2025. Introducing claude sonnet 4.5. Maciej Besta, Nils Blach, Ales Kubicek, Robert Gersten- berger, Michal Podstawski, Lukas Gianinazzi, Joanna Gajda, Tomasz Lehmann, Hubert Niewiadomski, Pi- otr Nyczyk, and 1 others. 2024. Graph of thoughts: Solving elaborate problems with large language mod- els. InProceedings of the AAAI conference on artifi- cial intelligence, volume 38, pages 17682–17690. Bikram Pratim Bhuyan, Amar Ramdane-Cherif, Ravi Tomar, and TP Singh. 2024. Neuro-symbolic artifi- cial intelligence: a survey.Neural Computing and Applications, 36(21):12809–12844. Michael K Chen, Xikun Zhang, and Dacheng Tao. 2025. Justlogic: A comprehensive benchmark for evaluat- ing deductive reasoning in large language models. arXiv preprint arXiv:2501.14851. Peter Clark, Oyvind Tafjord, and Kyle Richardson. 2020. Transformers as soft reasoners over language.arXiv preprint arXiv:2002.05867. Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient smt solver. ininternational conference on tools and algorithms for the construction and analy- sisof systems. Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. 2015. The lean theorem prover (system description). InInter- national Conference on Automated Deduction, pages 378–388. Springer. Google Deepmind. 2025a. Gemini 2.5 flash. Google Deepmind. 2025b. Gemini 2.5 pro. Google Deepmind. 2025c. Gemini 3.0 pro. DeepSeek-AI. 2025. Introducing deepseek-v3.2-exp. Shujie Deng, Honghua Dong, and Xujie Si. 2024. En- hancing and evaluating logical reasoning abilities of large language models. InICLR 2024 Workshop on Secure and Trustworthy Large Language Models. Yuanning Feng, Sinan Wang, Zhengxiang Cheng, Yao Wan, and Dongping Chen. 2025. Are we on the right way to assessing llm-as-a-judge?arXiv preprint arXiv:2512.16041. Yumeng Fu, Jiayin Zhu, Lingling Zhang, Bo Zhao, Shaoxuan Ma, Yushun Zhang, Yanrui Wu, and Wen- jun Wu. 2025. Geolaux: A benchmark for evalu- ating mllms’ geometry performance on long-step problems requiring auxiliary lines.arXiv preprint arXiv:2508.06226. Joy Paul Guilford. 1967.The nature of human intelli- gence.McGraw-Hill. Simeng Han, Hailey Schoelkopf, Yilun Zhao, Zhent- ing Qi, Martin Riddell, Wenfei Zhou, James Coady, David Peng, Yujie Qiao, Luke Benson, and 1 oth- ers. 2024. Folio: Natural language reasoning with first-order logic. InProceedings of the 2024 Con- ference on Empirical Methods in Natural Language Processing, pages 22017–22031. Kaixuan Huang, Jiacheng Guo, Zihao Li, Xiang Ji, Ji- awei Ge, Wenzhe Li, Yingqing Guo, Tianle Cai, Hui Yuan, Runzhe Wang, and 1 others. 2025. Math- perturb: Benchmarking llms’ math reasoning abil- ities against hard perturbations.arXiv preprint arXiv:2502.06453. Robert M. Johnson. 1999.A Logic Book: Fundamen- tals of Reasoning. Wadsworth Publishing Company, Belmont, CA, USA. Scott Barry Kaufman, Colin G DeYoung, Deidre L Reis, and Jeremy R Gray. 2011. General intelligence pre- dicts reasoning ability even for evolutionarily familiar content.Intelligence, 39(5):311–322. Jian Liu, Leyang Cui, Hanmeng Liu, Dandan Huang, Yile Wang, and Yue Zhang. 2020.Logiqa: A challenge dataset for machine reading compre- hension with logical reasoning.arXiv preprint arXiv:2007.08124. Terufumi Morishita, Gaku Morio, Atsuki Yamaguchi, and Yasuhiro Sogawa. 2023. Learning deductive rea- soning from synthetic corpus based on formal logic. InInternational Conference on Machine Learning, pages 25254–25274. PMLR. OpenAI. 2025a. Gpt-5.1: A smarter, more conversa- tional chatgpt. OpenAI. 2025b. gpt-oss-120b & gpt-oss-20b model card.Preprint, arXiv:2508.10925. OpenAI. 2025c. Introducing openai o3 and o4-mini. Liangming Pan, Alon Albalak, Xinyi Wang, and William Wang. 2023. Logic-lm: Empowering large language models with symbolic solvers for faithful logical reasoning. InFindings of the Association for Computational Linguistics: EMNLP 2023, pages 3806–3824. Mihir Parmar, Nisarg Patel, Neeraj Varshney, Mutsumi Nakamura, Man Luo, Santosh Mashetty, Arindam Mitra, and Chitta Baral. 2024. Logicbench: To- wards systematic evaluation of logical reasoning ability of large language models.arXiv preprint arXiv:2404.15522. Chengwen Qi, Ren Ma, Bowen Li, He Du, Binyuan Hui, Jinwang Wu, Yuanjun Laili, and Conghui He. 2025. Large language models meet symbolic provers for logical reasoning evaluation.arXiv preprint arXiv:2502.06563. Eleanor Rosch and Carolyn B Mervis. 1975. Family resemblances: Studies in the internal structure of categories.Cognitive psychology, 7(4):573–605. Abulhair Saparov and He He. 2022. Language models are greedy reasoners: A systematic formal analysis of chain-of-thought.arXiv preprint arXiv:2210.01240. Ziju Shen, Naohao Huang, Fanyi Yang, Yutong Wang, Guoxiong Gao, Tianyi Xu, Jiedong Jiang, Wanyi He, Pu Yang, Mengzhou Sun, and 1 others. 2025. Real- prover: Retrieval augmented lean prover for mathe- matical reasoning.arXiv preprint arXiv:2505.20613. Annalisa Szymanski, Noah Ziems, Heather A Eicher- Miller, Toby Jia-Jun Li, Meng Jiang, and Ronald A Metoyer. 2025. Limitations of the llm-as-a-judge approach for evaluating llm outputs in expert knowl- edge tasks. InProceedings of the 30th International Conference on Intelligent User Interfaces, pages 952– 966. Oyvind Tafjord, Bhavana Dalvi, and Peter Clark. 2021. Proofwriter: Generating implications, proofs, and abductive statements over natural language. InFind- ings of the Association for Computational Linguistics: ACL-IJCNLP 2021, pages 3621–3634. Qwen Team. 2025a. Qwen3: Think deeper, act faster. Qwen Team. 2025b. Qwq-32b: Embracing the power of reinforcement learning. Jidong Tian, Yitian Li, Wenqing Chen, Liqiang Xiao, Hao He, and Yaohui Jin. 2021. Diagnosing the first-order logical reasoning ability through logicnli. InProceedings of the 2021 Conference on Empiri- cal Methods in Natural Language Processing, pages 3738–3747. Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang. 2024a. Theoreml- lama: Transforming general-purpose llms into lean4 experts.arXiv preprint arXiv:2407.03203. Siyuan Wang, Zhongyu Wei, Yejin Choi, and Xiang Ren. 2024b. Can llms reason with rules? logic scaffolding for stress-testing and improving llms.arXiv preprint arXiv:2402.11442. Yidong Wang, Yunze Song, Tingyuan Zhu, Xuanwang Zhang, Zhuohao Yu, Hao Chen, Chiyu Song, Qi- ufeng Wang, Cunxiang Wang, Zhen Wu, and 1 oth- ers. 2025. Trustjudge: Inconsistencies of llm-as- a-judge and how to alleviate them.arXiv preprint arXiv:2509.21117. Fangzhi Xu, Qika Lin, Jiawei Han, Tianzhe Zhao, Jun Liu, and Erik Cambria. 2025. Are large language models really good logical reasoners? a comprehen- sive evaluation and beyond.IEEE Transactions on Knowledge and Data Engineering. Fangzhi Xu, Zhiyong Wu, Qiushi Sun, Siyu Ren, Fei Yuan, Shuai Yuan, Qika Lin, Yu Qiao, and Jun Liu. 2024. Symbol-llm: Towards foundational symbol- centric interface for large language models. InPro- ceedings of the 62nd Annual Meeting of the Associa- tion for Computational Linguistics (Volume 1: Long Papers), pages 13091–13116. An Yang, Anfeng Li, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Gao, Chengen Huang, Chenxu Lv, and 1 others. 2025.Qwen3 technical report.arXiv preprint arXiv:2505.09388. Shunyu Yao, Dian Yu, Jeffrey Zhao, Izhak Shafran, Tom Griffiths, Yuan Cao, and Karthik Narasimhan. 2023. Tree of thoughts: Deliberate problem solving with large language models.Advances in neural information processing systems, 36:11809–11822. Weihao Yu, Zihang Jiang, Yanfei Dong, and Jiashi Feng. 2020.Reclor: A reading comprehension dataset requiring logical reasoning.arXiv preprint arXiv:2002.04326. ZhipuAI. 2025. Glm-4.6. Wanjun Zhong, Siyuan Wang, Duyu Tang, Zenan Xu, Daya Guo, Jiahai Wang, Jian Yin, Ming Zhou, and Nan Duan. 2021. Ar-lsat: Investigating analytical reasoning of text.arXiv preprint arXiv:2104.06598. A Benchmark A.1 Argument Forms In this paper, we adopt the seven most basic ar- gument forms (Johnson, 1999), as summarized in Table 5. Using these core rules, many inference patterns that are not listed explicitly can often be obtained by composing several basic forms. As an illustration, we show how the Destructive Dilemma (D) can be derived using only the argument forms in Table 5. Derived rule (D). D:((p→q)∧(r→s)∧(¬q∨¬s))⊢(¬p∨¬r). Derivation using only the forms in Table X. 1. p→qPremise 2. r→sPremise 3.¬q∨¬sPremise 4.¬q→¬pfrom 1 by MT 5.¬s→¬rfrom 2 by MT 6.¬p∨¬rfrom 3, 4, 5 by CD A.2 Dataset Distribution Figure 7 visualizes the LogicGraph’s distribution along two key dimensions: (1) the average number of reasoning steps (x-axis), which reflects reason- ing complexity, and (2) the number of valid ground- truth solutions (y-axis), which reflects solution- space ambiguity. The bubble size and color both indicate the sample frequency at each coordinate. A notable observation is that the two dimensions are largely independent. The Pearson correlation between average reasoning steps and the number of valid solutions is approximatelyρ≈0.06, in- dicating a negligible linear relationship. This sug- gests that our construction effectively decouples reasoning depth from the size of the solution space, enabling controlled evaluation of both complexity and ambiguity within a single benchmark. A.3 Dataset Domain Diversity Analysis As illustrated in Table 6, LogicGraph encompasses over 90 distinct specific fields spanning 7 major cat- egories: Business & Finance, Environment & Sci- ence, Medical & Health, Law & Governance, Engi- neering & Tech, Humanities & Society, and Trans- portation & Urban. The distribution includes high- stakes environments such as Emergency Medicine, Clinical Trials, and Network Security, as well as complex professional scenarios like Regulatory Argument FormFormal NotationDefinition (informal) Modus Ponens (MP)((p→q)∧p)⊢qIfp→qandp, thenq. Modus Tollens (MT)((p→q)∧¬q)⊢¬pIfp→qand¬q, then¬p. Hypothetical Syllogism (HS)((p→q)∧(q→r))⊢(p→r)Ifp→qandq→r, thenp→r. Disjunctive Syllogism (DS)((p∨q)∧¬p)⊢qIfp∨qand¬p, thenq(symmetrically,¬qyieldsp). Constructive Dilemma (CD)((p→q)∧(r→s)∧(p∨r))⊢(q∨s)Ifp→q,r→s, andp∨r, thenq∨s. Reductio ad Absurdum (RAA)((p→q)∧(p→¬q))⊢¬pIf assumingpleads to a contradiction (e.g., bothqand¬q), then¬p. Disjunction Elimination (DE)((p∨q)∧(p→r)∧(q→r))⊢rIfp∨q, andp→randq→r, thenr. Table 5: Basic argument forms and their formal notations. 345678910 Average Reasoning Steps 2.5 5.0 7.5 10.0 12.5 15.0 17.5 Number of Solutions Distribution of Dataset by Complexity and Ambiguity 5 10 15 20 25 Number of Datasets Figure 7: Distribution of the benchmark dataset by av- erage steps and number of solutions. The bubble size indicates the frequency of samples. Compliance, Industrial Engineering, and Legal Pro- cedures. This diversity ensures that the evaluation reflects the model’s ability to handle specialized knowledge and reasoning patterns inherent to dif- ferent professional and practical domains. A.4 Examples To illustrate the three levels of complexity in our dataset, we present one representative ex- ample from each category:Small(Figure 8), Medium(Figure 9), and Large(Figure 10). These cases are categorized by the number of distinct reasoning paths available for the given problem. Test 5 (Small Case) This case represents a sce- nario with a limited number of paths, containing a total of 4 valid solutions. We provide a de- tailed look at Solution 2, which features compre- hensive annotations including symbolic representa- tions, natural language descriptions, and a complete reasoning chain linking premises to conclusions. Notably, Solution 1 and Solution 4 are classified into the same reasoning family (Family 1). This grouping is due to the presence of shared reasoning nodes between the two paths, demonstrating our method of clustering logically similar derivations. Test 664 (Medium Case) Representing medium complexity, this test case contains 7 solutions orga- nized into 4 reasoning families. The length of these solutions varies from 5 to 13 steps. The largest family, Family 1, encompasses 4 distinct paths, highlighting the potential for multiple variations within a single line of reasoning. Test 821 (Hard Case) This case illustrates a high- complexity scenario with 13 solutions distributed across 5 reasoning families. The solution lengths range from 4 to 10 steps. The abundance of alterna- tive paths and families in this example underscores the depth of the logical problems presented. These examples collectively demonstrate the quality and depth of our dataset. By capturing a wide range of reasoning complexities—from sim- ple, direct derivations to highly branched logical structures—and providing granular annotations, the dataset offers a rigorous standard for evaluating the reasoning capabilities of Large Language Models. B Error Type Details B.1 Detailed Definition Table 7 shows detailed definitions and examples of the error taxonomy. B.2 Error Distribution Figure 11 illustrates the distribution of error types (semantic understanding and logical execution) in models, along with a detailed comparison across different error categories. C Case Study C.1 Divergent Metrics Reveal Hidden Reasoning Gaps. We present a representative LogicGraph instance with four ground-truth minimal proof paths orga- nized into three distinct reasoning families to qual- itatively analyze model behavior beyond aggregate metrics. As shown in Figure 6, all evaluated mod- els achieve perfect convergent performance on this Domain CategorySpecific Fields (Examples)# SamplesPercentage Business & FinanceQuality Control, Insurance, Industrial Engineering, etc.20723.0% Environment & ScienceScientific Method, Biodiversity, Forestry, etc.18720.8% Medical & HealthClinical Trials, Pharmacology, Emergency Medicine, etc.16718.6% Law & GovernanceRegulatory Compliance, Legal Procedure, Litigation, etc.11312.6% Engineering & TechIoT, Software Development, Telecommunications, etc.9410.4% Humanities & SocietySports, Visual Arts, Culinary Arts, etc.849.3% OtherGeneral Knowledge, Mixed Domains252.8% Transportation & UrbanSoil Science, Agriculture, Automotive, etc.232.6% Table 6: Domain Distribution of the LogicGraph Benchmark. The dataset covers a wide spectrum of real-world scenarios, categorized into 7 major domains and over 90 specific fields. This diversity ensures a comprehensive evaluation of reasoning capabilities across various professional and practical contexts. case, with Success Rate, Precision, and Shortest Path Finding Rate all reaching 100%. Under tra- ditional evaluation, these models would therefore appear indistinguishable. This case illustrates that current LLMs tend to conflate reformulation with exploration, highlighting the necessity of explicit divergent evaluation. However, divergent metrics reveal substantial differences in reasoning behavior. Gemini-3-Pro successfully identifies three out of four valid proof paths, covering all reasoning families (Diversity = 75%, Versatility = 100%). In contrast, o3, despite producing multiple solutions, repeatedly commits to the same dominant derivation, recovering only a single ground-truth path (Diversity = 25%, Versa- tility = 33%). This indicates early commitment to a high-probability reasoning route, with alternative valid paths remaining unexplored. A different failure mode is observed for Qwen3- 235B-A22B. While the model attempts to enumer- ate multiple solutions, only two out of six generated paths are logically valid, resulting in a sharp drop in precision. Step-level verification (C.2) shows that invalid solutions often rely on fabricated or insuffi- cient intermediate steps, reflecting result-oriented reasoning rather than structured exploration of the proof space. This highlights that generating more solutions does not necessarily correspond to im- proved divergent reasoning. Notably, the reasoning-oriented variant Qwen3- 235B-A22B-Thinking achieves full coverage of all ground-truth paths with perfect precision, demon- strating that explicit reasoning optimization can substantially improve both exploration breadth and logical faithfulness in small multi-path settings. Nevertheless, as shown in our large-scale results, such improvements do not fully eliminate the degra- dation of diversity under increased reasoning depth. Overall, this case study illustrates that con- vergent correctness can mask fundamentally dif- ferent reasoning strategies. Models may reach the correct conclusion while exhibiting pseudo- divergence—superficially diverse outputs that col- lapse to the same minimal support—or hallucinated exploration driven by result-oriented fabrication. These behaviors underscore the necessity of ex- plicit divergent evaluation for diagnosing genuine multi-path reasoning ability. C.2 Diagnosing Logical Fallacies Extending this analysis to Qwen3-235b-A22b, we observe that high success rates can mask subtle logical flaws in Figure 12. While the models ar- rive at the correct final answer, a granular inspec- tion of the reasoning chains reveals specific failure modes. Notably, our qualitative analysis identi- fies that the Thinking model frequently succumbs toinsufficient_premiseerrors—making unjustified logical leaps without establishing necessary inter- mediate lemmas. These findings underscore the ne- cessity of our multi-dimensional evaluation frame- work for detecting result-oriented fabrications in proof generation. C.3 Why Formal Verification Is Necessary for Evaluating Logical Reasoning To illustrate the limitations of current LLM-as- a-judge paradigms and to motivate our formal- verification-based evaluation, we provide a qual- itative analysis of three representative scenarios observed in thetest_11benchmark. These cases expose both (i) false negatives (rejecting valid but compressed reasoning) and (i) false positives (ac- cepting formally invalid steps) that frequently occur under direct LLM-based evaluation. Error TypeDetailed DescriptionConcrete Example A. Semantic Comprehension (Information Processing Layer) Semantic MisinterpretationThe model fails to correctly parse the linguistic meaning of a specific fact or rule. This often involves confusing the direction of causality or ignoring negations. Context:“If A, then B.” Model interpretation:“If B, then A.” (Conditional inversion) Context:“John is not eligible.” Model interpretation:“John is eligible.” (Negation neglect) Information OmissionThe model completely ignores a critical piece of evidence or a con- straint provided in the input con- text during the reasoning chain. Context:“John has no medical insurance.” Error:The model concludes John proceeds with a procedure requiring insurance, failing to retrieve the negation fact. Fact HallucinationThe model fabricates premises or assumes external knowledge that contradicts or is absent from the provided context. Context:“John visits the hospital.” Error:The model adds “John has cancer” as a premise for deduction, despite no such mention in the text. B. Logical Execution (Reasoning Layer) Invalid DeductionThe derivation step is logically fun- damentally flawed. Even if the premises are correct, the conclu- sion cannot be derived using stan- dard logic (e.g., formal fallacies). Premises:“Rule: If it rains, the ground is wet.” + “Fact: The ground is wet.” Conclusion:“Therefore, it is raining.” Reason:Fallacy of affirming the consequent. Rule MisapplicationThe model selects a rule that exists in the context but applies it to an entity or situation where the rule’s preconditions are not met. Context:“All doctors must be licensed. John is a driver.” Error:Applying the “doctor licensing” rule to John, claiming he must have a medical license. Insufficient PremiseThe model draws a definitive con- clusion based on a subset of premises that are necessary but not sufficient. It fails to aggregate all required conditions. Rule:“If A and B, then C.” Fact:“A is true.” (B is unknown/false). Error:Model concludes “C is true” solely based on A, ignoring the missing condition B. Table 7: Detailed definitions and examples of the error taxonomy. We provide concrete scenarios to illustrate the distinction between comprehension failures and execution failures. C.4 False Negatives on Compressed Logical Inference LLM-based evaluators often struggle when multi- ple logical operations are compressed into a single step, which can lead to false negatives. Figure 13 shows a solution produced by qwen3-235b-a22b- thinking. In Step 2, the model effectively applies a CD form, and the premises correspond to: (Rule 2)ResearchTeam∨MedicinalPlant (Rule 1)ResearchTeam→¬Infected (Step 1)MedicinalPlant→¬Infected Our verification pipeline (Deepseek-V3.2-Exp with Prover9) successfully proves the target and validates Step 2.However, when using Deepseek-V3.2-Expdirectly as an LLM judge (i.e., without formal proof checking), the same step is incorrectly flagged as invalid. This indicates that standard LLM evaluators may lack the robustness to assess logically correct but highly compressed inferences, inadvertently penalizing models that employ higher-efficiency reasoning patterns. C.5 False Positives and the Gap-Filling Bias of LLM Judges A more severe failure mode of LLM-as-a-judge is the tendency to over-credit incomplete derivations by implicitly supplying missing premises (i.e., “fill- ing in the gaps”). We compare twotest_11solu- tions to demonstrate this issue. Figure 14(a) presents a correct solution from qwen3-235b-a22b-thinking.In Step 2, the derivation explicitly cites the necessary bridge rule: (Rule 5)Operational∧Dispensers→Controlled, together with the required factual premises. All evaluation methods correctly identify this solution as valid. Figure 14(b) shows a flawed solution from qwq-32b. In Step 2, the model attempts to derive the same conclusion using only: (Step 1)Operational(Fact 2)Dispensers, while omitting Rule 5. Formally, without the impli- cation rule we have Operational∧Dispensers⊬Controlled, so the step is a non sequitur. Our formal verifier correctly rejects this step (False). In contrast, the other LLM-based eval- uators mark it as valid (True). This highlights a systematic bias: LLM judges tend to prioritize semantic plausibility over logical entailment, and may implicitly reconstruct missing rules from their own priors or context. As a result, conventional LLM-only evaluation can inflate scores for “nearly correct” but formally invalid proofs, making it unre- liable for measuring strict logical reasoning ability. D Prompt for Dataset Generation Figure 15 shows the prompt we used to infer a co- herent real-world domain from a set of abstract en- tities and instantiate logical formulas into Prover9 syntax. Below is the prompt we used to translate the instantiated Prover9 expressions into natural language to form the final dataset. E Prompt for Model Evaluation Figure 16 shows the prompt we used to test the Large Language Models (LLMs) on the multi-path reasoning task. F Prompt for Model Performance Evaluation We present the condensed prompts used in our eval- uation pipeline. Dynamic content injected at run- time is denoted by brackets (e.g., CONTEXT). Figure 17 shows the prompt we used by the eval- uator agent to parse the LLM’s raw response into structured JSON for automated verification. G Details of human annotators For data qualitative evaluation, we engaged four graduate students (including both PhD and Mas- ter’s students) from engineering disciplines who are also co-authors of this paper. All annotators pos- sessed strong backgrounds in formal logic and crit- ical reasoning, making them well-qualified for this task. Since the annotators were co-authors actively involved in the research, no formal recruitment pro- cess or compensation was required, and they were fully aware of how the data would be used in the study. The annotation process focused solely on logical validity and natural language quality eval- uation and did not involve collecting any personal identifying information or expose annotators to any risks. As this research involved co-authors analyz- ing academic content rather than external human subjects, it was determined to be exempt from for- mal ethics review board approval. The annotation work was conducted as part of regular academic research activities within our institution. No pro- tected or sensitive demographic information was collected or used in this research. H Details of Ai Assistants In Research Or Writing Artificial Intelligence tools were utilized in two distinct capacities during this research: Dataset Generation.To construct the multi- solution logic benchmark, we utilized LLMs (specifically DeepSeek-V3 via API) to translate symbolic logic templates into natural language nar- ratives. This process involved converting formal logical rules (e.g., implications, disjunctions) into coherent scenarios across various domains such as cybersecurity, law, and medical diagnosis. The generated text was subsequently verified by human annotators to ensure clarity and fidelity to the un- derlying logic. Research and Writing Assistance.We utilized GitHub Copilot (powered by Gemini 3 Pro) as a coding assistant to help develop the evaluation scripts and analyze the experimental data. Addi- tionally, AI assistance I Details of Computational Experiment Our computational experiments evaluated a diverse set of Large Language Models (LLMs) for logical reasoning, covering both proprietary API-based systems and open-weight releases. Models Evaluated.We evaluated proprietary models accessed via APIs, including GLM-4.6, GPT-5.1, Claude-Sonnet-4.5, o3/o4-mini, and Gemini 2.5-Flash, Gemini-2.5-Pro, Gemini-3-Pro- Preview,. We also evaluated open-weight models, including GPT-OSS-120B, Qwen3-235B-A22B (and its Thinking variant) (Team, 2025a), QwQ- 32B (Team, 2025b), and DeepSeek-V3.2-Exp (and its Thinking variant) (DeepSeek-AI, 2025). For all models, we adopted a unified prompting protocol that encourages the model to produce as many in- dependent and verifiable solution paths as possible under a fixed structured answer template; prompt templates are provided in Appendix E. Deployment and Access.All proprietary models were queried through their official APIs. Among the open-weight models, only QwQ-32B was de- ployed locally for inference; it was tested on a machine equipped with two NVIDIA A100 GPUs. All other models were accessed via APIs. Evaluation Framework.We implemented an au- tomated evaluation pipeline to assess model out- puts. In particular, we performed formal verifica- tion using the automated theorem proverProver9 to check the logical validity of the generated deriva- tions. Only logically valid steps, as verified by Prover9, were counted toward the final evaluation metrics. "Fact1: The research team has advanced sensor equipment", "Fact2: The research team does not violate ethical guidelines protocol", "Fact3: The research team does not request assistance from consultants" "Proof Goal": "The research team completes the study on drought-resistant wheat" Family 1: •Solution 1 (2 steps): Step 1 (Rule: MP): Premises: - Rule3: (has_equipment(ResearchTeam, AdvancedSensors) -> (completes_fieldwork(ResearchTeam, SpringSeason) -> completes_study(ResearchTeam, DroughtResistantWheat))) Natural: Provided that the research team has advanced sensor equipment, then if they complete fieldwork during the spring season, they will complete the study on drought-resistant wheat - Fact1: has_equipment(ResearchTeam, AdvancedSensors) Natural: The research team has advanced sensor equipment Step1_Conlusion: The research team completes the study on drought-resistant wheat if they complete fieldwork during the spring season Step 2 (Rule: DE): Premises: - Rule10: (completes_fieldwork(ResearchTeam, SpringSeason) | completes_fieldwork(ResearchTeam, SummerSeason)) Natural: The research team completes fieldwork during the spring season or they complete fieldwork during the summer season - Derived: (completes_fieldwork(ResearchTeam, SpringSeason) -> completes_study(ResearchTeam, DroughtResistantWheat)) Natural: The research team completes the study on drought-resistant wheat if they complete fieldwork during the spring season - Rule11: (completes_fieldwork(ResearchTeam, SummerSeason) -> completes_study(ResearchTeam, DroughtResistantWheat)) Natural: Should the research team complete fieldwork during the summer season, then they complete the study on drought-resistant wheat Step2_Conlusion: The research team completes the study on drought-resistant wheat Family 2: •Solution 2 (5 steps): Step 1: RAA + [Rule14, Rule15] => Derived1 Step 2: HS + [Derived1, Rule9] => Derived2 Step 3: DE + [Rule8, Rule7, Derived2] => Derived3 Step 4: RAA + [Rule13, Derived3] => Derived4 Step 5: DE + [Rule2, Rule1, Derived4] => G •Solution 3 (4 steps): Step 1: HS + [Rule12, Rule5] => Derived1 Step 2: MT + [Derived1, Fact3] => Derived2 Step 3: HS + [Rule6, Derived2] => Derived3 Step 4: DE + [Rule2, Rule1, Derived3] => G "Rule1: If the research team receives government grant funding, then they complete the study on drought- resistant wheat", "Rule2: The research team receives government grant funding or they receive private grant funding", "Rule3: Provided that the research team has advanced sensor equipment, then if they complete fieldwork during the spring season, they will complete the study on drought-resistant wheat", "Rule4: If the research team follows ethical guidelines protocol, then they do not publish preliminary findings", "Rule5: Under the condition that the research team implements changes to their procedures, they request assistance from consultants", "Rule6: If the research team receives private grant funding, then they achieve the crop yield milestone", "Rule7: If the review board approves a project extension, then should the private grant funding not lead to study completion, the research team does not modify their research methodology", "Rule8: The review board either approves a project extension or denies a project extension", "Rule9: If the research team submits an appeal against the decision, then whenever private grant funding fails to lead to study completion, they do not modify their research methodology", "Rule10: The research team completes fieldwork during the spring season or they complete fieldwork during the summer season", "Rule11: Should the research team complete fieldwork during the summer season, then they complete the study on drought-resistant wheat", "Rule12: Provided that achieving the crop yield milestone does not result in study completion, the research team implements changes to their procedures", "Rule13: When private grant funding does not trigger study completion, the research team modifies their research methodology", "Rule14: Under the condition that denying a project extension does not cause the research team to submit an appeal, they accept the ruling on their case", "Rule15: Should denying a project extension not result in the research team submitting an appeal, then they do not accept the ruling on their case", "Rule16: If the research team does not follow ethical guidelines protocol, then they violate ethical guidelines protocol", "Rule17: The research team publishes preliminary findings if they do not complete the study on drought- resistant wheat" Family 3: •Solution 4 (3 steps): Step 1: MT + [Rule16, Fact2] => Derived1; Step 2: MP + [Rule4, Derived1] => Derived2; Step 3: MT + [Rule17, Step2] => G Figure 8: A Small type example in LogicGraph. "Rule1: Either the EPA has approved research funding for the climate study or the EPA has approved research funding for the biodiversity survey.", "Rule2: If samples have been processed in the Arctic region, then preliminary data has been analyzed in the Arctic region.", ... "Rule41: If environmental protection goals have not been met by the EPA, then regulation compliance has been met by the EPA.", "Rule42: If environmental protection goals have not been met by the EPA, then regular audits have been conducted by the EPA." "Fact1: The contingency plan has been activated by the EPA.", ... "Fact11: Project milestones have not been achieved by the EPA." "Proof Goal": "Environmental protection goals have been met by the EPA." Family 2: •Solution 2 (7 steps): Step 1: RAA + [Rule36, Rule37] => Derived1 Step 2: RAA + [Rule30, Derived1] => Derived2 Step 3: DS + [Derived2, Fact6] => Derived3 Step 4: HS + [Derived3, Rule2] => Derived4 Step 5: HS + [Rule28, Derived4] => Derived5 Step 6: RAA + [Derived5, Rule29] => Derived6 Step 7: DS + [Derived6, Fact5] => G Family 3: •Solution 4 (7 steps): Step 1: MT + [Rule33, Fact8] => Derived1 Step 2: HS + [Derived1, Rule9] => Derived2 Step 3: HS + [Derived2, Rule8] => Derived3 Step 4: HS + [Rule39, Derived3] => Derived4 Step 5: MT + [Derived4, Fact7] => Derived5 Step 6: MP + [Rule7, Derived5] => Derived6 Step 7: MP + [Rule6, Derived6] => G Family 4: •Solution 3 (5 steps): Step 1: RAA + [Rule31, Rule32] => Derived1 Step 2: HS + [Rule42, Derived1] => Derived2 Step 3: HS + [Derived2, Rule4] => Derived3 Step 4: HS + [Derived3, Rule3] => Derived4 Step 5: RAA + [Rule41, Derived4] => G Family 1: •Solution 1 (7 steps): Step 1: HS + [Rule26, Rule27] => Derived1 Step 2: MP + [Derived1, Fact4] => Derived2 Step 3: RAA + [Derived2, Rule35] => Derived3 Step 4: DE + [Derived3, Rule24, Rule25] => Derived4 Step 5: MP + [Rule20, Derived4] => Derived5 Step 6: HS + [Derived5, Rule11] => Derived6 Step 7: DE + [Rule1, Derived6, Rule5] => G •Solution 5 (5 steps): Step 1: MP + [Rule14, Fact1] => Derived1 Step 2: MP + [Rule13, Derived1] => Derived2 Step 3: DS + [Rule12, Derived2] => Derived3 Step 4: MP + [Rule10, Derived3] => Derived4 Step 5: DE + [Rule1, Derived4, Rule5] => G •Solution 6 (8 steps): Step 1: MP + [Rule19, Fact2] => Derived1 Step 2: DE + [Rule18, Rule17, Derived1] => Derived2 Step 3: RAA + [Rule15, Derived2] => Derived3 Step 4: DS + [Rule16, Derived3] => Derived4 Step 5: RAA + [Rule40, Derived4] => Derived5 Step 6: MP + [Rule20, Derived5] => Derived6 Step 7: HS + [Derived6, Rule11] => Derived7 Step 8: DE + [Rule1, Derived7, Rule5] => G •Solution 7 (13 steps): Step 1: MT + [Rule22, Fact11] => Derived1 Step 2: DS + [Rule23, Derived1] => Derived2 Step 3: RAA + [Rule38, Derived2] => Derived3 Step 4: RAA + [Rule34, Derived3] => Derived4 Step 5: MP + [Derived4, Fact3] => Derived5 Step 6: DS + [Derived5, Fact10] => Derived6 Step 7: DS + [Rule21, Derived6] => Derived7 Step 8: MT + [Derived7, Fact9] => Derived8 Step 9: RAA + [Derived8, Rule35] => Derived9 Step 10: DE + [Derived9, Rule24, Rule25] => Derived10 Step 11: MP + [Rule20, Derived10] => Derived11 Step 12: HS + [Derived11, Rule11] => Derived12 Step 13: DE + [Rule1, Derived12, Rule5] => G Figure 9: A Medium type example in LogicGraph. "Rule1: Either the stream is live or the tournament is successful.", "Rule2: Provided that the match needs an update, the schedule is finalized or it is not approved.", ... "Rule60: If the event is not scheduled, then the event is cancelled.", "Rule61: Provided that the tournament is not successful, the platform does not have a backup." "Fact1: The team has transport.", ... "Fact13: It is not the case that the schedule is finalized." "Proof Goal": "The tournament is successful." Family 2: •Solution 2 (4 steps): Step 1: DE + [Rule3, Rule2, Rule4] => Derived1 Step 2: DS + [Derived1, Fact13] => Derived2 Step 3: DS + [Rule44, Derived2] => Derived3 Step 4: DS + [Rule43, Derived3] => G •Solution 6 (6 steps): Step 1: RAA + [Rule48, Rule49] => Derived1 Step 2: CD + [Rule22, Rule23, Derived1] => Derived2 Step 3: DS + [Derived2, Fact8] => Derived3 Step 4: DS + [Derived3, Fact13] => Derived4 Step 5: DS + [Rule44, Derived4] => Derived5 Step 6: DS + [Rule43, Derived5] => G Family 1: •Solution 1 (5 steps): Step 1: MP + [Rule40, Fact3] => Derived1 Step 2: MP + [Derived1, Fact2] => Derived2 Step 3: DE + [Rule21, Rule20, Derived2] => Derived3 Step 4: DS + [Derived3, Fact5] => Derived4 Step 5: DS + [Rule1, Derived4] => G Family 3: •Solution 5 (5 steps): Step 1: RAA + [Rule55, Rule56] => Derived1 Step 2: MT + [Derived1, Fact7] => Derived2 Step 3: HS + [Rule19, Derived2] => Derived3 Step 4: HS + [Rule18, Derived3] => Derived4 Step 5: DE + [Rule17, Rule16, Derived4] => G •Solution 11 (8 steps): Step 1: DS + [Rule37, Fact11] => Derived1 Step 2: HS + [Rule51, Derived1] => Derived2 Step 3: RAA + [Rule50, Derived2] => Derived3 Step 4: DE + [Derived3, Rule35, Rule36] => Derived4 Step 5: RAA + [Rule47, Derived4] => Derived5 Step 6: HS + [Rule19, Derived5] => Derived6 Step 7: HS + [Rule18, Derived6] => Derived7 Step 8: DE + [Rule17, Rule16, Derived7] => G •Solution 12 (6 steps): Step 1: RAA + [Rule57, Rule58] => Derived1 Step 2: RAA + [Derived1, Rule52] => Derived2 Step 3: RAA + [Rule38, Derived2] => Derived3 Step 4: DS + [Rule39, Derived3] => Derived4 Step 5: HS + [Rule18, Derived4] => Derived5 Step 6: DE + [Rule17, Rule16, Derived5] => G •Solution 13 (4 steps): Step 1: DS + [Rule42, Fact12] => Derived1 Step 2: MP + [Rule41, Derived1] => Derived2 Step 3: HS + [Rule18, Derived2] => Derived3 Step 4: DE + [Rule17, Rule16, Derived3] => G Family 5: •Solution 3 (7 steps): Step 1: MT + [Rule10, Fact4] => Derived1 Step 2: MT + [Rule9, Derived1] => Derived2 Step 3: MT + [Rule7, Derived2] => Derived3 Step 4: DS + [Rule8, Derived3] => Derived4 Step 5: RAA + [Rule6, Derived4] => Derived5 Step 6: MT + [Rule60, Derived5] => Derived6 Step 7: MP + [Rule5, Derived6] => G •Solution 7 (8 steps): Step 1: HS + [Rule11, Rule24] => Derived1 Step 2: MT + [Derived1, Fact9] => Derived2 Step 3: MT + [Rule9, Derived2] => Derived3 Step 4: MT + [Rule7, Derived3] => Derived4 Step 5: DS + [Rule8, Derived4] => Derived5 Step 6: RAA + [Rule6, Derived5] => Derived6 Step 7: MT + [Rule60, Derived6] => Derived7 Step 8: MP + [Rule5, Derived7] => G Family 4: •Solution 4 (6 steps): Step 1: MP + [Rule15, Fact1] => Derived1 Step 2: DS + [Rule14, Derived1] => Derived2 Step 3: MT + [Rule45, Derived2] => Derived3 Step 4: DS + [Derived3, Fact6] => Derived4 Step 5: RAA + [Rule59, Derived4] => Derived5 Step 6: RAA + [Derived5, Rule61] => G •Solution 8 (4 steps): Step 1: DE + [Rule27, Rule26, Rule28] => Derived1 Step 2: DS + [Rule25, Derived1] => Derived2 Step 3: RAA + [Rule59, Derived2] => Derived3 Step 4: RAA + [Derived3, Rule61] => G •Solution 9 (10 steps): Step 1: RAA + [Rule53, Rule54] => Derived1 Step 2: HS + [Derived1, Rule30] => Derived2 Step 3: RAA + [Rule46, Derived2] => Derived3 Step 4: HS + [Derived3, Rule29] => Derived4 Step 5: RAA + [Derived4, Rule13] => Derived5 Step 6: DS + [Rule14, Derived5] => Derived6 Step 7: MT + [Rule45, Derived6] => Derived7 Step 8: DS + [Derived7, Fact6] => Derived8 Step 9: RAA + [Rule59, Derived8] => Derived9 Step 10: RAA + [Derived9, Rule61] => G •Solution 10 (9 steps): Step 1: CD + [Rule32, Rule34, Rule33] => Derived1 Step 2: DS + [Derived1, Fact10] => Derived2 Step 3: DS + [Rule31, Derived2] => Derived3 Step 4: MT + [Rule12, Derived3] => Derived4 Step 5: DS + [Rule14, Derived4] => Derived5 Step 6: MT + [Rule45, Derived5] => Derived6 Step 7: DS + [Derived6, Fact6] => Derived7 Step 8: RAA + [Rule59, Derived7] => Derived8 Step 9: RAA + [Derived8, Rule61] => G Figure 10: A Large type example in LogicGraph. 0500100015002000 gemini-3-pro-preview qwen3-235b-a22b-T Deepseek-V3.2-Exp-T gemini-2.5-pro gemini-2.5-flash Deepseek-V3.2-Exp o4-mini o3 kimi-k2-T claude-sonnet-4-5-T claude-sonnet-4-5 qwq-32b qwen3-235b-a22b gpt-5.1 gpt-oss-120b glm-4.6 Semantic Comprehension Errors (Count) Error Type Semantic Misinterpretation Information Omission Fact Hallucination 050010001500200025003000 Logical Execution Errors (Count) Error Type Invalid Deduction Rule Misapplication Insufficient Premise Figure 11: Error distribution across models, grouped by semantic comprehension and logical execution. Solution 3: Step 1: [Rule10] => The research team completes fieldwork during the spring season or they complete fieldwork during the summer season (Used: [Rule10]) Step 2: [Rule11, Step1] => The research team completes the study on drought-resistant wheat (Used: [Rule11, Step1]) Step 1Step 2 ✅ ❌ Evaluation Result: Error Type: insufficient_premise. Error Analysis: The reasoning step attempts to deduce 'The research team completes the study on drought-resistant wheat' using Rule11 and Step1. However, the premises cited are insufficient to support this conclusion. Rule11 (in Prover9) states: 'completes_fieldwork(ResearchTeam, SummerSeason) -> completes_study(ResearchTeam, DroughtResistantWheat)'. To apply this rule, we need the antecedent 'completes_fieldwork(ResearchTeam, SummerSeason)' to be true. Step1 is not provided in the context, but even if Step1 established some fact, it does not appear to provide 'completes_fieldwork(ResearchTeam, SummerSeason)'. Without this necessary premise, the conclusion cannot be logically derived from the cited rule alone. Proof ❌ Model Response: Figure 12: A specific example of our model’s error analysis. Test 11 qwen3-235b-a22b-thinking-2507 solution2: Step 1: Fact1, Rule3 => If the medicinal plant is blooming during spring season, then the deer population is not infected with Chronic Wasting Disease (Used: Fact1, Rule3) Step 2: Rule2, Rule1, Step1 => The deer population is not infected with Chronic Wasting Disease (Used: Rule2, Rule1, Step1) Step 3: Step2, Rule6 => Chronic Wasting Disease is controlled in the deer population (Used: Step2, Rule6) Our (Deepseek-V3.2-Exp) Deepseek-V3.2-Thinking Gemini-3-Pro Deepseek-V3.2-Exp Step 1Step 2Proof True True True False ✅ ✅ ✅ True True True False ✅ ✅ ✅ Proof True True True False ✅ ✅ ✅ True True True ✅ ✅ ✅ True ❌ ❌ ✅ ❌ Figure 13: A valid complex reasoning step correctly verified by our formal method but incorrectly accepted by an LLM-based judge (using Deepseek-V3.2-Exp directly as an LLM judge). Our (Deepseek-V3.2-Exp) Deepseek-V3.2-Thinking Gemini-3-Pro Deepseek-V3.2-Exp Step 2Proof False True True True ✅ ❌ ❌ ❌ False True True True ✅ ❌ ❌ ❌ (b) Test 11 qwq-32b solution1: Step 1: [Fact3, Rule4] => Disease monitoring system becomes operational (Used: Fact3, Rule4) Step 2: [Step 1, Fact2] => Chronic Wasting Disease is controlled in the deer population (Used: Step 1, Fact2) (a) Test 11 qwen3-235b-a22b-thinking-2507 solution1: Step 1: Fact3, Rule4 => Disease monitoring system is operational in the protected region (Used: Fact3, Rule4) Step 2: Step1, Fact2, Rule5 => Chronic Wasting Disease is controlled in the deer population (Used: Step1, Fact2, Rule5) Our (Deepseek-V3.2-Exp) Deepseek-V3.2-Thinking Gemini-3-Pro Deepseek-V3.2-Exp Step 1Step 2Proof True True True True ✅ ✅ ✅ ✅ True True True True ✅ ✅ ✅ ✅ Step 1 True True True True ✅ ✅ ✅ ✅ True True True True ✅ ✅ ✅ ✅ Figure 14: Comparison of evaluation robustness. (a) A fully valid solution. (b) An invalid solution with missing premises (Rule 5), correctly rejected by our method but incorrectly accepted by LLM judges. System Role: You are a creative assistant. Your task is to infer a coherent real-world domain and instantiate the provided logical formulas strictly in Prover9 syntax. User Prompt: Step 1: Infer a Domain Consider this list of abstract seed entities: "Person", "Animal", "Plant", "Food", "Alcohol", "Disease", "Drug", "Natural Phenomenon", "Condition", "Material", "Substance", "Furniture", "Publication", "Organization", "Authorization", "Facility", "Natural Place", "Event", "Show", "Artwork", "Job", "Game", "Vehicle", "Tool", "Technology", "Electronic Device", "Platform", "Financial Product", "Skill", "Legislation", “Region", "Time Period". Infer a single real-world scenario that connects them (e.g., Scientific Research, Medieval Politics, Pharmaceutical Manufacturing). Step 2: Instantiate Logical Nodes (Prover9 only) Using the inferred domain, instantiate each logical node below. All entities and relations must belong to the SAME coherent story. Do not produce natural language descriptions in this step. logical_nodes_list Instructions: 1. Atomic Fact Definition (Prover9 only) - For every atomic symbol (A1, A2, ...), define a fact using `predicate(entity1, entity2, ...)`. - Keep entity names consistent across all expressions. 2. Expression Instantiation (Prover9 only) - For each formula provided, instantiate it using the atomic facts you created. - Preserve the original logical structure exactly (operators &, |, ->, -, <->). 3. Strict Output Format (Markdown) Domain Theme: [Single coherent domain] Entity Instantiation & Atomic Facts (Prover9) A1: predicate(entity1, entity2, ...) ... Expression Instantiation (Prover9) Expression 1: ( ... ) ... System Role: You are a precise translator. Your job is to convert Prover9 expressions into natural language without losing any logical information. User Prompt: Domain Theme: domain_theme Atomic Facts (Prover9 syntax): atomic_facts Composite Expressions (Prover9 syntax, maintain order): composite_expressions Translation Requirements: - Translate every atomic fact into a clear sentence. - Translate every composite expression in the SAME order as provided. - Preserve all entities, logical operators, and conditional structures exactly. - For implications, alternate conditional phrasing styles (e.g., 'If A, then B', 'Provided that A, B occurs', 'Whenever A happens, B follows', 'Under the condition that A, B follows). Do not reuse the exact same template for multiple implications. - For conjunctions, mention all conjuncts (e.g., 'Both A and B'). - For disjunctions, vary the connective wording (e.g., 'Either A or B', 'A happens or B happens'). - For negations, state the negation clearly (e.g., 'It is not the case that A', 'A does not hold'). - Do not add or remove entities. - Use varied but precise phrasing while preserving meaning. Strict Output Format (Markdown): Atomic Facts (Natural Language) A1: sentence ... Expression (Natural Language) Expression 1: sentence ... Figure 15: Prompt we use during the generation process. Given the following Facts and Rules as the assumptions and conditions of a logical scenario, your task is to find all distinct and valid proof paths that derive the conclusion 'question'. FACTS: facts RULES: rules IMPORTANT NOTATION: 1. Do NOT introduce external knowledge. 2. If NO valid proof path exists, state: "No valid proof path exists for the conclusion 'question' based on the given facts and rules. 3. Follow the following Strict Output Format: Solution [number]: Step 1: [Fact x, Rule y] => [intermediate_conclusion] (Used: [Fact x, Rule y]) Step 2: [Step 1, Fact z] => [Next_intermediate_conclusion] (Used: [Step 1, Fact z]) ... Step n: [Step m, Fact w] => [Final deduction] (Used: [Step m, Fact w]) ... Figure 16: Prompt we use during the test process. (a) Solution Extraction Prompt Task: Extract solution paths from the LLM response while preserving ALL original details and structure. Input: •Knowledge Base: RULES_AND_FACTS •Response: LLM_RESPONSE Critical Constraints: •Preserve all original text, reasoning details, and case-by-case analysis. •Do not simplify or summarize; keep original step numbering. •Normalize references (e.g., expand "Steps 1-3" to "Step 1, Step 2, Step 3"). Output Format: JSON object containing a list of solutions, where each solution includes: •id: Unique identifier. •steps: List of strings, each containing the full original text of a step. •conclusion: The final conclusion statement. (b) Natural Natural Language to Symbolic Expression Conversion Prompt Task: Convert the given logical reasoning step into valid Prover9 format. Input: •Step Text: STEP_TEXT •Available Premises: PREMISES_LIST (Facts, Rules, and verified conclusions from previous steps) •Context: TRANSLATION_MAPPINGS Instructions: •Identify premises explicitly used in the step text. •Assumptions Block: Include ONLY the needed premises from the Available Premises list. •Constraint: When referencing previous steps, use the EXACT Prover9 expression provided, without modification. •Goals Block: Include only the conclusion derived in this specific step. •Special Handling: For proof by contradiction, place the positive conclusion in the goals section and do not include the negated assumption in assumptions. Output: A valid Prover9 block containing formulas(assumptions). ... end_of_list. and formulas(goals). ... end_of_list. (c) Error Analysis Prompt Task: Classify the logical error in a failed step using two independent dimensions. Input: Context: STEP_TEXT, KNOWLEDGE_BASE, PROVER9_INPUT/OUTPUT Classification Framework: Dimension A: Input Processing (Optional) A1. Semantic Misinterpretation: Model misunderstood the meaning of facts/rules (e.g., reversed conditions). A2. Information Omission: Model ignored critical given facts/rules. A3. Fact Hallucination: Model used facts not provided in the input. Dimension B: Reasoning Process (Mandatory) B1. Invalid Deduction: Logically invalid inference (e.g., affirming the consequent). B2. Rule Misapplication: Rule exists but conditions are not satisfied. B3. Insufficient Premise: Cited premises are incomplete to support the conclusion. Output Format: JSON object containing: dimension_a: "has_error": bool, "error_type": "A1"|"A2"|"A3"|null dimension_b: "error_type": "B1"|"B2"|"B3" evidence: Specific quotes or reasoning supporting the classification. Figure 17: Prompt template we use during the performance evaluation process.

Instant research discovery