One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs

Response to Reviewer tdTp

Thank you for your efforts in the review, and hope our response will address your concerns!

Supported by out-of-distribution (OOD) evaluations, but additional benchmarks from formal theorem proving could further validate this claim.

To further validate our approach, we expanded our evaluation to include higher-difficulty datasets at the competition level (OlympiadBench-Math, AIME 2024) and university level (MMLU-College-Math). The accuracy results are summarized below:

These results show significant improvements on both simpler and more complex OOD datasets, supporting our hypothesis that current LLMs lack the ability to effectively leverage counterexamples for mathematical reasoning.

While the results indicate that counterexample-based reasoning is crucial, the experiments lack an ablation study comparing different types of proof strategies (e.g., direct proof, proof by contradiction, proof by construction). Including such an analysis could strengthen the claim that counterexample-driven reasoning is uniquely impactful.

We appreciate this insightful suggestion. In our work, we conducted a preliminary analysis using different prompting strategies (CoT, ICL, and Hint) to assess their impact on example generation. Due to space limitations, we provided only a brief overview. We plan to conduct a more detailed ablation study in future work and hope our current analysis will encourage further research in this area.

Have you considered applying COUNTERMATH to a Lean-based proof assistant (or Isabelle, Coq, etc.) to test whether counterexample-driven learning aids in formal symbolic reasoning?

Our decision not to use formal tools stems from a mismatch with COUNTERMATH’s natural language rationale annotations. Formal data generated by automated tools rely heavily on autoformalization models—which currently show inconsistent performance on datasets like GSM8K and MATH. However, we agree that exploring formal generation of counterexamples is a promising direction for future research.

How does the model perform on longer proofs (like theorems in research-level math papers) that require lots of counterexamples? Is reasoning depth a bottleneck?

Our benchmark is derived from university-level mathematics textbooks, covering key definitions, theorems, properties, and axioms. In many cases, the model incrementally builds its reasoning by adding constraints and refining assumptions. While this demonstrates some reasoning depth, research-level theorems—requiring extensive counterexamples and multi-step proofs—pose a significant challenge. We hypothesize that tackling such complex proofs requires the LLM to possess multiple capabilities, and reasoning depth does emerge as a bottleneck for LLMs in these scenarios.

Moreover, as seen in models like o1 and Deepseek-R1, an excessively prolonged reasoning process can lead to a phenomenon where the model "overthinks" and becomes trapped in a loop of iterative self-correction. This results in reasoning fallacies, where the model repeatedly attempts to refine its initial claim but ultimately diverges further from a correct solution. We encountered this specific issue during our evaluation of Deepseek-R1 on the COUNTERMATH benchmark, resulting in more than 500s thinking time per question.

Addressing these research-level reasoning challenges requires a multi-faceted approach. Further model optimization like SFT and Reinforcement Learning can improve the model’s understanding of mathematical concepts, its proficiency in using formal languages for structured reasoning, and its ability to generate logically consistent counterexamples. We believe that continued advancements in these areas will significantly enhance LLMs' performance on complex mathematical proofs.

Thank you once again for your valuable question, which really encourage us to further improve our research.

Response to Reviewer vkWZ

Claim (2) has weak experimental evidence: only one model fine-tuned, evaluated on two math benchmarks.

Our primary goal is to introduce a benchmark and explore LLMs’ math capability in providing counterexamples. We observed that even state-of-the-art LLMs struggle with this task. Therefore, we fine-tune the typical model, Qwen2.5-Math-Instruct, to enhance its counterexample reasoning abilities. To strengthen our claim, we expanded our evaluation to more challenging datasets, including Competition-level (OlympiadBench-Math, AIME 2024) and University-level (MMLU-College-Math).

These results demonstrate significant improvements on both simpler and complex datasets, supporting our hypothesis that learning from counterexamples enhances performance.

Concern about "Hint prompt".

We observe that directly prompting LLMs for true/false judgments led to poor performance and random guessing. Therefore, we hope to use the Hint prompt to inspire LLMs to "give examples", instead of assuming the truth. It guides LLM to prove in a more reasonable way of thinking, which aims to let the model reason by giving examples.

Code documentation and dataset quality.

Thank you for your meticulous review. Regarding the second statement you mentioned, we classify True/False based on the existence of examples: False if no such examples exist, and True if at least one example exists, and framing these with binary labels enables more efficient evaluation. As for dataset quality, COUNTERMATH was initially from textbooks and verified by experts to ensure all statement-rationale pairs are unambiguous and reasonably categorizable, as detailed in Sections 3.1, 3.2, and the Appendix.

Lack of benchmark disclosure for quality assessment.

Sorry for only providing the sampled dataset during the anonymous period. The main reason is that we plan to set up a public Leaderboard, so it is not appropriate to disclose all data. In addition, providing sampled datasets during the anonymous review stage does not violate any rules (in fact, this is a common practice, which can protect from being leaked prematurely and facilitate reviewers to review samples).

Writing clarity issues.

We apologize for any confusion, and we will ensure clearer phrasing in the final version. Key clarifications:

• "Conceptual Finetuning" refers to fine-tuning on annotated, complex reasoning data.
• "Statement is True or False by its rationale" means determining validity based on supporting reasoning.

Claim that counterexample-based reasoning is more important is unjustified.

Sorry for the confusion caused here. We aim to emphasize that drill-based learning alone is insufficient for developing deep mathematical understanding, and fostering deeper mathematical understanding. While drills transfer knowledge, counterexample-based reasoning enhances problem-solving and concept validation. We appreciate your observation and will revise Line 51 to avoid overclaims.

higher F1 but lower Examples (%)

1. Sometimes the judgment is correct, but the reasoning process is not rigorous.

Example 1:

• Statement: The smallest number ring containing $\sqrt{3}$ is the real number ring.
• Answer: False
• Model Prediction: False (Correct)
• Model Output: Incorrectly discusses Banach spaces and the RNP instead of relevant number theory concepts.
• Explanation: The model guessed the correct answer but provided an irrelevant rationale, resulting in a correct judgment but a poor Examples score.

2. Constructing effective counterexamples requires a comprehensive master of mathematical knowledge.

Example 2:

• Statement: All countably compact spaces are compact.
• Model Output: Proposes an invalid counterexample based on Hilbert cube subsets.
• Explanation: The Hilbert cube itself is compact, and its closed subsets inherit compactness. Thus, this counterexample is self-defeating.

Inspection of model-generated counterexamples.

Here is an LLM-generated counterexample:

• Statement: For a fixed element $a$ of the ring $R$, $N = \{ra \mid r \in R\}$ forms an ideal of $R$ but does not necessarily contain $a$.
• Reference Example: $R$ as the ring of even numbers; $N = \{r \cdot 4 \mid r \in R\}$ is an ideal, but $4 \notin N$.
• LLM Output: The model analyzed a trivial ring $R = \{0\}$ where the counterexample was consistent with evaluation criteria.

The LLM’s counterexample differs from the reference but is marked as "consistent" because it satisfies the evaluation criteria. Our judge model successfully extracts and assesses these counterexamples, determining their consistency with the intended logic.

"statement": "Examples where the $n(n \\geqslant 3)$-ary associative law does not hold",

Please reason by giving examples about whether the above statement is True or False.

Response to Reviewer bVLs

We sincerely appreciate your efforts in the review and hope our response will address your concerns.

Did the authors look at EN-based textbooks for such proofs?

Yes. While our annotators are native Chinese speakers and thus did not annotate directly from English textbooks, our core authors aligned the English version of COUNTERMATH with standard EN-based textbooks during quality control. Additionally, many counterexamples in our Chinese sources originate from English works like Counter-Examples in Topology (Steen & Seebach) and Counterexamples in Topological Vector Spaces (Khaleelulla). We are confident that our dataset maintains cross-language representativeness.

Did the authors consider generating a counterexample-based dataset using formal tools?

We chose not to use formal tools because the resulting data would conflict with the natural language rationale annotations in COUNTERMATH. Using formal tools risks misalignment between generated counterexamples and the human-provided explanations, and their quality depends heavily on the autoformalization model—which, given current performance on datasets like GSM8K and MATH, remains inconsistent. However, we agree that formal generation of counterexamples is an intriguing direction for future work.

It was not clear if the authors considered simpler problems that can be solved with examples, which would be more amenable to formal provers (e.g., SAT/SMT encodable instances).

We have indeed considered simpler math datasets such as GSM8K and MATH. Our experimental results (Table 3) show that counterexample-driven reasoning yields significant improvements on these elementary math scenarios—demonstrating that even 7B-scale models can outperform 72B-scale models when leveraging examples effectively.

Do you think that using RL instead of standard SFT training would yield better results?

We share your view on the potential of RL. Unfortunately, our current GPU resources (only 2 L20 48G GPUs) limited our ability to conduct effective RL experiments for LLMs. Moreover, our primary goal was to emphasize counterexample-driven reasoning and introduce COUNTERMATH. We believe that further exploration—including RL-based training—remains a promising direction for future research.

It would have been nice to see a bit more of an evaluation of where the models fail, e.g., due to reasoning errors, miscalculations, or deeper issues?

This is a very interesting and important research direction. We did attempt to evaluate the reasoning process of the model in order to identify the precise step where errors begin. However, the complexity of the prompts led to instability in the output of the judge model. For example:

Statement: There exists a divergent series, which can be rearranged to arbitrarily slow down its divergence. Model Output: Correct understanding of divergent series, but mistakenly applies properties of conditionally convergent series. "First, let's recall that a divergent series is a series whose sequence of partial sums does not converge to a finite limit...it is possible to construct a divergent series whose divergence can be arbitrarily slowed down by rearranging its terms... Therefore, it is indeed possible to rearrange a divergent series..."

Human Judgment: False
LLM Judgment: True

Given these inconsistencies, we used the Example evaluation approach. Future research will explore stepwise error analysis, like using reward models to more systematically analyze the causes of the model's failures.

Provide an end-to-end example to clarify benchmark components and model performance.

We appreciate the reviewer’s suggestion and have refined the examples to better illustrate our benchmark’s utility and model performance, highlighting model successes and failures:

Example 1

• Statement: "The smallest number ring containing $\sqrt{3}$ is the real number ring."
• Answer: False
• Model Prediction: False (Correct)
• Model Output: "To determine whether $L^{p}[0,1]$ and $l^{p}$ are linearly isomorphic for $p \neq 2$..."
• Correct Rationale: "The minimal ring containing $\sqrt{3}$ is $\mathbb{Z}[\sqrt{3}]$."
• Model Issue: The model correctly answered "False" but hallucinated irrelevant concepts (e.g., Banach spaces) unrelated to ring theory.

Example 2

• Statement: "There exist rings without identity elements, and there are cases with left or right identity but not both."
• Answer: True
• Model Prediction: False (Incorrect)
• Model Output: "We aim to determine whether there exists a bilinear functional $\varphi(x, y)$..."
• Correct Rationale: "A finite 4-element ring can have left identities without right identities."
• Model Issue: The model entirely misinterpreted the problem type, discussing bilinear functionals instead of ring-theoretic identities.

Response to Reviewer KrNF

No comparison with model fine-tuned on dataset of non-counterexample-based math proofs.

We agree that such a comparison would further validate our approach. Since our primary motivation was to explore how LLMs use counterexamples in proofs, we initially evaluated only counterexample-based fine-tuning. To address your suggestion, we randomly selected 1,025 non-counterexample samples from the NaturalProofs dataset (the same source as our counterexample data) and fine-tuned Qwen2.5-Math-Instruct under identical settings. Results are as follows:

The superior performance of counterexample-based models supports our claim that improvements stem from learning counterexamples rather than increased exposure to advanced data.

The current evaluation prompt may overly penalize valid and mathematically sound counterexamples.

Our evaluation prioritizes whether generated examples lead to the same final conclusion as the reference. While the examples need not match exactly, they are marked as “consistent” if they function equivalently in proving the statement.

Concerns about GPT-4o's evaluation.

Given the current challenges of human annotation in terms of cost and efficiency, our approach aligns with prior works about GPT-4o evaluation (e.g., DPO[1], SimPO[2]) and established benchmarks like MT-Bench[3] and Alpaca-Eval[4]. To enhance accuracy, we provided reference information for GPT-4o and our human-validated results further confirm the approach's reliability.

[1] Direct Preference Optimization: NeurIPS 2023
[2] SimPO: Simple Preference Optimization: NeurIPS 2024
[3] MT-Bench: NeurIPS 2023
[4] AlpacaEval-LC: COLM 2024

Concerns about the generalizability of SFT model to more challenging OOD datasets.

We extended evaluations to competition-level (OlympiadBench-Math, AIME 2024) and college-level (MMLU-College-Math) datasets:

Our SFT model shows significant improvements across both simpler and more complex OOD datasets, supporting our hypothesis that learning from counterexamples enhances performance over a range of difficulty levels.

Lack of training details.

We apologize for the oversight. our training used Qwen2.5-Math-Instruct on two L20 48G GPUs with LoRA (rank 16). The learning rate was 1.0e-4 for one epoch. Full details will be clarified in the final version.

Suggestion to add performance of o1 model on simpler benchmarks.

Below is a comparison using official o1-preview results (due to resource constraints):

The gap between COUNTERMATH and simpler benchmarks underscores the challenge of counterexample-based reasoning.

Hint prompt evaluations limited to Qwen2.5-Math-7B-Instruct.

We have also tested the Hint prompt with the Deepseek-Math-7B-rl model. Although space constraints prevented us from including these results in the paper, the summary is as follows:

The Hint prompt notably increases the "Examples (%)" metric, demonstrating its positive impact on example generation. Due to consistent trends observed between Qwen2.5-Math-7B-Instruct and Deepseek-Math-7B-rl, we limited further evaluations to these two models.

Evaluation "consistency" of examples when facing multiple examples.

A generated example is considered "consistent" if it effectively serves as a valid proof for the statement—matching the intended meaning and function of at least one reference example. So even if the example is different from the ones we provided, it’s still considered consistent as long as it has the same meaning.

Clarification on Table 3 metrics.

We apologize for the confusion. The values represent accuracy, not F1 scores. This will be clarified in the final version.

Response to Reviewer H7Ry

Thank you for your efforts in the review, and hope our response will address your concerns.

On Line 200-202, Evaluation Metrics. "We use lexical matching such as F1 to match the judgments of the statements." What is lexical matching? Also, how exactly is F1 calculated here?

We apologize for the ambiguity. "Lexical matching" refers to extracting the model's final judgment (True or False) using regular expressions. Specifically, we parse the model's output to identify the final decision and map "False," "True," and empty responses to numerical values (0, 1, and 2, respectively). The F1-score is then computed as a macro-averaged multiclass F1, where each class's F1-score is calculated as: F1 = 2 * (precision * recall) / (precision + recall). We implement this using the evaluate library's F1 function, treating the empty response as a separate class. The final reported score is the macro-averaged F1 across all classes.

Why are strict and loose align meaningful metrics to evaluate? I imagine there could exist many valid counterexamples for a given statement. Both strict and loose align seem to suggest that the model should really provide counterexamples given by textbooks. Is this too restrictive?

Our evaluation aims to assess whether the model can generate examples that support its reasoning. During evaluation, we use GPT-4o to verify whether the model-generated examples lead to the same final conclusion as reference examples. This approach allows for flexibility: the generated examples do not need to match the reference ones exactly but should be logically consistent in leading to the conclusion. Thus, our metric captures the model’s reasoning ability rather than enforcing rigid textbook-style counterexamples.

Can the authors provide more details on which subject or what type of questions the SFT model improves the most on MATH?

We conduct a case study on 50 instances where the base model failed but the SFT model succeeded. Since the MATH dataset lacks explicit problem type annotations, we manually annotate and categorize them. The most significant improvements are observed in:

1. Geometry: Problems requiring length and area calculations. The base model struggles with triangle proportions and spatial reasoning.
2. Number Theory: Tasks like repeating decimal periods and divisibility checks, where errors stem from incorrect cyclic period calculations or overlooked edge cases.
3. Algebra: Problems involving averages, fractions, and arithmetic, where the base model frequently miscalculates.

The SFT model demonstrates a better understanding of mathematical concepts, more effective application of formulas, and improves accuracy in calculations. Here is an example:

Question: Sallie earned a grade of exactly 90% based on six equally weighted tests. The four test papers she found have grades of 83%, 96%, 81%, and 82%. What is the sum of the two missing grades?
Correct Answer: 198

• Base Model: Predicted 208
  • Step: $\frac{83 + 96 + 81 + 82 + x + y}{6} = 90$ → $342 + x + y = 540$
  • Error: Miscomputed $540 - 342 = 208$ (correct value is 198).
• SFT Model: Predicted 198
  • Step: Same, but correctly computed $540 - 342 = 198$.