Can AI Really Reason? Inside LogicAsker, the Framework Testing LLMs on Formal Logic

Large Language Models (LLMs) like GPT-4 and Llama 3 have become ubiquitous in our lives. They write poetry, generate code, summarize complex emails, and even crack jokes. When you interact with a chatbot that seems so articulate, it is natural to assume that there is a robust reasoning engine beneath the hood—a digital brain capable of connecting facts to draw logical conclusions.

But here lies a significant challenge in the field of Artificial Intelligence: Is the model actually reasoning, or is it just really good at pattern matching?

Consider a simple scenario: “Either it is raining, or Tom will play football. It is not raining. Therefore, Tom will play football.” This is a basic logical deduction. If an LLM answers this correctly, did it use logic? Or did it simply associate the words “not raining” with “play football” based on millions of similar sentences in its training data? And more importantly, if the model fails, how do we diagnose exactly which part of the logic broke down?

In this deep dive, we are exploring a research paper titled “LogicAsker: Evaluating and Improving the Logical Reasoning Ability of Large Language Models.” The researchers propose a novel framework designed to strip away the ambiguity of natural language and test LLMs on the fundamental “atomic” skills of formal logic. It acts essentially as a unit test for AI reasoning, revealing surprising gaps in even the most advanced models and offering a path to fix them.

The Problem: The Illusion of Competence

Evaluating reasoning in LLMs has historically been difficult. Traditional benchmarks often rely on downstream tasks—like solving math word problems or answering reading comprehension questions. While these are useful, they prioritize the final answer over the process. A model might arrive at the right answer for the wrong reasons, using “shortcuts” or heuristics (educated guesses) rather than strict logical derivation.

Furthermore, existing datasets often lack coverage. They might test simple implications (If A, then B), but miss more complex logical structures like equivalence (A is true if and only if B is true) or specific logical fallacies. Without a comprehensive diagnostic tool, we are flying blind regarding the reliability of these models in high-stakes reasoning scenarios.

Background: What is Formal Reasoning?

To understand how LogicAsker works, we first need to distinguish between informal and formal reasoning.

Informal reasoning relies on intuition, experience, and common sense. For example: “The streets are wet, so it probably rained.” This is inductive and open-ended.

Formal reasoning, which is the focus of this research, is a systematic process. It follows strict rules where, if the premises are true and the rules are followed, the conclusion must be true. The researchers focus on two fundamental systems:

1. Propositional Logic: Deals with simple statements (propositions) connected by operators like AND (\(\land\)), OR (\(\lor\)), NOT (\(\neg\)), and IMPLIES (\(\rightarrow\)).
2. Predicate Logic: Extends propositional logic to include variables and quantifiers. It deals with statements involving “For all \(x\)” (\(\forall x\)) or “There exists an \(x\)” (\(\exists x\)).

For an LLM to be a robust reasoner, it must master the specific rules—or “laws”—that govern these systems.

Table 7: Examples of atomic laws in propositional logic. These represent the fundamental “rules of the road” for logical equivalence.

As shown in the table above, rules like “DeMorgan’s laws” or “Contraposition” are non-negotiable in logic. If an LLM cannot reliably apply these atomic rules, its reasoning foundation is shaky.

LogicAsker: The Methodology

The core contribution of this paper is LogicAsker, an automated framework that generates test cases based on these formal rules. Think of it as a teacher generating an infinite number of unique quizzes, each designed to test a specific logical concept.

1. Defining Atomic Skills

The researchers identified 34 atomic rules from propositional and predicate logic (such as Modus Ponens, Modus Tollens, and Constructive Dilemma). They then expanded these into 208 extended skills by combining them with different logical operators and quantifiers. This creates a “skill tree” covering the entire spectrum of formal reasoning.

Figure 1: The LogicAsker workflow. It begins by defining atomic skills (left), generating test cases (center), evaluating models to find weaknesses, and finally using those findings to improve the models (right).

2. Generating Test Cases

How do you create a test that measures pure logic without allowing the model to cheat using common sense? LogicAsker uses a clever pipeline:

1. Logic Expression Generation: The system first generates a symbolic logic expression based on a specific rule (e.g., \(P \rightarrow Q, P \vdash Q\)).
2. Natural Language Translation: It translates these symbols into grammatically correct English sentences using templates. It uses a diverse vocabulary of subjects (e.g., “Alice”, “The Doctor”) and predicates (e.g., “is happy”, “plays tennis”) to ensure the model isn’t biased by specific words.
3. Creating Falsehoods: To ensure the model isn’t just guessing “Yes,” LogicAsker generates “negative” samples. It creates conclusions that are Contradictions (directly opposite to the logic) or Unrelated (irrelevant to the premises).

Figure 2: An example of generating a test case. A formal logic chain is synthesized and then translated into a story about Alice reading and Bob cooking. Crucially, the system also generates false conclusions (Contradiction and Unrelated) to rigorously test the model.

This rigorous generation process allows LogicAsker to adopt a Minimum Functionality Test (MFT) approach. Much like unit testing in software engineering, MFTs test small, isolated behaviors. If a model fails an MFT for “Modus Ponens,” we know exactly what is broken.

Experiments & Results: exposing the Gaps

The researchers tested LogicAsker on six major LLMs, including GPT-4, GPT-4o, Gemini, Llama 3, and Mixtral. The results were revealing, showing that even the most powerful models have significant blind spots.

Overall Accuracy vs. Weaknesses

When tested generally, models performed reasonably well. However, when LogicAsker zoomed in on the specific areas identified as “weaknesses” for each model, the performance dropped precipitously.

Figure 3: The gap between general performance (Blue) and performance on identified weaknesses (Red) is striking. For example, while GPT-4o has a general accuracy of 92%, its accuracy on its specific weak points drops to 35%.

This graph highlights a critical insight: an aggregate score on a benchmark can hide deep logical flaws. A model might be 90% accurate overall because it is excellent at simple logic, but it might be 0% accurate on specific complex rules.

Propositional vs. Predicate Logic

The study found a clear hierarchy in difficulty. Models consistently performed better on Propositional Logic (simple statements) than on Predicate Logic (complex statements with quantifiers like “All” or “Some”).

Figure 4: Across all models, accuracy on Propositional logic (Blue) is higher than Predicate logic (Red). This suggests that LLMs struggle to internalize the complex relationships involved in universal and existential quantifiers.

The Failure of Fallacy Recognition

Perhaps the most concerning result was the models’ ability—or lack thereof—to recognize logical fallacies. Fallacies are arguments that sound correct but are logically invalid (e.g., “If it rains, the street is wet. The street is wet, therefore it rained.” This is invalid because the street could be wet from a hose).

Figure 5: While models are decent at Equivalence and Inference, many struggle with Fallacy recognition. Note the performance of Llama3 and ChatGPT in the ‘Fallacy’ category compared to the others.

The data shows that LLMs are often “overconfident.” They tend to agree with a conclusion that sounds plausible, even if it doesn’t logically follow from the premises. This susceptibility to fallacies mimics human cognitive biases, but in an AI system designed for reasoning, it is a significant defect.

A Case Study: GPT-4’s Blind Spots

Even GPT-4, arguably the strongest model tested, showed specific atomic failures.

Table 3 (Top): Specific rules where GPT-4 struggles. For instance, it only achieved 60% accuracy on “Existential resolution,” a specific type of predicate logic inference.

This granular level of detail is what makes LogicAsker valuable. Instead of just knowing “GPT-4 failed the test,” we know “GPT-4 struggles with the Law of Quantifier Movement.”

Improving LLMs: Turning Failure into Success

LogicAsker isn’t just a grading tool; it’s a tutor. The researchers utilized the identified weaknesses to improve the models. They employed two primary strategies:

1. In-Context Learning (ICL) Demonstrations

By knowing exactly which rules a model struggles with, the researchers constructed specific prompts that included examples of those rules being applied correctly. They also included “explanations” in the prompt to guide the model’s reasoning.

Table 5: The results of using LogicAsker-generated prompts. “ICL (Weak)” refers to demonstrations targeting the model’s specific weaknesses. Notice the jump in performance for GPT-4o (91.92% \(\rightarrow\) 97.23%).

2. Fine-Tuning

For models that allow re-training (like open-source models or via APIs), the researchers created a dataset of LogicAsker problems to fine-tune the model.

Table 6: Fine-tuning ChatGPT on LogicAsker data not only solved the logic problems (jumping from 77% to 99%) but also slightly improved performance on an external benchmark, LogiQA, demonstrating that the model actually learned to reason better, rather than just memorizing the test.

The Chain-of-Thought Anomaly

One of the most interesting discussions in the paper revolves to Chain-of-Thought (CoT) prompting. CoT is a popular technique where you ask the LLM to “think step-by-step.” Usually, this improves performance.

However, in the context of LogicAsker, CoT sometimes hurt performance.

Why? Because CoT encourages the model to use natural language reasoning, which often brings in “common sense” or external knowledge. In formal logic, external knowledge is forbidden; you must reason only based on the provided premises.

For example, if the premise is “If Linda is sad, it is sunny,” and “It is sunny,” strict logic says we cannot infer that Linda is sad (this is the fallacy of affirming the consequent). However, a model using CoT might hallucinate a connection based on weather and mood patterns, talking itself into a wrong answer. This highlights that for strict formal reasoning, the concise, rule-based approach is often superior to verbose “thinking.”

Conclusion and Implications

The LogicAsker framework provides a sobering but optimistic look at the state of AI reasoning. It reveals that while LLMs are incredibly capable, their grasp of formal logic is brittle and inconsistent. They are prone to fallacies and struggle with complex quantification.

However, the paper also demonstrates that these are solvable problems. By systematically identifying atomic weaknesses and targeting them with specific training data and prompts, we can patch the holes in the “digital brain.”

As we move toward agents that execute code, verify contracts, or conduct scientific research, formal reasoning capabilities will be non-negotiable. Tools like LogicAsker act as the essential stress tests to ensure that when an AI says “Therefore…”, it actually knows what it’s talking about.