LLMEval-Logic: een solver-geverifieerd Chinees benchmark voor logisch redeneren van LLMs met adversarial hardening

Samenvatting

Het evalueren van grote taalmodellen (LLMs) op natuurlijke-taal logisch redeneren is essentieel omdat regelgeleide taken vereisen dat conclusies strikt volgen uit gestelde premissen. Veel bestaande logische-redeneringsbenchmarks worden gegenereerd door het templaten van natuurlijke-taalitems uit bemonsterde formules, bieden alleen grove of niet-gecontroleerde formele annotaties, en worden nu snel verzadigd door geavanceerde redeneringsmodellen. We presenteren LLMEval-Logic, een Chinese logische-redeneringsbenchmark gebouwd op realistische situationele scenario's. De pipeline forward-authors en expert-audits natuurlijke-taalitems samen met hun referentieformalizeringen, verifieert geannoteerde antwoorden met Z3, construeert expertrubrieken voor natuurlijk-naar-formeel beoordelen, en verstevigt geselecteerde items via een gesloten-lus adversarial workflow. De benchmark wordt uitgebracht in twee gepaarde subsets: een 246-item Base subset geleverd met 1.400 door experts ontwikkelde rubriekatomen, en een 190-item Hard subset met 938 meerstaps subvragen over gesloten modelruimtes. Het evalueren van 14 geavanceerde LLMs op LLMEval-Logic onthult aanzienlijke hiaten in huidige modellen: het beste model bereikt slechts 37,5% Hard Item Accuracy, en zelfs met referentiesymbolen bereikt de hoogste gezamenlijke Z3+Rubric formalisatiescore onder geëvalueerde modellen slechts 60,16%. Onze benchmark is openbaar beschikbaar op https://github.com/llmeval/LLMEval-Logic.

English

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.