PaperlayerView exact revision on arXiv

Source-linked AI summary

LLMEval-Logic: A Solver-Verified Chinese Benchmark for Logical Reasoning of LLMs with Adversarial Hardening

Ming Zhang, Qiyuan Peng, Yinxi Wei, Yujiong Shen, Kexin Tan, Yuhui Wang, Zhenghao Xiang, Junjie Ye, Zhangyue Yin, Zhiheng Xi, Shihan Dou, Tao Gui, Maxm Pan, Ruizhi Yang, Qi Zhang, Xuanjing Huang

arXiv:2605.19597v1cs.CL

TL;DR

Existing logical-reasoning benchmarks can be templated, weakly audited, and quickly saturated, motivating more reliable evaluation of LLM reasoning from natural language. LLMEval-Logic builds a Chinese benchmark from realistic scenarios with expert and Z3 auditing, local rubrics, and adversarial hardening. Across 14 frontier LLMs, the strongest Hard Item Accuracy is 37.5%, while the best fixed-symbol joint Z3+Rubric score is 60.16%.

  • Problem

    Existing logical-reasoning benchmarks often use templated items, limited formal annotations, or insufficient difficulty, weakening evaluation of premise-grounded LLM reasoning.

  • Method

    LLMEval-Logic combines forward authoring from realistic Chinese scenarios with expert review, layered normalization, Z3 verification, expert rubrics, and adversarial hardening.

  • Results

    37.5% Hard Item Accuracy is the strongest reported score, while 60.16% is the best non-gold fixed-symbol joint Z3+Rubric formalization score.

  • Takeaways & Limitations

    Base accuracy, Hard accuracy, and formalization faithfulness capture distinct aspects of frontier logical reasoning.

  • Takeaways & Limitations

    The benchmark currently focuses on Chinese items and propositional or first-order logic, while Z3 alone cannot certify full natural-language/formalization equivalence.

Abstract

from arXiv · show

Evaluating large language models (LLMs) on natural-language logical reasoning is essential because rule-governed tasks require conclusions to follow strictly from stated premises. Many existing logical-reasoning benchmarks are generated by templating natural-language items from sampled formulas, provide only coarse or unaudited formal annotations, and are now quickly saturated by frontier reasoning models. We present LLMEval-Logic, a Chinese logical reasoning benchmark built from realistic situational scenarios. Its pipeline forward-authors and expert-audits natural-language items together with their reference formalizations, verifies annotated answers with Z3, constructs expert rubrics for natural-to-formal grading, and hardens selected items through a closed-loop adversarial workflow. The benchmark is released in two paired subsets: a 246-item Base subset shipped with 1,400 expert-developed rubric atoms, and a 190-item Hard subset with 938 multi-step sub-questions over closed model spaces. Evaluating 14 frontier LLMs on LLMEval-Logic reveals substantial gaps in current models: the best model reaches only 37.5% Hard Item Accuracy, and even with reference symbols the highest joint Z3+Rubric formalization score among evaluated models reaches only 60.16%. Our benchmark is publicly available at https://github.com/llmeval/LLMEval-Logic.

1. Introduction

LLMEval-Logic addresses realism, auditable natural-to-formal translation, and discriminative difficulty in logical-reasoning benchmarks through an audited Chinese benchmark with paired Base and Hard subsets.

  • Rule-governed applications require conclusions to follow strictly from stated premises, making reliable logical-reasoning benchmarks important for trustworthy LLM deployment.
  • Existing benchmarks often reverse-generate language from formulas, producing template-like artifacts that can permit surface-based answer prediction.
  • Natural-to-formal evaluation remains difficult because many human-written narratives provide limited annotations and no rubric for checking local logical relations, constraints, and query alignment.
  • Published benchmark splits can saturate under modern reasoning models, clustering near ceiling accuracy and offering little failure localization.
  • LLMEval-Logic forward-authors realistic Chinese scenarios, expert-audits formalizations, applies layered normalization, verifies answers with Z3, and constructs expert rubrics.
  • The benchmark releases paired Base and Hard subsets, combining audited single-question reasoning and natural-to-formal evaluation with multi-question adversarial reasoning.

2. Design

The benchmark uses sequential human and solver audits for Base items, then routes validated items through adversarial hardening to create Hard, with answer and formalization metrics evaluated separately.

  • Dataset Construction: Base construction proceeds through forward authoring, expert review, layered normalization, Z3 verification, and rubric construction.
  • Dataset Construction: The dataset begins with 521 human-seeded Chinese items embedding formalizable logic in naturalistic rules, schedules, eligibility, and institutional procedures.
  • Formal Verification: Z3 checks whether formalized premises and queries certify labelled answers while surfacing missing or redundant premises, type mismatches, and inconsistent mappings.
  • Formalization Grading: Rubrics audit local natural-language-to-formal faithfulness across logical relations, stated constraints, and query alignment.
  • Hardening: Hard contains 190 items and 938 sub-questions, averaging 4.94 sub-questions per item across a range of 2–8.
  • Evaluation: Answer evaluation reports Base Item Accuracy and Hard Item/Sub-Question Accuracy, while formalization evaluation combines Z3 execution with rubric atom matching under free- and fixed-symbol settings.

3. Experiment and Analysis

The experiments test shortcut resistance, formalization faithfulness, and discriminative headroom across frontier models, finding sharp Hard degradation and persistent natural-to-formal translation gaps.

  • Research Questions: The study evaluates whether forward-authored items resist shortcuts, whether models faithfully formalize language, and whether Hard provides discriminative headroom.
  • Experimental Protocol: Fourteen frontier LLMs from seven families are tested in thinking and no-thinking configurations across three independent runs.
  • RQ1: Shortcut Resistance: 65.1% Base Item Accuracy falls to 22.9% on Hard, a 42.2-point drop; the strongest Hard score is 37.5 ± 3.8%.
  • RQ2: Formalization Faithfulness: Joint Z3+Rubric scores are lower than either individual signal for every evaluated model in both free-symbol and fixed-symbol settings.
  • RQ2: Formalization Faithfulness: Providing reference symbols raises GPT-5.4 Pro without thinking from 32.93% to 60.16% Z3+Rubric, yet 60.16% remains the best non-gold fixed-symbol score.

Z3 Rubric Both Z3 Rubric Both

The benchmark compares Z3, Rubric, and joint formalization signals alongside Base–Hard accuracy patterns. Fixed symbols improve formalization, while Hard evaluation changes rankings and exposes failures in chained closed-space reasoning.

  • Formalization metrics: Z3 and Rubric provide distinct formalization signals whose joint agreement is stricter than either signal alone.The formalization table defines Z3 as solver execution, Rubric as atom-level pass rate, and Both as agreement between them.
  • Base versus Hard: Hard evaluation widens performance gaps across model families relative to Base on complex closed candidate spaces.The Hard setting requires maintaining the full candidate space across related queries.
  • Ranking divergence: Base and Hard rankings diverge: Seed 2.0 Pro and Hy3 preview lead Base at 75.5% and 75.3% but fall near the bottom on Hard at 20.4% and 21.6%.Claude Opus 4.6 rises from the lowest Base rank to Hard rank 2, while thinking-variant rankings show 𝜌= −0.61.
  • Chained reasoning: The 25–43-point Sub-Q→Item gaps show that models often solve individual sub-questions but fail the all-subquestions-correct item criterion.Hard failures involve counterfactual recomputation, uncertainty enumeration, projection levels, provenance, and validity-tier boundaries.
  • Visual diagnostics: Most Figure 5 points lie below y= x, while fixed symbols shift model results up-right without reaching the 72.36% Rubric ceiling or the 100% gold reference.Figure 6 reports thinking 𝜌= −0.61 and no/low-thinking 𝜌= +0.79 for Base–Hard ranking association.

4. Related Work

Prior benchmarks advanced natural-language logical reasoning evaluation but retain limitations in construction realism and formalization auditing. LLMEval-Logic combines forward-authored Chinese scenarios, rubric-graded formalizations, and controlled hardening.

  • Logic benchmarks: Many existing benchmarks generate items from symbolic rule worlds, while FOLIO adds human-written narratives with FOL annotations.Formula-derived construction can leave template-like artifacts, and final-answer scoring cannot audit semantic preservation in formalization.
  • NL-to-FL evaluation: Natural-to-formal evaluation methods often rely on answer or execution signals that cannot localize which source-semantic component a candidate formalization mis-encodes.LLMEval-Logic scores logical-relation, stated-constraint, and query-alignment rubric atoms.
  • Benchmark design: LLMEval-Logic combines rubric-graded formalization evaluation with controlled hardening of closed candidate spaces.The resulting items are designed to remain human-interpretable, solver-executable, and discriminative for frontier LLMs.

5. Conclusion

LLMEval-Logic pairs solver-verified Base items with adversarially hardened Hard items and evaluates both answer accuracy and formalization faithfulness. Its results show that these signals expose distinct weaknesses in frontier logical reasoning.

  • Conclusion: Across 14 frontier LLMs, the strongest Hard score is only 37.5% Hard Item Accuracy, while no-thinking collapse is family-specific and Base–Hard rankings diverge.The conclusion also reports that Z3 correctness can overestimate rubric faithfulness.
  • Conclusion: Forward authoring, Z3/rubric auditing, and controlled hardening provide the benchmark’s quality-control and discrimination foundation.The benchmark, workflow, and audit traces are slated for release upon publication.
  • Conclusion: Base accuracy, Hard accuracy, and formalization faithfulness capture distinct aspects of frontier logical reasoning.

Limitations

The paper’s audited workflow uses normalization, gated adversarial hardening, and solver verification, but the benchmark remains bounded by language, logic-coverage, and formalization-equivalence limitations.

  • Scope limitations: LLMEval-Logic currently focuses on Chinese natural-language items, so generalization to other languages and writing conventions remains empirically unvalidated.The underlying formalizations are described as languageagnostic.
  • Scope limitations: The benchmark covers propositional and first-order logic, leaving higher-order, modal, temporal, and probabilistic reasoning for future extensions.
  • Verification limitations: Z3 certifies that the labelled answer follows from the normalized reference formalization but cannot alone certify full equivalence with the natural-language item.Expert rubrics mitigate this gap, though their construction requires annotation effort and may retain fine-grained blind spots.
  • Adversarial hardening: The hardening workflow admits only items that pass Review and Verification gates, with failures looping back for revision or answer repair.The workflow uses Decider, Proposal, Review, Answering, Verification, and finalization stages.
  • Adversarial hardening: Hardening must alter the closed candidate space, required operation, or reasoning path rather than merely rewording surface text.The six structural strategies include branching and distractor premises among other operations.

B.3. Quality Control Statistics

The hardening workflow required repeated proposal, review, verification, and answer-repair cycles, with only completed items contributing to gate statistics.

  • 224 of 254 items completed the hardening workflow, an 88.2% completion rate; 30 exhausted the retry budget before a passing revision.Final manual curation removed additional ambiguous or redundant items before release.
  • 89.3% of items triggered at least one proposer retry, averaging 4.0 retries.
  • 80.8% triggered the Review →Proposer loop, indicating that review rejected a substantial share of proposals.
  • 58.0% were returned by Verification after passing Review, exposing flaws that appeared only in model-answering traces.
  • 58.9% required at least one answer repair, showing that answer generation remained iterative after item design passed review.

C. Evaluation Detail

Evaluation separates answer judging from natural-to-formal evaluation, using solver execution and rubric checks under free- and fixed-symbol settings.

  • Models produce structured JSON answers, which an LLM judge compares with reference answers for semantic equivalence.
  • Translation evaluation begins with Formal Language JSON and compares Free-FL, where models define symbols, with Fixed-FL, where gold declarations are read-only context.
  • Z3 mode executes candidate premises and queries, then compares solver-derived answers with gold references through semantic judging.
  • Rubric free-FL mode scores logical_relation, stated_constraint, and query_alignment checklist atoms directly against candidate premises and queries.
  • Rubric fixed-FL mode adds a Z3 premise-equivalence gate and soft-review of premise differences when solved answers still match.

D. LLM-as-Judge Validation

The evaluation uses LLM judges for leaderboard and rubric verdicts, then tests their stability on independently sampled answer and rubric cases.

  • gpt-5.1-chat produces both leaderboard verdicts and formalization-side Z3, Rubric, and Both scores.
  • The validation samples 103 Hard sub-questions and 105 LLM-decided rubric atoms, rejudged by gpt-5.1-chat, Claude Opus 4.6, and Gemini 3.1 Pro.
  • All six pairwise Cohen’s κ values fall between 0.873 and 0.922, within the almost-perfect agreement band.
  • Observed pairwise agreement is at least 94%, with unanimous verdicts for 93.2% of sub-questions and 93.3% of rubric atoms.
  • The agreement study cannot exclude family-correlated blind spots, and rubric agreement covers only atoms delegated to the LLM rather than the full hybrid pipeline.

E. Why Z3 and Rubric Disagree

Z3 and Rubric measure complementary aspects of formalization: solver answers can overlook semantic divergences, while positive-only rubrics can overlook unlisted errors.

  • E. Why Z3 and Rubric Disagree: Section E. Why Z3 and Rubric Disagree: Free Z3 accuracy systematically exceeds Free Rubric accuracy, while the best Fixed-symbols Rubric reaches 72.36% versus 100% for gold.
  • E. Why Z3 and Rubric Disagree: Section E. Why Z3 and Rubric Disagree: Z3 can accept a wrong formalization when low-cardinality answer spaces allow accidental agreement with the reference answer.
  • E. Why Z3 and Rubric Disagree: Section E. Why Z3 and Rubric Disagree: Closed-world candidate formalizations may diverge at the constraint or relation layer without changing the solver’s decision.
  • E. Why Z3 and Rubric Disagree: Section E. Why Z3 and Rubric Disagree: Positive-only rubrics test required semantics but may pass added constraints, weakened relations, or unanticipated free variables.
  • E. Why Z3 and Rubric Disagree: Section E. Why Z3 and Rubric Disagree: The 72.36% Fixed-symbols Rubric ceiling measures rubric coverage rather than faithful formalization, leaving some errors invisible to both signals.
  • E. Why Z3 and Rubric Disagree: Section E. Why Z3 and Rubic Disagree: The Both column combines solver filtering with rubric auditing, but inherits both biases and remains harder to align in free-form formalization.
  • F. A Closer Look at Hard-Subset Difficulty: Section F. A Closer Look at Hard-Subset Difficulty: This analysis describes how hardening operators reshape the task, whereas the following error analysis examines concrete model failures.

F.1. Counterfactual recomputation

Counterfactual variants expose whether models globally recompute dependent conclusions or merely patch the edited fact. Across variants, counterfactual questions consistently reduce accuracy, isolating recomputation as a distinct burden.

  • Counterfactual recomputation: Counterfactual editing requires reopening every branch whose status depended on the changed fact, rather than retaining downstream conclusions derived from the original baseline.The operator replaces one fact or rule while holding the rest of the item fixed.
  • Counterfactual recomputation: Every thinking variant loses accuracy on counterfactual sub-questions, with drops ranging from 3.6 pp to 11.0 pp.The baseline and counterfactual questions share items and discourse style, helping isolate recomputation cost from topic or wording effects.
  • Counterfactual recomputation: Hard items combine branching, distractors, set-valued outputs, uncertainty, and alias tracking, creating multiple interacting axes that must be maintained together.These mechanisms require combining consequential axes rather than solving them independently.
  • Counterfactual recomputation: Hard items average 4.94 sub-questions, and Item Accuracy requires every sub-question to be correct, so one error can undermine the whole item.Later questions query the same closed model space through projections, alternatives, updates, or evidence tiers.
  • Counterfactual recomputation: The failure analysis distinguishes modal-quantifier confusion and incomplete model enumeration among Base errors, alongside counterfactual and other Hard failures.The taxonomy retains case studies whose reference answers remained stable under re-audit.

G.2. Hard Errors

Hard-error cases show that models fail when reasoning requires global state maintenance, exhaustive enumeration, projection across set levels, and preservation of evidence validity. The examples span counterfactual updates, interacting state axes, and nested set structures.

  • Hard Errors: Local counterfactual editing is the largest Hard failure source: models change one fact while retaining downstream conclusions derived from the old fact.Correct solving requires recomposing the edited fact with all surviving branches.
  • Hard Errors: Complete enumeration fails when models solve interacting uncertainty axes separately and omit legal cross-products from the full state space.This error can cascade from the baseline model set into later projection, comparison, and counterfactual questions.
  • Hard Errors: Projection-level errors arise when models classify individual elements instead of set-family members or fail to map formal set operations back to required semantic labels.Correct solving projects complete baseline models to their direct-basis sets and deduplicates the resulting family.
  • Hard Errors: Evidence-provenance failures occur when models elevate weak evidence, retain counterfactually invalidated chains, or lose the binding between evidence sources and conclusions.Hard items include formal records, marginal notes, ambiguous annotations, destroyed confirmations, and source-dependent validity.
  • Hard Errors: The modal-quantifier case shows all 14 models answering a validity question instead of the requested satisfiability question, despite formally sound local entailment statements.This is a binary-decision failure caused by tracking the wrong quantifier.
  • Hard Errors: The semantic-equivalence judge accepts equivalent sets, counts, labels, orderings, and answer polarities rather than requiring literal string matches.It evaluates each sub-question within the complete multi-subquestion problem and preserves internally consistent model numbering.
Loading 2605.19597v1…