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

arXiv: https://arxiv.org/abs/2605.19597 · HTML: https://mlsanity.com/paper/2605.19597/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 7 of its 36 references that are in the map.
- First posted on arXiv 19 May 2026.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 7 of 7)

- [DeepSeek-V4: Towards Highly Efficient Million-Token Context Intelligence](https://mlsanity.com/paper/2606.19348/) (2026)
- [Humanity's Last Exam](https://mlsanity.com/paper/2501.14249/) (2025)
- [FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI](https://mlsanity.com/paper/2411.04872/) (2024)
- [ReClor: A Reading Comprehension Dataset Requiring Logical Reasoning](https://mlsanity.com/paper/2002.04326/) (2020)
- [AutoLogi: Automated Generation of Logic Puzzles for Evaluating Reasoning Abilities of Large Language Models](https://mlsanity.com/paper/2502.16906/) (2025)
- [The Ouroboros of Benchmarking: Reasoning Evaluation in an Era of Saturation](https://mlsanity.com/paper/2511.01365/) (2025)
- [From 0-Order Selection to 2-Order Judgment: Combinatorial Hardening Exposes Compositional Failures in Frontier LLMs](https://mlsanity.com/paper/2605.07268/) (2026)

## Abstract (arXiv)

Existing logic benchmarks primarily measure models' ability to answer reasoning questions directly. Scalable benchmarks often generate text from formal structures, which makes answers easy to compute but fixes the formalization before the problem is written. Forward construction preserves the challenge of finding a faithful formalization, yet makes difficulty and answer reliability harder to control. We introduce HyperLogic, a forward-construction pipeline that separates problem authoring from answer generation. A multi-agent workflow hardens undergraduate-authored Chinese seeds without solving them; two agents from different model families independently translate each finished item into executable finite-domain models; their encodings and solver-derived answers undergo layered, agent-assisted adjudication under human-expert oversight. HyperLogic-Base contains 195 items and 922 sub-questions and separates seven frontier models by 33.0 percentage points in strict item accuracy (44.6-77.6%). HyperLogic-Hard contains 100 items with larger, coupled search spaces, on which no model exceeds 16% accuracy in direct answering. We also use Hard to evaluate agents' ability to formalize and solve problems with tools, comparing a code sandbox alone with one that includes our logic modeling library. The sandbox improves every model by 16.7-40.1 points; adding the library helps five models and hurts two. These results highlight the difficulty of faithful formalization even with tool access.