QMFOL: Benchmarking Large Language Model Reasoning via Quantifiable Monadic First-Order Logic Test Case Generation

As Large Language Models (LLMs) and Large Reasoning Models (LRMs) continue to advance, existing benchmarks often struggle to balance semantic diversity with rigorous logical control. The authors seek to address this by developing a scalable, automated framework that allows for fine-grained manipulation of logical complexity, enabling a more precise evaluation of deductive reasoning capabilities.

The authors propose QMFOL, a framework that constructs formal logical structures using Monadic First-Order Logic (MFOL). By utilizing conjunction and disjunction patterns, the framework allows researchers to explicitly configure reasoning depth, width, label types (True, False, Unknown), and the number of distractor rules.

To bridge the gap between formal logic and natural language, QMFOL employs an LLM-based translation process. To ensure the generated natural language remains logically consistent with the underlying formal structure, the framework uses a round-trip verification process: the generated text is translated back into formal logic and validated against an external theorem prover. This process repeats until the generated task is logically sound.

Using this framework, the authors constructed QMFOLBench, a dataset of 2,880 instances across 960 distinct configurations. Evaluations of six LRMs and two LLMs yielded several key insights:

• Complexity Sensitivity: Model accuracy consistently drops and computational overhead increases as the logical depth and width of the tasks grow.
• Label Bias: Models generally perform better on tasks labeled as 'True' compared to those labeled 'False' or 'Unknown', suggesting a potential bias in how models handle different logical outcomes.
• Distractor Impact: The inclusion of distractor rules significantly hampers performance, though more advanced models show greater robustness to these irrelevant premises.
• Semantic Dependence: Even when logical structures are identical, model performance varies across different topic domains (e.g., Food, Animals, University, Mathematics), indicating that semantic context influences reasoning reliability.