Evaluating the Formal Reasoning Capabilities of Large Language Models through Chomsky Hierarchy
On the map: LLM reasoning → Reasoning benchmarks and evaluation
Abstract (arXiv)
The formal reasoning capabilities of LLMs are crucial for advancing automated software engineering. However, existing benchmarks for LLMs lack systematic evaluation based on computation and complexity, leaving a critical gap in understanding their formal reasoning capabilities. Therefore, it is still unknown whether SOTA LLMs can grasp the structured, hierarchical complexity of formal languages as defined by Computation Theory. To address this, we introduce ChomskyBench, a benchmark for systematically evaluating LLMs through the lens of Chomsky Hierarchy. Unlike prior work that uses vectorized classification for neural networks, ChomskyBench is the first to combine full Chomsky Hierarchy coverage, process-trace evaluation via natural language, and deterministic symbolic verifiability. ChomskyBench is composed of a comprehensive suite of language recognition and generation tasks designed to test capabilities at each level. Extensive experiments indicate a clear performance stratification that correlates with the hierarchy's levels of complexity. Our analysis reveals a direct relationship where increasing task difficulty substantially impacts both inference length and performance. Furthermore, we find that while larger models and advanced inference methods offer notable relative gains, they face severe efficiency barriers: achieving practical reliability would require prohibitive computational costs, revealing that current limitations stem from inefficiency rather than absolute capability bounds. A time complexity analysis further indicates that LLMs are significantly less efficient than traditional algorithmic programs for these formal tasks. These results delineate the practical limits of current LLMs, highlight the indispensability of traditional software tools, and provide insights to guide the development of future LLMs with more powerful formal reasoning capabilities.
Key facts. No citing papers in the map yet (data through 7 Oct 2026). Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning. Builds on 28 of its 57 references that are in the map. First posted on arXiv 3 Apr 2026.
Builds on
28 of 57 references.
Closest ancestors · 3
Same direction, newest first
- 2025Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework28 Apr
- 2024Training Neural Networks as Recognizers of Formal Languages11 Nov
- 2024Proof of Thought : Neurosymbolic Program Synthesis allows Robust and Interpretable Reasoning25 Sep
Other references · 25
- 2017Attention Is All You Needcited by 59,932
- 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Modelscited by 8,851
- 2021Evaluating Large Language Models Trained on Codecited by 8,053
- 2021Program Synthesis with Large Language Modelscited by 3,509
- 2023SWE-bench: Can Language Models Resolve Real-World GitHub Issues?cited by 3,193
- 2023Sparks of Artificial General Intelligence: Early experiments with GPT-4cited by 2,579
- 2024LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Codecited by 1,906
- 2024A Survey on Large Language Models for Code Generationcited by 646
- 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
- 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
- 2022Autoformalization with Large Language Modelscited by 252
- 2022Neural Networks and the Chomsky Hierarchycited by 214
13 more
- 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
- 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 173
- 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
- 2020On the Computational Power of Transformers and its Implications in Sequence Modelingcited by 85
- 2024EvoCodeBench: An Evolving Code Generation Benchmark Aligned with Real-World Code Repositoriescited by 71
- 2024DevEval: A Manually-Annotated Code Generation Benchmark Aligned with Real-World Code Repositoriescited by 71
- 2023nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Modelscited by 57
- 2024Process-Driven Autoformalization in Lean 4cited by 45
- 2024Autoformalizing Euclidean Geometrycited by 27
- 2025PDE-Controller: LLMs for Autoformalization and Reasoning of PDEscited by 23
- 2025Constant Bit-size Transformers Are Turing Completecited by 19
- 2025Finite State Automata Inside Transformers with Chain-of-Thought: A Mechanistic Study on State Trackingcited by 17
- 2024Simulating Weighted Automata over Sequences and Trees with Transformerscited by 4
Built on by
Not cited yet.
Similar, not cited
Close in wording, no citation either way
- 2025HiBench: Benchmarking LLMs Capability on Hierarchical Structure Reasoning
- 2026Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification
- 2023Chain-of-Thought Hub: A Continuous Effort to Measure Large Language Models' Reasoning Performance
- 2025RELIC: Evaluating Complex Reasoning via the Recognition of Languages In-Context
- 2024The CLRS-Text Algorithmic Reasoning Language Benchmark
- 2023NPHardEval: Dynamic Benchmark on Reasoning Ability of Large Language Models via Complexity Classes
- 2026Grading the Graders: Verification Autonomy Levels (L0-L5) for LLM Reasoning
- 2026ReEfBench: Quantifying the Reasoning Efficiency of LLMs