Evaluating the Formal Reasoning Capabilities of Large Language Models through Chomsky Hierarchy

Yihong Dong; Jianha Xiao; Xue Jiang; Xuyuan Guo; Zhiyuan Fan; Jiaru Qian; Kechi Zhang; Jia Li

cs.CLApr 3, 2026

Evaluating the Formal Reasoning Capabilities of Large Language Models through Chomsky Hierarchy

Authors: Yihong Dong, Jianha Xiao, Xue Jiang, Xuyuan Guo, Zhiyuan Fan, Jiaru Qian, Kechi Zhang, Jia Li,

Organizations: Peking University, China · Wuhan University, China

Abstract

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.

Figures & tables

Figure 1. A conceptual comparison between existing benchmarks and our proposed benchmark.

Figure 2. Chomsky Hierarchy and ChomskyBench: Four computational complexity levels (Type-3 to Type-0) with corresponding automata models and representative formal languages used for systematic evaluation of LLM formal reasoning capabilities.

Dataset	Chomsky Level (Task Num)					Total	Question Focus	I/O Type
	RE	CS	NCF	DCF	Regular
NNCH ( Delétang et al., 2022 )	✘	✔	✘	✔	✔	15	Final state	One-hot Vectors
	0	7	0	4	4
FLaRe ( Butoi et al., 2024 )	✘	✔	✔	✔	✔	18	Final state	One-hot Vectors
	0	7	3	1	7
ChomskyBench (Ours)	✔	✔	✔	✔	✔	115	Process Trace + Final state	Natural Language

Table 1. Difference of ChomskyBench and previous formal language benchmark, where each task of ChomskyBench can change the structural complexity by modifying the input length of strings.

Figure 3. Construction Process of the ChomskyBench.

Figure 4. An Example in ChomskyBench.

Model	Closed Source / Open Source	Model Size	Training Tokens	API Price	Context Window	Data Cutoff
deepseek v3.1	Open	37B/ $\sim$ 671B	14.8T	$0.25/M In$ 1/M Out	128K	07/2024
gemini-2.5-pro	Closed	-	-	$1.25/M In$ 10/M Out	1M/64K	01/2025
gemini-2.5-flash	Closed	-	-	$0.3/M In$ 2.5/M Out	1M/64K	01/2025
gpt-5	Closed	-	-	$1.25/M In$ 10/M Out	272K/128K	09/2024
gpt-4o	Closed	-	-	$2.5/M In$ 10/M Out	128K	06/2024
kimi-k2	Open	32B/ $\sim$ 1T	15.5T	$0.38/M In$ 1.52/M Out	256K	06/2024

Table 2. Statistics of evaluated LLMs in our experiments.

LLMs	Regular		DCF		NCF		CS		RE		Avg
LLMs	Acc	PR	Acc	PR	Acc	PR	Acc	PR	Acc	PR	Acc	PR
Closed-source
o3	0.333	0.619	0.207	0.491	0.286	0.548	0.250	0.461	0.217	0.489	0.278	0.563
gpt-5	0.250	0.569	0.069	0.457	0.190	0.405	0.214	0.435	0.217	0.478	0.200	0.509
gemini-2.5-pro	0.250	0.500	0.103	0.500	0.286	0.524	0.143	0.310	0.087	0.424	0.183	0.486
gpt-4o	0.125	0.290	0.172	0.483	0.048	0.393	0.036	0.336	0.043	0.413	0.096	0.418

Table 3. Comparison of SOTA LLMs on automata and formal language tasks across different Chomsky hierarchy levels, which reports Accuracy (Acc) and PassRatio (PR) for both closed-source and open-source models, reflecting their comprehensive formal reasoning capabilities in regular, DCF, NCF, CS, and RE tasks.

Panel of Figure 5 — Figure 5. A multi-faceted visualization of SOTA LLMs for formal reasoning performance on ChomskyBench.

	Regular			DCF			NCF			CS			RE
	Time	$p_{e\&pr}$	$p_{l\&pr}$	Time	$p_{e\&pr}$	$p_{l\&pr}$	Time	$p_{e\&pr}$	$p_{l\&pr}$	Time	$p_{e\&pr}$	$p_{l\&pr}$	Time	$p_{e\&pr}$	$p_{l\&pr}$
Program	$<0.001$	-	-	$<0.001$	-	-	$<0.001$	-	-	$<0.001$	-	-	$<0.001$	-	-
Closed-source
o3	20.67	0.39	-0.34	26.41	0.10	-0.22	44.45	-0.62	-0.54	76.68	-0.06	-0.18	40.35	-0.31	-0.02
gpt-5	46.68	-0.23	-0.07	69.73	0.24	0.08	77.62	-0.30	-0.51	121.63	0.03	-0.34	66.53	-0.21	-0.33
gemini-2.5-pro	48.85	0.38	-0.09	54.49	-0.27	-0.23	58.76	-0.54	-0.60	105.44	-0.24	-0.44	74.50	-0.21	-0.48

Table 4. Comparison of Program Execution Time and LLM Reasoning Time, and their respective Pearson correlations with PassRatio, i.e.,

p_{e\&pr}

and

p_{l\&pr}

, respectively.

Approaches	Regular		DCF		NCF		CS		RE		Avg
Approaches	Acc	PR	Acc	PR	Acc	PR	Acc	PR	Acc	PR	Acc	PR
deepseek v3.1	0.058	0.225	0.183	0.505	0.219	0.533	0.091	0.407	0.095	0.437	0.125	0.419
Increasing sample size
Majority voting N=32	0.045	0.212	0.231	0.548	0.353	0.662	0.148	0.472	0.130	0.467	0.174	0.467
Best of N-Oracle N=2	0.075	0.296	0.244	0.569	0.311	0.628	0.149	0.509	0.138	0.500	0.178	0.498
Best of N-Oracle N=4	0.092	0.370	0.297	0.615	0.403	0.707	0.224	0.597	0.179	0.549	0.233	0.564

Table 5. Test-time Scaling of LLMs on ChomskyBench, including approaches of increasing sample size and extended reasoning length.

Model

Regular

DCF

NCF

Avg

Peak

deepseek v3.1

0.015

0.006

Table 6. Data Contamination Detection CDD ( Dong et al., 2024b ) , where Peak denotes the average peakedness of output distribution, and CR denotes the ratio of contaminated tasks. The lower value is better.

Model	Terminology (1-5)	Transition Rules (1-5)	Output Format (1-5)
gpt-4o	4.09	3.21	4.29
sonnet-4	4.09	3.53	4.52
gemini-2.5-pro	3.65	3.49	4.14
deepseek-v3.1	4.26	3.77	4.48
kimi-k2	4.30	3.83	4.29
llama-4-maverick	3.76	2.96	3.65

Table 7. LLM-as-Judge Analysis of Error Cases: Understanding vs. Execution, where higher value means understanding better.

LLM Evaluation

Large language model evaluation measures what models can do, how reliably they do it, and whether benchmark scores predict real-world performance.

See all 2,355 papers

Aug 20, 2026

FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models

Large language models (LLMs) have shown growing potential for automated theoretical computer science (TCS) research, yet existing benchmarks remain far from realistic research settings. We introduce \ourbenchmark, an expert-validated benchmark for evaluating LLMs on frontier, end-to-end TCS research. \ourbenchmark contains

143

instances drawn from papers accepted to STOC, FOCS, SODA, and COLT in 2025-2026, preserving paper-specific definitions, assumptions, and proof dependencies, with expert-verified Lean formalizations and proofs. Evaluations of leading LLMs reveal that current models remain far from reliably completing the full research pipeline. In particular, autoformalization is the sharpest bottleneck: the best model achieves only

11.5

on translating natural-language claims into formal theorem statements, compared with

28.6

Pass@8 when proving human-provided formal statements. Building on \ourbenchmark, we further develop an automated TCS research framework that generates, formalizes, filters, and proves new claims. Of

64

generated claims, only

6

ultimately pass expert evaluation and proof verification, indicating that beyond formalization, limited research taste remains another major barrier to autonomous TCS research.

Dingzirui Wang, Xuanliang Zhang, Keyan Xu +2

Harbin Institute of Technology

LLM Evaluation Automated Theorem Proving Autoformalization Large Language Model-Guided Scientific Discovery

Ask PDF

Apr 15, 2026

Empirical Evidence of Complexity-Induced Limits in Large Language Models on Finite Discrete State-Space Problems with Explicit Validity Constraints

Large Language Models (LLMs) are increasingly described as possessing strong reasoning capabilities, supported by high performance on mathematical, logical, and planning benchmarks. However, most existing evaluations rely on aggregate accuracy over fixed datasets, obscuring how reasoning behavior evolves as task complexity increases. In this work, we introduce a controlled benchmarking framework to systematically evaluate the robustness of reasoning in Large Reasoning Models (LRMs) under progressively increasing problem complexity. We construct a suite of nine classical reasoning tasks: Boolean Satisfiability, Cryptarithmetic, Graph Coloring, River Crossing, Tower of Hanoi, Water Jug, Checker Jumping, Sudoku, and Rubik's Cube, each parameterized to precisely control complexity while preserving underlying semantics. Using deterministic validators, we evaluate multiple open and proprietary LRMs across low, intermediate, and high complexity regimes, ensuring that only fully valid solutions are accepted. Our results reveal a consistent phase transition like behavior: models achieve high accuracy at low complexity but degrade sharply beyond task specific complexity thresholds. We formalize this phenomenon as reasoning collapse. Across tasks, we observe substantial accuracy declines, often exceeding 50%, accompanied by inconsistent reasoning traces, constraint violations, loss of state tracking, and confidently incorrect outputs. Increased reasoning length does not reliably improve correctness, and gains in one problem family do not generalize to others. These findings highlight the need for evaluation methodologies that move beyond static benchmarks and explicitly measure reasoning robustness under controlled complexity.

Md. Fahad Ullah Utsho, Mohd. Ruhul Ameen, Akif Islam +2

Department of Information and Communication Engineering, University of Rajshahi, Bangladesh · College of Engineering and Computer Sciences, Marshall University, Huntington, WV, USA · Department of Computer Science and Engineering, University of Rajshahi, Bangladesh

LLM Evaluation Large Reasoning Models Reasoning Consistency in Language Models Constraint Satisfaction

Ask PDF

Sep 17, 2026

PetriBench: Benchmarking LLM Reasoning over Dynamic State Spaces

Characterizing LLM reasoning remains an open challenge, as many existing benchmarks isolate specific reasoning skills, rely on external knowledge, or are costly to extend. We introduce PetriBench, a compact, fully self-contained, and scalable benchmark for evaluating LLM reasoning over dynamic state spaces using Petri nets, a mature formalism for modeling real-world concurrent and distributed systems. PetriBench organizes reasoning into four task families varying by scope and temporal horizon, with Easy, Medium, and Hard levels generated by increasing structural complexity and evaluated against exact ground truth. Across a diverse set of proprietary and open-weight models, accuracy decreases consistently with difficulty, while harder instances expose increasingly distinct task-specific capability profiles. Additional analyses show that test-time compute improves performance but interacts differently with different reasoning tasks, and that procedural generation yields smooth scaling with structural complexity. Together, these results show that PetriBench provides a unified and extensible setting for probing the strengths, limits, and scaling behavior of LLM reasoning.

Pyrros Koussios, Benjamin Jäger, John Hua Yao +3

ETH Zürich · Stanford University

LLM Evaluation Temporal Reasoning in Language Models

Ask PDF

Abstract

LLM Evaluation

Explore similar work

FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models

Empirical Evidence of Complexity-Induced Limits in Large Language Models on Finite Discrete State-Space Problems with Explicit Validity Constraints

PetriBench: Benchmarking LLM Reasoning over Dynamic State Spaces