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

Many natural-language logic benchmarks derive items from sampled formulas, producing template-like phrasing rather than realistic scenarios. LLMEval-Logic builds a Chinese benchmark through forward authoring and auditing; across 14 frontier LLMs, the top Hard Item Accuracy is 37.5%.

  • Problem

    Many natural-language logic benchmarks reverse-construct items from formulas, yielding template-like language rather than realistic scenarios, despite the need to evaluate premise-faithful reasoning.

    Source: §1 · pp. 1–2

  • Method

    LLMEval-Logic forward-authors Chinese scenario-based items, expert-reviews formalizations, verifies answers with Z3, adds rubrics, and adversarially hardens items into paired Base and Hard subsets.

    Source: §1 · p. 3, §2.1 · p. 4

  • Results

    Across 14 frontier LLMs, performance differs across Base, Hard, and formalization faithfulness, and top Hard Item Accuracy is 37.5%.

    Source: §5 · p. 10

  • Takeaways & Limitations

    Base accuracy, Hard accuracy, and formalization faithfulness capture distinct aspects of frontier logical reasoning and should be considered as separate evaluation dimensions.

    Source: §5 · p. 10

    The benchmark covers Chinese natural-language items, so generalization of natural-to-formal evaluation to other languages and writing conventions remains empirically unvalidated.

    Source: Limitations · p. 10

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

Because rule-governed applications require conclusions to follow stated premises, LLMEval-Logic addresses gaps in realistic scenarios, auditable formalization, and frontier-model discrimination with paired Chinese Base and Hard subsets.

1. Introduction

  • Existing benchmarks face three gaps: template-like items lack realistic grounding, formal annotations lack local semantic auditing, and many splits saturate under frontier models.The formalization gap includes whether logical relations, constraints, and queries are faithfully encoded in a model-produced translation.Source: §1 · p. 2
  • LLMs face an empirical alignment bottleneck in identifying the logical relations, types, and quantifiers needed to faithfully formalize natural-language reasoning, motivating evaluation for high-stakes rule-governed tasks.The introduction frames reliable benchmarking as a prerequisite for trustworthy deployment where conclusions must follow from stated premises.Source: §1 · pp. 1, 3
  • Base covers single-question PL/FOL reasoning and formalization grading with 1,400 rubric atoms; Hard uses adversarial multi-question items requiring every sub-question to be correct.The rubric atoms cover logical relations, stated constraints, and query alignment.Source: Figure 3 · p. 3, §1 · p. 3
  • LLMEval-Logic is a Chinese benchmark pairing forward-authored situational items with expert-reviewed formalizations, Z3-verified answers, expert rubrics, and paired Base/Hard subsets.The pipeline checks lexical, syntactic, semantic, and type-and-parameter consistency before solver verification; rubrics assess logical relations, stated constraints, and query alignment.Source: Figure 2 · p. 2, §1 · p. 3
  • Items found too easy in model probing enter a five-role adversarial workflow that applies six hardening strategies and retains only reviewed and verified Hard items.The roles are Decider, Proposal, Review, Answering, and Verification, with a per-step audit trace for accepted items.Source: §1 · p. 3
  • The authors evaluate 14 frontier LLM variants over three independent runs on natural-language logical reasoning and faithful natural-to-formal translation.The benchmark evaluates answer accuracy and formalization accuracy, including Z3 execution and rubric matching.Source: Figure 2 · p. 2, §1 · p. 3

2. Design

LLMEval-Logic constructs a Chinese logical-reasoning benchmark through forward authoring, expert review, Z3 verification, and expert rubrics. Validated Base items can enter an adversarial workflow that produces the Hard subset, and both answer accuracy and formalizations are evaluated.

2.1. Dataset Construction

  • Base items are forward-authored as Chinese scenarios, expert-reviewed and normalized, then Z3-verified before inclusion.The three task types are possible, necessary, and enumerate_models; failed checks trigger repair and re-verification.Source: §2.1 · pp. 4–5
  • Expert rubrics assess logical relations, stated constraints, and query alignment in model-produced formalizations.Each criterion has a natural-language form and a Z3-checkable form, calibrated so the expert-confirmed reference passes the full rubric set.Source: §2.1 · pp. 4–5

2.2. Adversarial Hardening

  • Difficulty probes route candidates only; high-accuracy items enter a five-role hardening loop and must pass review and verification gates.The loop uses branching, valid distractors, explicit uncertainty, set-valued outputs, counterfactual variants, and alias/coreference variation to alter candidate spaces or required operations rather than merely reword items.Source: §2.2 · pp. 5–6
  • Hard contains 190 items and 938 sub-questions, averaging 4.94 per item, and adds unique_solution and has_alternative operations over closed model spaces.Items contain 2–8 sub-questions, requiring models to maintain and update the full candidate space across related queries.Source: §2.2 · p. 6

2.3. Evaluation Protocol

  • Answer accuracy and rubric atoms are LLM-judged across three runs, while Base formalizations are scored under free-symbol and fixed-symbol settings.Formalization signals are Z3 execution, rubric pass rate, and their agreement; re-judging samples with two additional frontier judges yielded pairwise Cohen’s κ of 0.873–0.922 and identical verdicts on 93% of items.Source: §2.3 · p. 6

3. Experiment and Analysis

The analysis tests whether forward-authored items resist template shortcuts, how faithfully models formalize natural-language logic, and whether Hard items distinguish frontier models and expose their failure modes.

3.1. Experimental Setup

  • The evaluation covers 14 frontier LLMs from 7 model families in thinking and no-thinking configurations, with three runs reported as mean ± std.Table 2 reports formalization results on 246 Base items and includes the gold reference as an upper-bound calibration that passes both Z3 execution and rubric matching.Source: §3.1 · p. 7

3.2. RQ1: Shortcut Resistance of Forward-Authored Items

  • 65.1% Base Item Accuracy versus 22.9% Hard Item Accuracy marks a 42.2-point average drop, while the strongest Hard score is 37.5 ± 3.8%.Hard items retain natural language and scenarios while adding closed-world recomputation, branching, distractors, set-valued outputs, uncertainty, and alias/coreference tracking.Source: §3.2 · p. 7

3.3. RQ2: Faithfulness of Natural-to-Formal Translation

  • For every model, the joint Z3+Rubric score is lower than either individual signal in both free-symbol and fixed-symbol settings.Z3 can accept formalizations that reach the reference answer while distorting semantics; rubric checklists can miss extra or mis-specified constraints, making their combination a stricter practical proxy for faithfulness.Source: §3.3 · p. 7
  • 60.16% is the highest non-gold Fixed Z3+Rubric score, while GPT-5.4 Pro (no-think) rises from 32.93% to 60.16% with reference symbols.The best non-gold score remains below the 100% gold reference, indicating residual translation failures even when symbols and glosses are supplied.Source: §3.3 · p. 7

3.4. RQ3: Discriminative Headroom on Frontier Reasoning Models

  • Every model family drops from Base to Hard, and disabling thinking costs open-weight Chinese models 20–26 pp of Hard Item Accuracy.The hardened multi-question scenarios require maintaining the full candidate space across related queries; the supplied passage cuts off before completing its comparison with proprietary models.Source: §3.4 · p. 7

Z3 Rubric Both Z3 Rubric Both

Base and Hard results diverge for thinking-enabled frontier models, while Hard exposes failures in maintaining closed candidate spaces across chained queries. On Base, Z3 and rubric judgments also remain below the stated rubric ceiling and gold performance.

Z3 Rubric Both

  • Hard produces wider performance gaps across model families than Base when models reason over complex closed candidate spaces.The no/low-thinking effect is family-specific, with Chinese open-weight families dropping on both Base and Hard.Source: Z3 Rubric Both Z3 Rubric Both · p. 8, Figure 7 · p. 9
  • A 25–43-point Sub-Q-to-Item accuracy gap on Hard shows that models often solve individual questions but fail the all-subquestions-correct item criterion.Hard requires global recomputation after counterfactual edits and exhaustive candidate-space maintenance under branching, distractors, uncertainty, set-valued outputs, and coreference; observed failures include missed dependencies, under-enumeration, projection confusion, and lost evidence or validity boundaries.Source: Z3 Rubric Both Z3 Rubric Both · p. 8, Figure 7 · p. 9
  • On Base, most thinking-variant points fall below the Z3-equals-rubric line, and fixing symbols shifts results up-right, but none exceeds the 72.36% rubric ceiling or reaches gold at (100, 100).Table 2 reports Base formalization accuracy with Z3, rubric, and agreement signals, using gpt-5.1-chat judges validated against two further frontier judges.Source: Table 2 · p. 8, Figure 5 · p. 9
  • Seed 2.0 Pro and Hy3 preview fall from Base accuracy of 75.5% and 75.3% to Hard accuracy of 20.4% and 21.6%, while Claude Opus 4.6 rises from last on Base to second on Hard (thinking ρ=−0.61).The inversion shows that high single-question accuracy does not reliably transfer to adversarial multi-question reasoning over closed candidate spaces; no/low-thinking variants instead have a positive correlation (ρ=+0.79).Source: Z3 Rubric Both Z3 Rubric Both · p. 8, Figure 6 · p. 9

4. Related Work

Prior logical-reasoning benchmarks include formula-derived symbolic worlds and human-written narratives, while NL-to-formal-language evaluation and difficulty hardening leave gaps in semantic auditing and item design. LLMEval-Logic addresses these gaps with expert-audited Chinese scenarios, rubric-graded formalizations, and controlled hardening.

Logic benchmarks

  • Benchmarks include symbolic-world items in RuleTaker (Clark et al., 2020), Proof Writer (Tafjord et al., 2021), LogicBench (Parmar et al., 2024), and SATBench (Wei et al., 2025), while FOLIO (Han et al., 2024a,b) adds human-written narratives with FOL annotations.These resources advanced natural-language reasoning evaluation, but formula-derived construction can leave template-like artifacts, and final-answer scoring alone cannot audit whether formalization preserves source semantics.Source: §4 · pp. 9–10
  • LLMEval-Logic contributes forward-authored Chinese scenarios paired with expert-audited reference formalizations and Z3-verified answers to the LLMEval evaluation framework (Zhang et al., 2023, 2025a,b, 2024).Source: §4 · p. 10

NL-to-FL eval and hardening

  • NL-to-FL work (Yang et al., 2024) uses answer- or execution-level signals that do not localize mis-encoded source content, so LLMEval-Logic scores formalizations with expert rubric atoms.The rubric covers logical relations, stated constraints, and query alignment.Source: §4 · p. 10
  • Prior difficulty methods use proof depth (Saparov and He, 2023; Saparov et al., 2023), SAT puzzles (Wei et al., 2025), counterintuitive compositions (Chung et al., 2025), or logic grids (Lin et al., 2025); LLMEval-Logic restructures closed candidate spaces through controlled hardening.The resulting items are interpretable to humans, executable by solvers, and discriminative for current frontier LLMs.Source: §4 · p. 10

5. Conclusion

LLMEval-Logic pairs Z3-verified Chinese Base items with adversarially hardened Hard items and evaluates answer accuracy alongside rubric-graded formalization faithfulness. Its results show that these metrics capture distinct aspects of frontier logical reasoning.

5. Conclusion

  • 37.5% Hard Item Accuracy was the highest score among 14 frontier LLMs evaluated across three runs.The conclusion also reports family-specific no-thinking collapse, divergent Base and Hard rankings, and Z3 correctness overestimating rubric faithfulness.Source: §5 · p. 10
  • No-thinking collapse was family-specific, Base and Hard rankings diverged, and Z3 correctness overestimated rubric faithfulness, indicating distinct evaluation signals.Source: §5 · p. 10
  • The benchmark pairs Z3-verified Base items with adversarially hardened Hard items, using answer accuracy and rubric-graded formalization faithfulness.The authors say forward authoring and Z3/rubric auditing form its quality-control foundation, while controlled hardening preserves discrimination as raw accuracy saturates; they plan to release the benchmark, workflow, and audit traces upon publication.Source: §5 · p. 10

Limitations … B.2. Six Hardening Strategies

The appendices qualify the benchmark’s language, logic, and annotation scope, then describe normalization and a gated adversarial workflow whose six strategies make hard items structurally rather than superficially more demanding.

Limitations

  • The benchmark covers Chinese items and propositional and first-order logic; extending languages and logic types, and fully validating natural-language equivalence, remain open limitations.Z3 verifies entailment from the normalized reference formalization, while expert rubrics mitigate—but may not eliminate—formalization gaps and fine-grained blind spots.Source: Limitations · p. 10

A. Layered Normalization Pipeline

  • Normalization converts varied author notation into typed, parameter-normalized formulas for Z3 through lexical, syntactic, semantic-alignment, and type-and-parameter layers.The layers unify glyphs and formatting, parse formulas and route failures to human repair, check symbol roles and glosses, then separate PL and FOL with corresponding normalization.Source: A. Layered Normalization Pipeline · p. 15

B. Adversarial Hardening Workflow

  • Only items that pass review and verification gates enter Hard; failed proposals loop back for revision, while answer-only failures trigger answer repair.The five-step loop is Decider → Proposal → Review → Answering → Verification → finalize.Source: B. Adversarial Hardening Workflow · p. 15

B.1. Agent Roles

  • Decider plans hardening across six strategies, while specialized background and question proposers implement the blueprint and reviewers audit mechanisms, question responsibilities, and strategy coverage.The question proposer writes against the locked background using the fixed Hard question-type schema; review issues use a fixed catalog.Source: §B.1 · p. 15
  • A three-model answerer ensemble produces answers and reasoning traces, an adjudicator resolves disagreements, and verification checks correctness, reasoning, leakage, and reviewer misses.Verification can trigger answer repair or return an item to the proposers when answering reveals residual design flaws.Source: §B.1 · p. 16

B.2. Six Hardening Strategies

  • The strategies add cross-constrained branching, consequential distractors, and closed-space complete-search outputs, each altering the candidate space, operation, or reasoning path rather than merely rewording an item.Complete-search tasks include enumeration, counting, projection, uniqueness, alternative-solution search, or feasible-set intersections and differences.Source: §B.2 · p. 16
  • The remaining strategies preserve multiple computable worlds under mechanism-grounded uncertainty, test distinct counterfactual flips, and use resolvable aliases that impose genuine entity-tracking cost.Uncertainty can propagate to downstream questions; counterfactuals hold other conditions constant, and aliases must do more than substitute surface synonyms.Source: §B.2 · p. 16

B.3. Quality Control Statistics

Hardening required repeated proposer revisions and answer repair, while Reviewer and Verifier gates caught complementary design flaws. Of 254 items entering the workflow, 224 completed, before further manual curation for release.

B.3. Quality Control Statistics

  • 224 of 254 items entering hardening completed (88.2%); 30 exhausted the retry budget and were excluded from gate counters, and manual curation later removed more items.The 224 count measures workflow completion, not the final released-item count.Source: §B.3 · p. 17
  • 89.3% of items trigger proposer retries (mean 4.0), 80.8% enter Review→Proposer, and 58.0% return Verify→Proposer after passing review.The Verifier catches flaws that Reviewer-only checks miss when model-answering traces reveal shallow solution paths or unused background mechanisms.Source: §B.3 · p. 17, Table 4 · p. 17
  • 58.9% of items require at least one answer repair, showing answer generation can remain iterative even when item design is sound.Source: §B.3 · p. 17

C. Evaluation Detail … C.2.3. Rubric Mode — Fixed Formalization

The evaluation pipeline separates answer checking from natural-language-to-formal translation, using solver execution and rubric judgments to assess answers and formalizations. Fixed-formalization rubric scoring combines Z3 equivalence checks with targeted LLM review of ambiguous premise differences.

C.1. Answer Evaluation

  • For answer evaluation, models return structured JSON and an LLM judge compares each response with the reference answer for semantic equivalence.Separate judge prompts address multi-subquestion and flat single-answer items; harmless formatting or labeling differences are accepted, while contradictory or incomplete answers are rejected.Source: §C.1 · p. 17

C.2. Translation Evaluation

  • Translation evaluation first has models produce solver-compatible FL JSON, either declaring all symbols and translations freely or using provided gold symbols as read-only context.In Fixed-FL, models write only the premise set and solver queries.Source: §C.2 · p. 17

C.2.1. Z3 Mode

  • In Z3 mode, the candidate FL is executed under its premises, and an LLM judges the solver-derived answer against the gold reference answer for semantic equivalence.The judge accepts specified structurally recoverable transformations, including formatting variations, stronger-positive possibility answers, and complement-based queries.Source: §C.2.1 · p. 17

C.2.2. Rubric Mode — Free Formalization

  • Free-FL rubric scoring checks candidate premises and queries against per-problem logical-relation, stated-constraint, and query-alignment requirements.A Z3 check may establish query equivalence for QA items; otherwise the LLM judges them, while LR and SC items are judged entirely by the LLM.Source: §C.2.2 · p. 18
  • Free-FL rubric scoring evaluates formalization quality independently of answer correctness.The scoring prompt specifies acceptable variants, equivalent rewritings, and boundaries between reasonable alternatives and genuine errors.Source: §C.2.2 · p. 18

C.2.3. Rubric Mode — Fixed Formalization

  • In fixed-FL rubric mode, Z3-equivalent premises auto-pass LR/SC items, while matching solved answers trigger LLM review of individual premise differences.Defensible extra or missing premises can softpass and promote failed LR/SC items; genuine errors fail. This hybrid reserves LLM review for ambiguous cases while reducing false positives from reasonable alternatives.Source: §C.2.3 · p. 18

D. LLM-as-Judge Validation

The validation finds high agreement among three LLM judges on sampled answer and rubric verdicts, while noting that shared blind spots and the rubric check’s limited scope remain possible.

D. LLM-as-Judge Validation

  • Using gpt-5.1-chat as the main evaluator, researchers rejudged 103 Hard sub-questions and 105 LLM-delegated rubric atoms with Claude Opus 4.6 and Gemini 3.1 Pro.Judges used the main protocol’s answer- and rubric-judging prompts; all ran at temperature 0, with Claude and Gemini reasoning disabled for deterministic verdicts.Source: D. LLM-as-Judge Validation · p. 18, Table 5 · p. 19
  • All six pairwise Cohen’s κ values were 0.873–0.922, pairwise agreement was ≥94%, and unanimous agreement was 93.2% for sub-questions and 93.3% for rubric atoms.The reported κ values exceed the stated κ≥0.7 threshold typically asked of judge-replacement studies and fall in the almost-perfect band (κ≥0.81).Source: Table 5 · p. 19, D. LLM-as-Judge Validation · p. 19
  • Because Claude and Gemini also appear on the leaderboard, agreement cannot rule out family-correlated blind spots, and rubric-side validation covers only atoms decided by the LLM.The 93% unanimous-agreement rate bounds the size of any joint blind spot in the sampled items but cannot eliminate it; Z3-prefiltered atoms are deterministic, so the check does not validate the full hybrid rubric pipeline.Source: D. LLM-as-Judge Validation · p. 19

E. Why Z3 and Rubric Disagree · F. A Closer Look at Hard-Subset Difficulty

Z3 and Rubric expose complementary weaknesses in evaluating formalizations: Z3 can accept structurally wrong candidates, while Rubric can miss errors beyond its positive coverage. The hard-subset analysis frames difficulty in terms of how hardening operators reshape the task.

E. Why Z3 and Rubric Disagree

  • 72.36% is the strongest Fixed-symbols Rubric score, below the gold reference’s 100%, while Free Z3 accuracy systematically exceeds Free Rubric accuracy.The authors attribute both patterns to how the signals are designed, not to one failure mode in candidate formalizations.Source: E. Why Z3 and Rubric Disagree · p. 19
  • Z3 can mark structurally mismatched formalizations correct when over-constraints, flipped relations, or omitted constraints do not change the queried decision.The largest Free Z3−Rubric gaps are GPT-5.4 Pro (66.26 −42.28 = 23.98), Qwen 3.5 Plus (61.79 −46.75 = 15.04), and Claude Opus 4.6 (64.63 −50.41 = 14.22).Source: E. Why Z3 and Rubric Disagree · pp. 19–20
  • Rubric checks whether expected semantic atoms are present, but its positive-only coverage can miss added constraints, weakened relations, or unanticipated free variables.With 5.69 atoms per item on average, its 72.36% Fixed-symbols ceiling combines missed atoms with errors invisible to both Rubric and Z3.Source: E. Why Z3 and Rubric Disagree · p. 20
  • The Both metric is the closest practical single-shot estimator of faithful formalization, but it inherits both signals’ biases and the difficulty of aligning free-form formalizations.Different symbols, predicates, type granularities, intermediate objects, and query decompositions can make candidate formalizations incompatible with the reference space; the authors recommend tracking Both rather than Z3 alone for NL→FL faithfulness.Source: E. Why Z3 and Rubric Disagree · p. 20

F. A Closer Look at Hard-Subset Difficulty

  • The hard-subset analysis explains difficulty through three mechanisms by describing how hardening operators reshape the task, rather than cataloguing concrete model failures.Concrete failure cases are reserved for Error Analysis in Appendix G.Source: F. A Closer Look at Hard-Subset… · p. 20

F.1. Counterfactual recomputation … G.1. Base Errors

The analysis finds that counterfactual questions impose a recomputation burden and that broader candidate-space demands challenge models. It identifies modal quantifier tracking and incomplete model enumeration as two Base error patterns.

The non-counterfactual strategies enlarge

  • Branching, valid distractors, set-valued outputs, uncertainty, and alias/coreference variation enlarge the candidate-space demands even when each logical relation is locally simple.These operators require combining consequential axes, rejecting lexically overlapping but invalid evidence, searching closed candidate sets, propagating evidence tiers across admissible worlds, and tracking entities.Source: The non-counterfactual strategies… · p. 21

F.1. Counterfactual recomputation

  • Qwen 3.5 Plus drops 3.6 pp and Seed 2.0 Pro drops 11.0 pp; every thinking variant loses accuracy on counterfactual sub-questions.The 938 Hard sub-questions are partitioned into 686 baseline and 252 counterfactual questions; each counterfactual replaces one fact or rule while holding the rest of the item fixed. Because both partitions occur within the same items and share discourse style, the observed drop isolates recomputation burden from topic or wording effects.Source: §F.1 · p. 20, Table 6 · p. 21

F.3. Multi-question state maintenance

  • Hard items average 4.94 sub-questions, and Item Accuracy requires every sub-question to be correct, so one missed branch or update can collapse the item score.Base, Hard Sub-Q, and Hard Item scores distinguish single-shot encoding, local partial credit, and sustained all-correct control over a shared model space.Source: §F.3 · p. 21
  • Baseline-versus-counterfactual, set-valued and uncertainty/distractor, and alias/coreference slices diagnose recomputation, exhaustive search and interference control, and entity tracking, respectively.Reporting these slices alongside aggregate Hard scores helps distinguish weak local encoding from failure to maintain the candidate space across an item.Source: §F.3 · p. 21

G. Error Analysis

  • Because items provide all required background facts, dominant errors are failures of formal semantics, complete model-set maintenance, and counterfactual recomputation rather than knowledge gaps.The taxonomy contains two Base error types and four Hard error types, with case studies retained only when reference answers remain stable under re-audit.Source: G. Error Analysis · p. 21

G.1. Base Errors

  • Base errors commonly confuse existential and universal queries in both directions, promoting what holds in some feasible models to all, or downgrading forced conclusions to uncertainty.Models also answer validity when asked whether a conclusion is merely satisfiable; high-frequency errors occur in both ^→□ and □→^ directions.Source: §G.1 · p. 22
  • Incomplete model enumeration replaces all feasible assignments with a first coherent explanation, prunes legal branches, or merges independent uncertainty dimensions.This makes enumerate_models and count_models especially fragile because an under-enumerated model set necessarily yields an incorrect list and count.Source: §G.1 · p. 22

G.2. Hard Errors … ID #359.3 Projection-Level Set Family Failure (hard/direct basis set)

This section covers hard errors in logical reasoning and defines prompts for adjudicating semantic answers and auditing natural-language-to-formal translations. It focuses on recomputing dependent branches, enumerating interacting uncertainties, reasoning at the correct set-family level, and preserving evidence provenance and validity tiers, while prioritizing meaning and fidelity to the source problem.

G.2. Hard Errors

  • Counterfactual recomputation is the largest Hard failure source: models patch an edited fact but retain conclusions derived from the old fact.Correct solving requires reopening every branch that depended on the edited evidence; Figure 9 illustrates recomposing the meeting change with surviving branches over Xiaomai’s status and old-friend aliases.Source: §G.2 · p. 22, Figure 9 · p. 24, ID #359.4 Counterfactual Set-Family… · p. 24
  • Models often enumerate uncertainty axes separately and miss legal cross-products, so an error in the baseline model set cascades into later questions.Figure 10’s state-tuple task requires enumerating five non-alarm states and one alarm-trigger state rather than treating a stale mirror snapshot as current.Source: §G.2 · p. 22, Figure 10 · p. 25, ID #252.1 Complete Enumeration Failure… · p. 25
  • Models frequently compute at the wrong nested-set level or fail to map formal set differences back to semantic labels.Figure 11 requires projecting each complete baseline model to its direct-basis set and deduplicating the resulting family of sets.Source: §G.2 · p. 22, Figure 11 · p. 26, ID #359.3 Projection-Level Set Family… · p. 26
  • Hard tasks expose failures to maintain evidence provenance and validity tiers, including elevating weak evidence or retaining chains invalidated by counterfactuals.Structured candidates may also lose the binding between an evidence source and its conclusion.Source: §G.2 · p. 22

H. Human Annotation Details

  • Students with at least one year of mathematical-logic training authored fictional Chinese problems and supplied initial formalizations and answers, which experienced logic researchers audited.Audits covered clarity, reasoning validity, natural-language–formal-language faithfulness, and rubric atoms; contributors were informed of research use and consented.Source: H. Human Annotation Details · pp. 22–23

ID #359.3 Projection-Level Set Family Failure (hard/direct basis set)

  • The answer judge accepts semantically identical answers despite changes in numbering, order, labels, or equivalent quantity and polarity expressions, but requires an explicit empty-set answer when the reference is empty.It judges each subquestion in context, follows internally consistent local labels, and rejects substantive contradictions, omissions, or incompatible additions.Source: ID #359.3 Projection-Level Set Family… · p. 38
  • Free-FL formalization requires one JSON object with declared symbols, translations, premise formulas, and solver queries in the supported syntax.The formalization must cover the full problem and question, and must not output an answer.Source: ID #359.3 Projection-Level Set Family… · p. 39
  • Rubric checklist scoring requires each formalization to express the stated constraint without strengthening it beyond what the natural-language source justifies.Evaluators score checklist items as binary semantic matches and should not judge final-answer correctness or solve the task.Source: ID #359.3 Projection-Level Set Family… · p. 41
  • Premise-equivalence soft review treats the original natural-language problem as authoritative and rejects extra premises unless the source or checklist clearly justifies them.An extra constraint that changes satisfiability or affects the question’s answer fails review; answer coincidence alone is insufficient justification.Source: ID #359.3 Projection-Level Set Family… · p. 42

Related papers

Loading 2605.19597v1…