Pith. sign in

REVIEW 4 major objections 6 minor 60 references

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

T0 review · 4 major / 6 minor · reviewed 2026-08-08 · deepseek-v4-flash

Pith's one-line read The paper claims that counterexample-driven training improves general mathematical reasoning in LLMs, and that a small fine-tune on such examples transfers to out-of-distribution benchmarks.

desk verdict Useful new counterexample benchmark, but the training claim needs a control SFT before it's taken seriously. read the letter →

arxiv 2502.10454 v2 pith:IG2AACFU submitted 2025-02-12 cs.LG cs.AIcs.CL

classification cs.LGcs.AIcs.CL
keywords counterexamplereasoningmathematicalLLMsconceptualbenchmarksupervisedfine-tuningout-of-distributiongeneralizationproofbyuniversity-levelmathematics
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper argues that today's mathematical LLMs are trained by drill: they solve many similar problems and imitate familiar proof patterns, which leaves them weak at the kind of conceptual understanding mathematicians exercise when they disprove a statement by finding one telling counterexample. To test this, it builds CounterMATH, a set of 1,216 university-level statement-rationale pairs drawn from counterexample textbooks in algebra, topology, real analysis, and functional analysis, and shows that even strong commercial models often fail to judge the statements correctly or to produce a valid counterexample. The central proposal is that counterexample-driven reasoning can be taught cheaply: fine-tuning Qwen2.5-Math-7B on 1,025 filtered and rewritten counterexample proofs improves its F1 on CounterMATH and raises its scores on out-of-distribution benchmarks such as MATH and AIME. If the claim holds, a small, concept-focused dataset is a high-leverage intervention for math reasoning, and counterexample-based tasks deserve a place in LLM training and evaluation.

What carries the argument

The load-bearing object is the counterexample as a reasoning unit: a single, well-chosen example that refutes a general statement and thereby tests whether a model distinguishes the concepts involved. Around this unit the paper builds two instruments: CounterMATH, a 1,216-item benchmark of statement-rationale pairs manually extracted from counterexample textbooks, and a data engineering pipeline that filters over 30,000 human-written proofs (ProofNet, NaturalProofs) with GPT-4o under three loose criteria, then refines the surviving 1,025 rationales to match CounterMATH's concise, example-centered distribution. The benchmark supplies the evaluation signal; the pipeline supplies the training signal; the fine-tuned model is the mechanism that connects them.

What would settle it

Fine-tune Qwen2.5-Math-7B-Instruct on 1,025 ordinary proof rationales of matched length, field distribution, and quality, for example random ProofNet proofs that GPT-4o judged not to use counterexamples, then evaluate on MATH and AIME; if the control matches the reported gains, the counterexample content is not the active ingredient.

Watch

Extended reading notes

Core claim

The central discovery claimed is that counterexample-based reasoning is learnable from a small curated set and that learning it transfers beyond the target task. Concretely, the authors report that their fine-tuned Qwen2.5-Math-7B-Instruct, trained on 1,025 samples, reaches an F1 of 39.7 on CounterMATH (up from 38.3 baseline) and with a hint prompt 41.1, while on OOD benchmarks it improves GSM8K from 95.1 to 95.6, MATH from 80.5 to 87.9, MMLU-college-math from 74.0 to 80.0, and AIME 2024 from 20.0 to 30.0, the last two surpassing the 72B model. The paper reads these gains as evidence that drill-based training alone is insufficient and that example-based conceptual reasoning has general significance for mathematical reasoning. It also documents that current LLMs, including o1-preview, perform far worse on CounterMATH than on standard math benchmarks, with topology and real analysis the hardest fields.

Load-bearing premise

The claim that counterexample content causes the general math gains rests on comparing the fine-tuned model against the base model; the paper never fine-tunes the same base model on equally many ordinary proofs, so any benefit from additional high-quality supervised fine-tuning could be driving the improvement.

Editorial extensions

If this is right

  • Fine-tuning on a thousand counterexample-style proofs can improve general math benchmarks, not just the target task.
  • Open-weight math LLMs trained mainly by drill score around 30 F1 on CounterMATH, indicating a measurable gap in conceptual reasoning.
  • Topology and real analysis are the weakest fields, suggesting where future math LLM training data is missing.
  • Explicit hint prompts to reason by example give only small gains, implying the ability must be trained rather than prompted.
  • Reinforcement-learning-trained models such as Deepseek-R1 achieve the highest judgement F1, hinting that RL may already induce some counterexample reasoning.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The reported OOD gains could in principle come from any additional proof-level supervised fine-tuning; the paper does not run a control fine-tune on equally sized non-counterexample proofs, so a testable extension is to compare such a control.
  • CounterMATH's True:False ratio (87.8% True) and the authors' modification of under 5% of statements to be False mean the benchmark mostly measures whether a model can justify a true statement with an example, not just refute false ones; a balanced refutation-focused subset might behave differently.
  • The data engineering pipeline could be reused to build counterexample curricula in other quantitative domains, such as physics or statistics, where a single counterexample also settles a universally quantified claim.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 6 minor

Summary. The paper introduces CounterMATH, a benchmark of 1,216 university-level statement-rationale pairs drawn from Chinese textbooks on counterexamples in algebra, topology, real analysis, and functional analysis. The authors evaluate a broad set of LLMs on the benchmark, finding low performance even for strong proprietary models, and they then propose a data-engineering pipeline that filters 1,025 samples from ProofNet and NaturalProofs, refines their rationales with GPT-4o, and fine-tunes Qwen2.5-Math-7B-Instruct with LoRA. The paper reports a small F1 gain on CounterMATH (38.3 to 39.7) and larger gains on OOD benchmarks such as MATH (80.5 to 87.9) and AIME 2024 (20.0 to 30.0), and it concludes that counterexample-driven training improves general mathematical reasoning.

Significance. If the central training claim were established, the paper would be significant: it would show that a small, carefully curated set of counterexample-style SFT samples can produce broad mathematical gains, a high-leverage and inexpensive intervention. The benchmark itself is a useful contribution: the construction is described in detail, with two-stage annotation, expert validation, a 95.4% retention rate, and a 100-sample human check of the automatic judge that reports 97% extraction accuracy and 93.5% alignment accuracy. The evaluation of many open-weight and proprietary models gives a valuable picture of current counterexample reasoning. However, the causal claim about counterexample-specific training is not yet supported: the experiments lack a control SFT condition, the data filter is too loose to isolate counterexample content, the refinement step aligns training data to the test distribution, and no error bars or multiple seeds are reported. These issues are load-bearing for the paper's headline conclusion, so the training portion needs substantial revision even though the benchmark portion is sound.

major comments (4)
  1. [§5.2, Table 3] The central claim that counterexample-driven SFT improves general mathematical reasoning is not supported because there is no control condition. The OOD gains (MATH 80.5→87.9, AIME 2024 20.0→30.0) could be produced by any additional proof-level SFT, by format alignment introduced by the refinement step, or by LoRA fine-tuning itself. The authors should fine-tune the same base model on an equal-sized, quality-matched set of mathematical proofs that do not emphasize counterexamples (e.g., ordinary ProofNet/NaturalProofs rationales with the same length and refinement pipeline) and compare all OOD metrics. They should also report multiple seeds and per-problem breakdowns for AIME 2024, since a +10-point swing on 30 problems is only three additional correct answers.
  2. [§5.1, Appendix C] The data filter is too loose to isolate counterexample reasoning. As stated in Section 5.1 and Appendix C, data are retained if any one of three criteria is met, and Criterion 1 is proof by contradiction while Criterion 3 is specially chosen cases; only Criterion 2 is a genuine counterexample. Thus the 1,025 training samples are not verified to be counterexample-driven, and the treatment mixes counterexample content with ordinary contradiction proofs and special-case arguments. To support the mechanism, the authors should report the distribution of criteria satisfied across the 1,025 samples and ideally run an ablation training only on samples that satisfy Criterion 2 (or only Criterion 1, or only Criterion 3) and compare OOD performance.
  3. [§5.1] The refinement step aligns the training distribution to CounterMATH by construction: one reference example from each CounterMATH field is used to rewrite the SFT rationales. This means the CounterMATH F1 improvement in Table 2 is partly attributable to training distribution overlap rather than to a learned counterexample ability. The OOD results provide some independent grounding, but they inherit the control problem raised above. To address this, the authors should either evaluate on a held-out counterexample benchmark that was not used in refinement, or ablate the refinement step by training on unfiltered or unrefined data and comparing OOD gains.
  4. [§5.2, Table 2] The reported gains on CounterMATH are small and appear to be within plausible noise: SFT improves F1 from 38.3 to 39.7, while the hint prompt alone gives 39.4 and SFT+Hint gives 41.1. Given that LoRA fine-tuning is stochastic and no error bars or multiple seeds are reported, a +1.4 F1 difference is not sufficient evidence of improvement on the target benchmark. The authors should run at least three seeds and report mean and standard deviation for F1, Examples, Strict, and Loose metrics, and perform a significance test or confidence-interval comparison.
minor comments (6)
  1. [§5.2, Table 3] The benchmark name is misspelled as 'OlympaidBench' in the table and text; it should be 'OlympiadBench'.
  2. [Throughout] The benchmark name is written inconsistently as COUNTERMATH, COUNTER MATH, and CounterMATH; please unify the notation (e.g., CounterMATH) throughout the manuscript.
  3. [Figure 1] The caption and figure contain the typo 'Principia athematica' and the phrase 'proving by examples' should be 'proof by examples' or 'proving with examples'.
  4. [§5.2] The hardware description '2 ×L20 48GB GPUs' is ambiguous; it should read '2× L20 48GB GPUs' or 'two L20 48GB GPUs'.
  5. [Appendix B, Evaluation Prompt] The evaluation prompt repeatedly refers to 'proof by contradiction' and asks the judge to focus on 'counterexamples used within the proof by contradiction,' which is conceptually inconsistent with the benchmark's counterexample framing; the prompt should be reworded to evaluate counterexample reasoning directly.
  6. [Figure 6] The axis label 'Mean Token Ratios (%)' is not fully defined in the caption; the caption should state that the ratio is model-generated tokens divided by ground-truth tokens and explain how the 100% reference line is computed.

Circularity Check

1 steps flagged · score 4.0 of 10

Example-alignment metrics are partially self-referential: the SFT refinement injects CounterMATH reference examples that the Strict/Loose rubric then rewards; F1 and OOD results remain non-circular.

  1. self definitional [Section 5.1 (Training Data Refinement); Section 4 (Evaluation Metrics, Strict/Loose Align); Table 2.]
    "we employ GPT-4o to refine the rationales to better align with the feature distribution of COUNTER MATH. Specifically, we randomly select one example from each of the four fields in our COUNTER MATH as a reference, and provide three manually rewritten before-and-after comparisons to guide the model. ... Strict Align: This measures the percentage of the model's provided examples that are fully consistent with the reference."

    The Strict/Loose metrics define example-based conceptual reasoning as semantic consistency with a predefined Reference Example from CounterMATH. The SFT refinement step rewrites the training rationales using reference examples sampled from CounterMATH fields, explicitly to 'align with the feature distribution of COUNTER MATH.' The post-training gain on Strict/Loose (30.2 to 31.4 and 33.2 to 34.7 in Table 2) is therefore partly a measure of how well the model absorbed the benchmark's own reference style during training, not an independent measurement of a general counterexample-reasoning ability. The F1 and OOD results do not share this construction.

full rationale

No load-bearing self-citations or imported uniqueness arguments were found. The benchmark is constructed from external textbooks, and the SFT corpus (ProofNet, NaturalProofs) is stated to be disjoint from CounterMATH, so the headline F1 and OOD numbers are genuine held-out measurements. The central OOD claim (MATH 80.5 to 87.9; AIME 20.0 to 30.0) is not circular, although it is confounded by the absence of a generic proof-level SFT control, which is a validity concern rather than a circularity. The one circular element is the example-alignment evaluation: the training-data refinement injects CounterMATH reference examples as style guides, and the Strict/Loose metrics then score outputs by consistency with the same benchmark's reference style, making the reported improvement in 'quality of examples' partially self-referential. Because that metric is supporting rather than the central generalizability claim, a moderate score is appropriate.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The paper contributes data and a training recipe, not a new theoretical object. Its central causal claim rests on four unverified assumptions: the proxy validity of counterexample reasoning, the reliability of the GPT-4o judge, the quality of the GPT-4o filter, and non-overlap of training and test data. The most important missing piece is a control condition to rule out generic SFT effects.

assumptions (4)
  • domain assumption Counterexample-driven proof ability is a valid proxy for deep conceptual understanding.
    Invoked in the Introduction and Figure 1 as motivation; the benchmark's validity depends on this pedagogical premise, which is not empirically tested in the paper.
  • domain assumption The GPT-4o automated judge measures example extraction and alignment reliably beyond the checked 100 cases.
    Section 4 reports 97% extraction accuracy and 93.5% alignment accuracy on 100 manually reviewed samples; the paper assumes this generalizes to the remaining 1,116 items.
  • domain assumption The GPT-4o loose filter (at least one of three criteria) identifies genuine counterexample proofs in ProofNet and NaturalProofs.
    Section 5.1 and Appendix C define the filter; no manual audit of the resulting 1,025 samples is reported, so the quality of the SFT signal depends on an unvalidated filter.
  • domain assumption The training sources do not overlap with CounterMATH.
    Stated in Section 5.1, but no overlap check details, hashes, or deduplication results are provided.

how reviews work

0 comments
Cite this review

Pith. "Pith review of One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs." pith.science (2026). https://pith.science/paper/IG2AACFU

@misc{pith2026250210454,
  author       = {Pith},
  title        = {Pith review of: One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/IG2AACFU}},
  note         = {Machine review of arXiv:2502.10454}
}
read the original abstract

Leveraging mathematical Large Language Models (LLMs) for proof generation is a fundamental topic in LLMs research. We argue that the ability of current LLMs to prove statements largely depends on whether they have encountered the relevant proof process during training. This reliance limits their deeper understanding of mathematical theorems and related concepts. Inspired by the pedagogical method of "proof by counterexamples" commonly used in human mathematics education, our work aims to enhance LLMs' ability to conduct mathematical reasoning and proof through counterexamples. Specifically, we manually create a high-quality, university-level mathematical benchmark, CounterMATH, which requires LLMs to prove mathematical statements by providing counterexamples, thereby assessing their grasp of mathematical concepts. Additionally, we develop a data engineering framework to automatically obtain training data for further model improvement. Extensive experiments and detailed analyses demonstrate that CounterMATH is challenging, indicating that LLMs, such as OpenAI o1, have insufficient counterexample-driven proof capabilities. Moreover, our exploration into model training reveals that strengthening LLMs' counterexample-driven conceptual reasoning abilities is crucial for improving their overall mathematical capabilities. We believe that our work offers new perspectives on the community of mathematical LLMs.

Figures

Figures reproduced from arXiv: 2502.10454 by the authors.

Figure 1
Figure 1. Comparison between drill-based learning and example-based learning. The first two math LLMs fail when confronted with advanced mathematics, and “Proving by examples” is a highly creative and concept-intensive mathematical skill. As illustrated in [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Overview the construction process of COUNTERMATH. COUNTERMATH was first extracted from photocopied mathematical textbooks by crowd-sourced labelers with the OCR tool. For the next step, authors with bachelor degrees in applied mathematics as annotation experts would filter and correct improper statement-rationale pairs. Finally, GPT-4o was prompted to translate the validated data into English under experts’ supervis… view at source ↗
Figure 3
Figure 3. Data Distribution of COUNTERMATH. Data Validation As mentioned in Section 3.1, the reten￾tion rate between the two annotation stages is 95.4%, demon￾strating that most high-quality statement-rationale pairs were extracted from the textbooks. The filtered statement￾rationale pairs often suffer from issues such as irrelevance between statement and rationale, excessive typos, and trivial rationales, such as simply quot… view at source ↗
Figures from the paper (5 more)
Figure 4
Figure 4. Figure 4: The overview of our training data engineering framework. the judgements of the statements. The reason of not using accuracy is the imbalance of data distributions mentioned in Section 3.2. To assess whether the model has acquired the capability of solving mathematical …
Figure 5
Figure 5. Figure 5: Fine-grained evaluation results of different fields in COUNTERMATH. ing abilities on our benchmark [PITH_FULL_IMAGE:figures/full_fig_p007_5.png]
Figure 6
Figure 6. Figure 6: The relationship between Mean Token Ratios (%) and F1 (macro) scores for various models. The red dashed line represents the Ground Truth Token Ratio (100%), serving as an efficiency benchmark. Models closer to this line are more token-efficient, while those farther to …
Figure 7
Figure 7. Figure 7: Our case studies of the performance of LLM include: (1) correct judgment with incorrect examples, (2) validation of novel but effective counterexamples, and (3) performance improvement on MATH dataset after counterexample training fers from reference ones, yet are corr…
Figure 8
Figure 8. Figure 8: An annotation example from Counterexamples in Real Analysis. (Wang, 1989). B. Details for Experimental Settings Summary for Open-weight Baselines The summary of the open-weight baseline models is shown in the following [PITH_FULL_IMAGE:figures/full_fig_p013_8.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

60 extracted references · 32 canonical work pages

  1. [1]

    Mathqa: Towards interpretable math word problem solving with operation-based formalisms

    Amini, A., Gabriel, S., Lin, P., Koncel-Kedziorski, R., Choi, Y., and Hajishirzi, H. Mathqa: Towards interpretable math word problem solving with operation-based formalisms. arXiv preprint arXiv:1905.13319, 2019

  2. [2]

    W., Radev, D., and Avigad, J

    Azerbayev, Z., Piotrowski, B., Schoelkopf, H., Ayers, E. W., Radev, D., and Avigad, J. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. CoRR, abs/2302.12433, 2023. doi:10.48550/ARXIV.2302.12433

  3. [3]

    Chen, W., Ma, X., Wang, X., and Cohen, W. W. Program of thoughts prompting: Disentangling computation from reasoning for numerical reasoning tasks. Transactions on Machine Learning Research, 2023

  4. [4]

    Inductive or deductive? rethinking the fundamental reasoning abilities of llms

    Cheng, K., Yang, J., Jiang, H., Wang, Z., Huang, B., Li, R., Li, S., Li, Z., Gao, Y., Li, X., et al. Inductive or deductive? rethinking the fundamental reasoning abilities of llms. arXiv preprint arXiv:2408.00114, 2024

  5. [5]

    Generative ai for math: Abel

    Chern, E., Zou, H., Li, X., Hu, J., Feng, K., Li, J., and Liu, P. Generative ai for math: Abel. https://github.com/GAIR-NLP/abel, 2023

  6. [6]

    Training verifiers to solve math word problems

    Cobbe, K., Kosaraju, V., Bavarian, M., Chen, M., Jun, H., Kaiser, L., Plappert, M., Tworek, J., Hilton, J., Nakano, R., Hesse, C., and Schulman, J. Training verifiers to solve math word problems. arXiv preprint arXiv:2110.14168, 2021

  7. [7]

    Process reinforcement through implicit rewards, 2025

    Cui, G., Yuan, L., Wang, Z., Wang, H., Li, W., He, B., Fan, Y., Yu, T., Xu, Q., Chen, W., Yuan, J., Chen, H., Zhang, K., Lv, X., Wang, S., Yao, Y., Peng, H., Cheng, Y., Liu, Z., Sun, M., Zhou, B., and Ding, N. Process reinforcement through implicit rewards, 2025

  8. [8]

    C., and Berner, J

    Frieder, S., Pinchetti, L., Chevalier, A., Griffiths, R.-R., Salvatori, T., Lukasiewicz, T., Petersen, P. C., and Berner, J. Mathematical capabilities of chatgpt, 2023

Show all 60 references
  1. [9]

    Large language models for mathematicians, 2024

    Frieder, S., Berner, J., Petersen, P., and Lukasiewicz, T. Large language models for mathematicians, 2024

  2. [10]

    Google, G. T. Gemini 1.5: Unlocking multimodal understanding across millions of tokens of contexts, 2024

  3. [11]

    Tora: A tool-integrated reasoning agent for mathematical problem solving

    Gou, Z., Shao, Z., Gong, Y., Yang, Y., Huang, M., Duan, N., Chen, W., et al. Tora: A tool-integrated reasoning agent for mathematical problem solving. In The Twelfth International Conference on Learning Representations, 2024

  4. [12]

    Putnam- AXIOM : A functional and static benchmark for measuring higher level mathematical reasoning

    Gulati, A., Miranda, B., Chen, E., Xia, E., Fronsdal, K., de Moraes Dumont, B., and Koyejo, S. Putnam- AXIOM : A functional and static benchmark for measuring higher level mathematical reasoning. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS'24, 2024

  5. [13]

    Llm reasoners: New evaluation, library, and analysis of step-by-step reasoning with large language models

    Hao, S., Gu, Y., Luo, H., Liu, T., Shao, X., Wang, X., Xie, S., Ma, H., Samavedhi, A., Gao, Q., et al. Llm reasoners: New evaluation, library, and analysis of step-by-step reasoning with large language models. arXiv preprint arXiv:2404.05221, 2024

  6. [14]

    L., Shen, J., Hu, J., Han, X., Huang, Y., Zhang, Y., Liu, J., Qi, L., Liu, Z., and Sun, M

    He, C., Luo, R., Bai, Y., Hu, S., Thai, Z. L., Shen, J., Hu, J., Han, X., Huang, Y., Zhang, Y., Liu, J., Qi, L., Liu, Z., and Sun, M. Olympiadbench: A challenging benchmark for promoting agi with olympiad-level bilingual multimodal scientific problems, 2024

  7. [15]

    Measuring mathematical problem solving with the math dataset

    Hendrycks, D., Burns, C., Kadavath, S., Arora, A., Basart, S., Tang, E., Song, D., and Steinhardt, J. Measuring mathematical problem solving with the math dataset. NeurIPS, 2021

  8. [16]

    Counterexamples in Algebra

    Hu, C. Counterexamples in Algebra. Shaanxi Science and Technology Press, 1983

  9. [17]

    Lateval: An interactive llms evaluation benchmark with incomplete information from lateral thinking puzzles

    Huang, S., Ma, S., Li, Y., Huang, M., Zou, W., Zhang, W., and Zheng, H. Lateval: An interactive llms evaluation benchmark with incomplete information from lateral thinking puzzles. In Calzolari, N., Kan, M., Hoste, V., Lenci, A., Sakti, S., and Xue, N. (eds.), Proceedings of t...

  10. [18]

    Q., Welleck, S., Zhou, J

    Jiang, A. Q., Welleck, S., Zhou, J. P., Lacroix, T., Liu, J., Li, W., Jamnik, M., Lample, G., and Wu, Y. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations, 2023

  11. [19]

    Counterexamples in Calculus

    Klymchuk, S. Counterexamples in Calculus. 01 2010. ISBN 9780883857656. doi:10.1090/clrm/034

  12. [20]

    Common 7b language models already possess strong math capabilities

    Li, C., Wang, W., Hu, J., Wei, Y., Zheng, N., Hu, H., Zhang, Z., and Peng, H. Common 7b language models already possess strong math capabilities. arXiv preprint arXiv:2403.04706, 2024 a

  13. [21]

    Q., Shen, Z., et al

    Li, J., Beeching, E., Tunstall, L., Lipkin, B., Soletskyi, R., Huang, S., Rasul, K., Yu, L., Jiang, A. Q., Shen, Z., et al. Numinamath: The largest public dataset in ai4maths with 860k pairs of competition math problems and solutions. Hugging Face repository, 13: 0 9, 2024 b

  14. [22]

    Towards real-world writing assistance: A chinese character checking benchmark with faked and misspelled characters

    Li, Y., Xu, Z., Chen, S., Huang, H., Li, Y., Jiang, Y., Li, Z., Zhou, Q., Zheng, H.-T., and Shen, Y. Towards real-world writing assistance: A chinese character checking benchmark with faked and misspelled characters. arXiv preprint arXiv:2311.11268, 2023

  15. [23]

    Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving

    Li, Y., Du, D., Song, L., Li, C., Wang, W., Yang, T., and Mi, H. Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving. arXiv preprint arXiv:2412.20735, 2024 c

  16. [24]

    Li, Y., Zhou, Q., Luo, Y., Ma, S., Li, Y., Zheng, H.-T., Hu, X., and Philip, S. Y. When llms meet cunning texts: A fallacy understanding benchmark for large language models. In The Thirty-eight Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2024 d

  17. [25]

    Correct like humans: Progressive learning framework for chinese text error correction

    Li, Y., Ma, S., Chen, S., Huang, H., Huang, S., Li, Y., Zheng, H.-T., and Shen, Y. Correct like humans: Progressive learning framework for chinese text error correction. Expert Systems with Applications, 265: 0 126039, 2025

  18. [26]

    Lean-star: Learning to interleave thinking and proving

    Lin, H., Sun, Z., Yang, Y., and Welleck, S. Lean-star: Learning to interleave thinking and proving. arXiv preprint arXiv:2407.10040, 2024 a

  19. [27]

    Rho-1: Not all tokens are what you need

    Lin, Z., Gou, Z., Gong, Y., Liu, X., Shen, Y., Xu, R., Lin, C., Yang, Y., Jiao, J., Duan, N., et al. Rho-1: Not all tokens are what you need. arXiv preprint arXiv:2404.07965, 2024 b

  20. [28]

    Mathbench: Evaluating the theory and application proficiency of llms with a hierarchical mathematics benchmark, 2024

    Liu, H., Zheng, Z., Qiao, Y., Duan, H., Fei, Z., Zhou, F., Zhang, W., Zhang, S., Lin, D., and Chen, K. Mathbench: Evaluating the theory and application proficiency of llms with a hierarchical mathematics benchmark, 2024

  21. [29]

    Mathvista: Evaluating mathematical reasoning of foundation models in visual contexts

    Lu, P., Bansal, H., Xia, T., Liu, J., Li, C., Hajishirzi, H., Cheng, H., Chang, K.-W., Galley, M., and Gao, J. Mathvista: Evaluating mathematical reasoning of foundation models in visual contexts. In International Conference on Learning Representations (ICLR), 2024

  22. [30]

    Wizardmath: Empowering mathematical reasoning for large language models via reinforced evol-instruct

    Luo, H., Sun, Q., Xu, C., Zhao, P., Lou, J., Tao, C., Geng, X., Lin, Q., Chen, S., and Zhang, D. Wizardmath: Empowering mathematical reasoning for large language models via reinforced evol-instruct. arXiv preprint arXiv:2308.09583, 2023

  23. [31]

    Gsm-symbolic: Understanding the limitations of mathematical reasoning in large language models

    Mirzadeh, I., Alizadeh, K., Shahrokhi, H., Tuzel, O., Bengio, S., and Farajtabar, M. Gsm-symbolic: Understanding the limitations of mathematical reasoning in large language models. arXiv preprint arXiv:2410.05229, 2024

  24. [32]

    Moura, L. d. and Ullrich, S. The lean 4 theorem prover and programming language. In Platzer, A. and Sutcliffe, G. (eds.), Automated Deduction -- CADE 28, pp.\ 625--635, Cham, 2021. Springer International Publishing. ISBN 978-3-030-79876-5

  25. [33]

    Gpt-4 technical report, 2023

    OpenAI. Gpt-4 technical report, 2023

  26. [34]

    Y., Padmakumar, V., Joshi, N., Kazemi, M., Kim, N., and He, H

    Saparov, A., Pang, R. Y., Padmakumar, V., Joshi, N., Kazemi, M., Kim, N., and He, H. Testing the general deductive reasoning capacity of large language models using OOD examples. In Thirty-seventh Conference on Neural Information Processing Systems, 2023

  27. [35]

    Deepseekmath: Pushing the limits of mathematical reasoning in open language models

    Shao, Z., Wang, P., Zhu, Q., Xu, R., Song, J., Bi, X., Zhang, H., Zhang, M., Li, Y., Wu, Y., et al. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. arXiv preprint arXiv:2402.03300, 2024

  28. [36]

    Simon, M. A. Studying mathematics conceptual learning: Student learning through their mathematical activity. North American Chapter of the International Group for the Psychology of Mathematics Education, 2011

  29. [37]

    Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition

    Tsoukalas, G., Lee, J., Jennings, J., Xin, J., Ding, M., Jennings, M., Thakur, A., and Chaudhuri, S. Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition. In The Thirty-eight Conference on Neural Information Processing Systems Datasets and Benc...

  30. [38]

    Counterexamples in Real Analysis

    Wang, L. Counterexamples in Real Analysis. Higher Education Press, 1989

  31. [39]

    Counterexamples in Functional Analysis

    Wang, L. Counterexamples in Functional Analysis. Higher Education Press, 1994

  32. [40]

    and Yang, F

    Wang, L. and Yang, F. Counterexamples in Topology. Science Press, 2000

  33. [41]

    Hypothesis search: Inductive reasoning with language models

    Wang, R., Zelikman, E., Poesia, G., Pu, Y., Haber, N., and Goodman, N. Hypothesis search: Inductive reasoning with language models. In The Twelfth International Conference on Learning Representations, 2024 a

  34. [42]

    On the role of entity and event level conceptualization in generalizable reasoning: A survey of tasks, methods, applications, and future directions

    Wang, W., Fang, T., Shi, H., Xu, B., Ding, W., Zhang, L., Fan, W., Bai, J., Li, H., Liu, X., et al. On the role of entity and event level conceptualization in generalizable reasoning: A survey of tasks, methods, applications, and future directions. arXiv preprint arXiv:2406.10...

  35. [43]

    Mmlu-pro: A more robust and challenging multi-task language understanding benchmark

    Wang, Y., Ma, X., Zhang, G., Ni, Y., Chandra, A., Guo, S., Ren, W., Arulraj, A., He, X., Jiang, Z., et al. Mmlu-pro: A more robust and challenging multi-task language understanding benchmark. Advances in Neural Information Processing Systems, 37: 0 95266--95290, 2024 c

  36. [44]

    V., Zhou, D., et al

    Wei, J., Wang, X., Schuurmans, D., Bosma, M., Xia, F., Chi, E., Le, Q. V., Zhou, D., et al. Chain-of-thought prompting elicits reasoning in large language models. Advances in neural information processing systems, 35: 0 24824--24837, 2022

  37. [45]

    L., Hajishirzi, H., Choi, Y., and Cho, K

    Welleck, S., Liu, J., Bras, R. L., Hajishirzi, H., Choi, Y., and Cho, K. Naturalproofs: Mathematical theorem proving in natural language. In Vanschoren, J. and Yeung, S. (eds.), Proceedings of the Neural Information Processing Systems Track on Datasets and Benchmarks 1, NeurIP...

  38. [46]

    and Gao, X.-S

    Wu, W. and Gao, X.-S. Mathematics mechanization and applications after thirty years. Frontiers of Computer Science in China, 1: 0 1--8, 02 2007. doi:10.1007/s11704-007-0001-8

  39. [47]

    Mathematics Mechanization: Mechanical Geometry Theorem-Proving, Mechanical Geometry Problem-Solving and Polynomial Equations-Solving

    Wu, W.-t. Mathematics Mechanization: Mechanical Geometry Theorem-Proving, Mechanical Geometry Problem-Solving and Polynomial Equations-Solving. Mathematics and Its Applications. Springer Netherlands, 2001. ISBN 9780792358350

  40. [48]

    Conceptmath: A bilingual concept-wise benchmark for measuring mathematical reasoning of large language models

    Wu, Y., Liu, J., Bu, X., Liu, J., Zhou, Z., Zhang, Y., Zhang, C., Bai, Z., Chen, H., Ge, T., et al. Conceptmath: A bilingual concept-wise benchmark for measuring mathematical reasoning of large language models. arXiv preprint arXiv:2402.14660, 2024

  41. [49]

    Let llms take on the latest challenges! a chinese dynamic question answering benchmark

    Xu, Z., Li, Y., Ding, R., Wang, X., Chen, B., Jiang, Y., Deng, X., Ma, J., Zheng, H.-T., Lu, W., et al. Let llms take on the latest challenges! a chinese dynamic question answering benchmark. arXiv preprint arXiv:2402.19248, 2024

  42. [50]

    Qwen2 technical report

    Yang, A., Yang, B., Hui, B., Zheng, B., Yu, B., Zhou, C., Li, C., Li, C., Liu, D., Huang, F., et al. Qwen2 technical report. arXiv preprint arXiv:2407.10671, 2024

  43. [51]

    and Deng, J

    Yang, K. and Deng, J. Learning to prove theorems via interacting with proof assistants. In International Conference on Machine Learning, pp.\ 6984--6994. PMLR, 2019

  44. [52]

    H., and Zhou, D

    Yasunaga, M., Chen, X., Li, Y., Pasupat, P., Leskovec, J., Liang, P., Chi, E. H., and Zhou, D. Large language models as analogical reasoners. In The Twelfth International Conference on Learning Representations, 2024

  45. [53]

    Internlm-math: Open math large language models toward verifiable reasoning

    Ying, H., Zhang, S., Li, L., Zhou, Z., Shao, Y., Fei, Z., Ma, Y., Hong, J., Liu, K., Wang, Z., et al. Internlm-math: Open math large language models toward verifiable reasoning. arXiv preprint arXiv:2402.06332, 2024

  46. [54]

    T., Li, Z., Weller, A., and Liu, W

    Yu, L., Jiang, W., Shi, H., Yu, J., Liu, Z., Zhang, Y., Kwok, J. T., Li, Z., Weller, A., and Liu, W. Metamath: Bootstrap your own mathematical questions for large language models. arXiv preprint arXiv:2309.12284, 2023

  47. [55]

    Metamath: Bootstrap your own mathematical questions for large language models

    Yu, L., Jiang, W., Shi, H., Jincheng, Y., Liu, Z., Zhang, Y., Kwok, J., Li, Z., Weller, A., and Liu, W. Metamath: Bootstrap your own mathematical questions for large language models. In The Twelfth International Conference on Learning Representations, 2024 a

  48. [56]

    Reasonagain: Using extractable symbolic programs to evaluate mathematical reasoning

    Yu, X., Zhou, B., Cheng, H., and Roth, D. Reasonagain: Using extractable symbolic programs to evaluate mathematical reasoning. arXiv preprint arXiv:2410.19056, 2024 b

  49. [57]

    Mammoth2: Scaling instructions from the web

    Yue, X., Zheng, T., Zhang, G., and Chen, W. Mammoth2: Scaling instructions from the web. arXiv preprint arXiv:2405.03548, 2024

  50. [58]

    M., and Polu, S

    Zheng, K., Han, J. M., and Polu, S. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations, 2022

  51. [59]

    Conceptual and unbiased reasoning in language models

    Zhou, B., Zhang, H., Chen, S., Yu, D., Wang, H., Peng, B., Roth, D., and Yu, D. Conceptual and unbiased reasoning in language models. arXiv preprint arXiv:2404.00205, 2024

  52. [60]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 gl...

Pith tools

Reviewed August 8, 2026 · model on record in the stance chip above.