Pith. sign in

REVIEW 5 major objections 5 minor 35 references

STORM-BORN: A Challenging Mathematical Derivations Dataset Curated via a Human-in-the-Loop Multi-Agent Framework

T0 review · 5 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper claims that STORM-BORN, a 100-problem dataset of derivation tasks from recent papers, defeats current LLMs (under 5% solved) and still fine-tunes them to improve numerical reasoning.

desk verdict STORM-BORN is a genuine new benchmark for dense mathematical derivations, but its headline <5% solve rate rests on an underspecified human evaluation that may penalize correct alternative derivations. read the letter →

arxiv 2506.01531 v2 pith:BDDL3FJT submitted 2025-06-02 cs.CL

Wenhao Liu , Zhenyi Lu , Xinyu Hu , Jierui Zhang , Dailin Li , Jiacheng Cen , Huilin Cao , Haiteng Wang
show 8 more authors
Yuhan Li Kun Xie Dandan Li Pei Zhang Chengbo Zhang Yuxiang Ren Xiaohong Huang Yan Ma
This is my paper · ORCID
classification cs.CL
keywords STORM-BORNmathematicalderivationsmulti-agentdatagenerationhuman-in-the-loopLLMbenchmarkfine-tuningreasoningdensitynumericaltransfer
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

STORM-BORN is a dataset of 100 mathematical derivation problems harvested from recent peer-reviewed papers, built by a six-agent LLM pipeline and then hand-filtered by human mathematicians. The paper's central claim is that these problems are genuinely hard: the strongest tested models, GPT-o1-Pro and DeepSeek-R1, solve fewer than 5% of them, far below their near-saturation performance on GSM8K and MATH. The authors further claim that fine-tuning open models on this small set transfers to out-of-domain numerical reasoning, with absolute gains of 7.84% (LLaMA3-8B) and 9.12% (Qwen2.5-7B) on MATH, and relative gains of over 200% for TinyLLaMA. If true, the dataset is both a high-difficulty benchmark for frontier AI and evidence that small amounts of dense, human-like derivation reasoning can teach generalizable problem-solving skills.

What carries the argument

The load-bearing mechanism is the STORM multi-agent generation framework combined with human expert selection. Six specialized agents—a LaTeX math extractor, a query drafter (GPT-o1-Pro), an answer retriever that pulls derivations verbatim from the source paper, a context collector, a question refiner that makes problems self-contained, and an answer filter—turn a paper's formulas into question–answer pairs; human mathematicians then score each candidate on reasoning type, clarity, correctness, and reasoning density and keep only the top 100. The paper's illustrative example is the DPO closed-form solution $\pi_r(y|x) = \frac{1}{Z(x)}\pi_{\mathrm{ref}}(y|x)\exp(\frac{1}{\beta}r(x,y))$, where the generated answer reproduces the derivation from the KL-constrained objective with explicit heuristic cues. The mechanism is what turns raw paper text into self-contained, hard, human-like derivation problems.

What would settle it

Have an independent panel of professional mathematicians, with stated credentials and measured inter-annotator agreement, re-verify all 100 ground-truth derivations and re-score the model outputs blind; if a substantial share of derivations contain errors or if any model's re-scored solve rate exceeds 5%, the difficulty claim would be refuted.

Watch

Extended reading notes

Core claim

STORM-BORN is positioned as a third kind of math dataset, neither numerical word problems nor formal theorem-proving code, but natural-language derivations that reproduce the long chains, approximations, and heuristic trial-and-error a mathematician actually performs. The authors claim that from 2,000 pipeline-generated samples, expert mathematicians selected 100 with the highest reasoning density and correctness, and that these 100 defeat all six evaluated frontier models, with the best (GPT-o1-Pro) at 5% and DeepSeek-R1 at 4.6%. They also claim that supervised fine-tuning on only these 100 samples yields consistent accuracy gains on GSM8K, MATH, and AIME across TinyLLaMA, LLaMA2-7B, LLaMA3-8B, and Qwen2.5 models, and that a quality ablation shows the curated top-100 outperforms larger uncurated subsets. The runnable artifact is the dataset itself plus the STORM pipeline that produced it.

Load-bearing premise

The benchmark's difficulty and correctness rest on the assumption that the human mathematicians' quick review—about fifteen minutes per paper, roughly thirty seconds per problem—caught every error in the AI-generated derivations and scored the model outputs fairly.

Editorial extensions

If this is right

  • If the <5% solve rate holds under independent scoring, STORM-BORN becomes a benchmark where frontier LLM progress on genuine research-level derivation can be tracked for the first time.
  • Fine-tuning on just 100 STORM-BORN samples transfers to GSM8K, MATH, and AIME, so small curated derivation sets could be a data-efficient alternative to large arithmetic corpora.
  • The quality ablation implies that uncurated synthetic data can actively hurt reasoning performance (full 2k set drops LLaMA2-7B GSM8K zero-shot from 7.96% to 5.16%), reinforcing the value of the human-in-the-loop filter.
  • The same pipeline can be pointed at fresh papers to produce new hard benchmarks continuously, avoiding the staleness and contamination that affect static datasets.

Reading between the lines

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

  • Inference: The <5% figure depends on human partial-credit scoring of long free-form derivations; a more mechanical scoring rule (e.g., checking only the final formula or key lemmas) could change model rankings even if the dataset is correct.
  • Inference: The transfer gains may come from the derivations' dense heuristic cues and step length rather than from mathematical content per se; ablating problems by step count or by presence of approximation language would test this directly.
  • Inference: The same multi-agent-plus-expert recipe could plausibly be reused for other reasoning-dense fields (theoretical physics, algorithms, formal methods) where derivation chains appear in papers.
  • Inference: Because the dataset deliberately samples recent (2023–2024) papers, its difficulty may decay quickly as models train on those same papers; the pipeline is the durable contribution, not the static 100 items.
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

5 major / 5 minor

Summary. The paper introduces STORM-BORN, a dataset of 100 mathematical derivation problems extracted from recent arXiv papers through a human-in-the-loop, six-agent LLM pipeline. The authors claim that frontier LLMs such as GPT-o1-Pro solve fewer than 5% of these problems, and that fine-tuning on STORM-BORN improves performance on standard numerical reasoning benchmarks such as GSM8K, MATH, and AIME. The paper also reports a quality ablation suggesting that a small, expertly curated subset outperforms larger automatically generated subsets. The dataset and code are publicly released.

Significance. If the difficulty and generalization claims hold, STORM-BORN would be a useful complement to existing numerical-reasoning and formal-theorem-proving benchmarks, targeting informal, human-like derivations with dense reasoning steps. The multi-agent curation framework is described in unusual detail, including full prompts in the appendix, and the public release of code and data is a practical strength. The fine-tuning experiments cover several model families and show some positive transfer effects. However, the headline 'fewer than 5%' difficulty claim is not yet secure because the human evaluation protocol is under-specified: the number and credentials of expert graders, the scoring rubric, and inter-annotator agreement are all missing, and the reference answers were produced by the same LLM pipeline being evaluated. The fine-tuning evidence is also mixed, with several large degradations in Table 1 that are not discussed.

major comments (5)
  1. [§3.3 and §4.2] The central difficulty claim ("even most advanced models solve fewer than 5%") rests entirely on expert scoring, but the manuscript does not report how many experts graded each response, what their mathematical qualifications were, the detailed rubric used to decide "fully correct" versus "partial credit," or any inter-annotator agreement statistic. Section 3.3 states that one paper's ~30 samples were processed in about 15 minutes, i.e., roughly 30 seconds per sample, which is too fast to give confidence that the LLM-extracted reference derivations were carefully checked. This is load-bearing: if the reference derivations contain errors, or if the rubric penalizes correct alternative derivations, the reported solve rates measure annotation artifacts rather than mathematical difficulty. The authors should release the full scoring protocol, the individual expert scores, and an agreement analysis, and ideally have an independent set of graders re-score a random subset.
  2. [§3.2 and §4.2] The reference answers used as ground truth in the human evaluation were produced by the same GPT-o1-Pro-based multi-agent pipeline that is being evaluated (Query Draft Agent and Answer Retriever Agent), and §4.2 does not state that graders were instructed to credit mathematically correct derivations that differ stylistically from the reference. Since the dataset deliberately contains "human-like approximations and heuristic cues" rather than formal proofs, a model can produce a correct derivation with different notation, ordering, or heuristic choices. If graders compare against the reference solution rather than the underlying mathematical claim, the <5% result would be partly a rubric-mismatch artifact. I recommend a targeted experiment: have independent mathematicians score a random sample of model outputs against the original paper's derivation (not the pipeline's extracted answer) and report the difference.
  3. [§4.2 vs §4.3] The paper states in §4.2 that DeepSeek-R1 "assigns a perfect score to flawed cases" and therefore expert validation is essential, yet §4.3 uses DeepSeek-R1 as the automatic evaluator for the formula-derivation test set, scoring correctness, completeness, and similarity. This is internally inconsistent unless the authors show that DeepSeek-R1's scores are calibrated for that particular test set. They should either validate DeepSeek-R1's scores against human scores on a subsample, report the correlation or agreement, or use a different evaluation method.
  4. [Table 1 and §4.3] The abstract and §4.3 highlight positive fine-tuning gains, but Table 1 contains notable degradations that are not discussed: LLaMA3-8B drops from 50.27% to 45.49% on GSM8K-8shot and from 17.08% to 13.82% on MATH-4shot after fine-tuning, and LLaMA2-7B gains on MATH are near zero in the 4-shot setting. No confidence intervals or multiple-seed results are reported, so it is unclear whether the headline gains (7.84% on MATH for LLaMA3-8B, 9.12% on MATH-4shot for Qwen2.5-7B) are statistically meaningful. The claim that "the improvement increases with model capability" is not supported by these mixed results. Please report variance across seeds, significance tests or effect sizes, and discuss the drops explicitly.
  5. [§3.3 and Table 4] The procedure for selecting the "100 most difficult" samples is described only through four qualitative principles, although §3.3 says there are five core principles and lists only Q1 through Q4. There is no quantitative difficulty score, no threshold, and no inter-rater reliability for the selection. This matters for the quality-ablation claim in Table 4 that "top-100" outperforms larger subsets. The authors should define an operational difficulty metric or at least report the agreement among experts in choosing the top-100, and state how borderline samples were resolved.
minor comments (5)
  1. [Figure 3] The numerical labels in Figure 3 are difficult to parse: the value "5" appears between the model names and the percentage list, and the abstract's "fewer than 5%" should be reconciled with the exact values shown. Please reformat the figure so each bar has a clear value, and ensure the text matches those values.
  2. [Figure 1 and §4.1] The MiniF2F example is described as "can be solved with only one ring"; this should be "one `ring` tactic" or "one proof step" for clarity.
  3. [Introduction] The introduction says "Qwen improves by 16.7%" while the abstract and Table 1 report a 9.12% absolute gain on MATH-4shot; the 16.7% is a relative improvement. Please state which convention is being used in each place.
  4. [Appendix C] The heading for the derivation evaluation prompt reads "Prompt of Answer Retriever," but this is the evaluation prompt, not the Answer Retriever agent prompt. Please correct the heading.
  5. [Throughout] The model name is written inconsistently as "Deepseek-R1" in some places and "DeepSeek-R1" in others; please standardize.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: STORM-BORN's ground truth comes from external papers, difficulty is an empirical measurement, and fine-tuning gains are evaluated on held-out benchmarks; noted evaluation inconsistencies are validity concerns, not circular derivation steps.

full rationale

STORM-BORN's questions are generated from formulas extracted from external academic papers, and the reference answers are retrieved from those same papers (Sec. 3.2), so the ground truth is an external source rather than a quantity fitted from model outputs. The benchmark difficulty claim (<5% solve rate) is an empirical measurement on a deliberately hard subset; while the selection criteria explicitly target difficulty and reasoning density (Sec. 3.3), that is standard benchmark curation, not an equation-level reduction. Fine-tuning gains are measured on held-out external benchmarks (GSM8K, MATH, AIME, and a NuminaMath-derived formula derivation test set), so the generalization claim is not equivalent to the training signal. The paper cites several works by its own authors, but only as related-work context (e.g., Lu et al. 2024a, 2024b; Fan et al. 2024; Liu et al. 2024); none of these citations is load-bearing for the central claim. The internal inconsistency that DeepSeek-R1 is described as an over-generous scorer in Sec. 4.2 yet used as an evaluator in Sec. 4.3, and the absence of inter-annotator agreement statistics, are validity/correctness concerns for the evaluations, not circular derivation steps. No prediction in the paper reduces by construction to its inputs.

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

The central claims rest on design choices (keyword threshold, review score gate, final count) and on assumptions about the reliability of the source papers, the human review, and the multi-agent extraction. No new physical or mathematical entities are introduced.

free parameters (3)
  • keyword occurrence threshold = 5
    Papers are included only if markers like 'assume', 'derive', and 'proof' appear more than five times (Section 3.1); the cutoff is chosen by hand.
  • OpenReview score threshold = above weak accept
    Only papers scoring higher than weak accept on OpenReview are kept (Section 3.1); a hand-chosen quality gate.
  • final dataset size = 100
    The authors deliberately reduced 2000 synthesized samples to the 100 most difficult (Sections 1 and 3.3); the number is a design choice, not derived from a power analysis.
assumptions (3)
  • domain assumption The source papers' derivations are assumed correct and complete enough to serve as ground truth.
    The Answer Retriever Agent extracts answers directly from the papers (Section 3.2). If a source paper skips steps or contains an error, the resulting benchmark answer inherits it.
  • domain assumption Human experts can verify derivation correctness and reasoning density in about 30 seconds per QA sample.
    Section 3.3 reports 30 samples per paper processed in about 15 minutes; no inter-annotator agreement or expert-count details are given.
  • ad hoc to paper The multi-agent LLM pipeline faithfully extracts formulas and answers without introducing errors that the human review would miss.
    The paper relies on GPT-o1-Pro and MLLM extraction (Section 3.2) but provides no quantitative reliability check beyond the human selection.

how reviews work

0 comments
Cite this review

Pith. "Pith review of STORM-BORN: A Challenging Mathematical Derivations Dataset Curated via a Human-in-the-Loop Multi-Agent Framework." pith.science (2026). https://pith.science/paper/BDDL3FJT

@misc{pith2026250601531,
  author       = {Pith},
  title        = {Pith review of: STORM-BORN: A Challenging Mathematical Derivations Dataset Curated via a Human-in-the-Loop Multi-Agent Framework},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/BDDL3FJT}},
  note         = {Machine review of arXiv:2506.01531}
}
read the original abstract

High-quality math datasets are crucial for advancing the reasoning abilities of large language models (LLMs). However, existing datasets often suffer from three key issues: outdated and insufficient challenging content, neglecting human-like reasoning, and limited reliability due to single-LLM generation. To address these, we introduce STORM-BORN, an ultra-challenging dataset of mathematical derivations sourced from cutting-edge academic papers, which includes dense human-like approximations and heuristic cues. To ensure the reliability and quality, we propose a novel human-in-the-loop, multi-agent data generation framework, integrating reasoning-dense filters, multi-agent collaboration, and human mathematicians' evaluations. We curated a set of 2,000 synthetic samples and deliberately selected the 100 most difficult problems. Even most advanced models like GPT-o1 solved fewer than 5% of them. Fine-tuning on STORM-BORN boosts accuracy by 7.84% (LLaMA3-8B) and 9.12% (Qwen2.5-7B). As AI approaches mathematician-level reasoning, STORM-BORN provides both a high-difficulty benchmark and a human-like reasoning training resource. Our code and dataset are publicly available at https://github.com/lwhere/STORM-BORN.

Figures

Figures reproduced from arXiv: 2506.01531 by the authors.

Figure 1
Figure 1. (I) Numerical Reasoning datasets (e.g., PRM-800K) require numerical values, which may be too simplistic for advanced LLMs. (II) Formalized Theory Proving datasets (e.g., MiniF2F) depend on formal languages like Lean, limiting intuitive reasoning and informal generalization. (III) In contrast, our STORM-BORN dataset emphasizes human-like reasoning (highlighted in purple), requiring deep understanding and creativity, … view at source ↗
Figure 2
Figure 2. Overview of the data generation framework of STORM-BORN, which consists of three main components: [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Performance of leading language models on STORM-BORN based on a human expert evaluation. All [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

35 extracted references · 29 canonical work pages

  1. [1]

    theorem,

    Formula Recognition: - Identify all mathematical formulas, theorems, lemmas, and corollaries in the paper. Especially Numbered formulas.Retain the formula's number (if any). - For formulas without explicit labels (i.e., those not labeled as "theorem, " "lemma, " or "corollary"), classify them as "formula." - Required types of formulas to recognize: - Numb...

    work page

  2. [2]

    where X is

    LaTeX Conversion (Convert the formulas identified in step 1 into LaTeX format strings): - Symbols: Convert mathematical symbols accurately. - Subscripts and superscripts: Convert subscripts and superscripts correctly. - Uppercase and lowercase: Preserve the original variable and constant casing. - Formula structure: Keep the entire structure of the formul...

    work page

  3. [3]

    formula",

    JSONL Output: - Output all converted LaTeX strings in multi-line JSONL format so they can be parsed line by line. - Each line should be a JSON object whose key is the type of the formula ("formula", "lemma", "theorem", "corollary", etc.) and whose value is the LaTeX string obtained from step 2. - Be sure to follow the requirements in step 2! Ensure the fo...

    work page

  4. [4]

    What are the preconditions?

    Completeness of Preconditions: - The question content must include all direct necessary conditions. Particularly, indicate which other formulas the current formula is derived from or depends on, and clearly specify the entire content, numbering, or name of those referenced formulas. Do not produce questions such as "What are the preconditions?" --- Exampl...

    work page

  5. [6]

    InThe Twelfth Inter- national Conference on Learning Representations

    Let’s verify step by step. InThe Twelfth Inter- national Conference on Learning Representations. Wenhao Liu, Tianxing Bu, Erchen Yu, Dailin Li, Ding Ai, Zhenyi Lu, and Haoran Luo. 2024. Optimiz- ing few-shot learning: From static to adaptive in qwen2-7b. InSubmitted to Amazon KDD Cup 2024 Workshop. Under review. Pan Lu, Liang Qiu, Wenhao Yu, Sean Welleck,...

    arXiv 2024

  6. [7]

    InThirty-seventh Conference on Neural Information Processing Sys- tems

    Direct preference optimization: Your language model is secretly a reward model. InThirty-seventh Conference on Neural Information Processing Sys- tems. Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, Y . K. Li, Y . Wu, and Daya Guo. 2024. Deepseekmath: Pushing the limits of mathemati- cal reasoning in ...

    arXiv 2024

  7. [12]

    For each such formula, record its full content (in LaTeX format), its numbering (if any), and its name (if any)

    Which other formulas this formula is derived from or depends on. For each such formula, record its full content (in LaTeX format), its numbering (if any), and its name (if any)

    work page

  8. [13]

    Relevant problem settings

    work page

Show all 35 references
  1. [14]

    --- Step 2: Based on the extracted preconditions, generate a complete question that clearly asks how to derive or prove the formula

    The specific meaning of symbols or variables involved in the formula. --- Step 2: Based on the extracted preconditions, generate a complete question that clearly asks how to derive or prove the formula. The question should include:

  2. [15]

    Do not only reference its number

    The formula itself: Present the full content of this formula (in LaTeX format). Do not only reference its number

  3. [16]

    What are the preconditions?

    The preconditions: Explicitly integrate the preconditions extracted from the paper into the question. List out the full contents of all the formulas it depends on and reference them by their respective numbers or names. Do not produce a question such as "What are the precondit...

  4. [17]

    formula,

    Formula type: - The key is "formula, " "lemma, " "theorem, " etc. - The value is the LaTeX content of the formula

  5. [18]

    --- Important Notes:

    Generated question: - The key is "query." - The value is the complete question generated according to Step 1 and Step 2. --- Important Notes:

  6. [19]

    Format Requirements: - Ensure the output is in JSONL format, with each line corresponding to one data entry

  7. [20]

    Make sure they align with the original mathematical meaning

    Formula Accuracy: - If the question contains mathematical expressions, convert them into LaTeX format. Make sure they align with the original mathematical meaning. Minor formatting differences can be ignored

  8. [21]

    - Subscripts and superscripts: Convert subscripts and superscripts correctly

    LaTeX Conversion (Converts the mathematical expressions contained in the problem to strings in LaTeX format): - Symbols: Convert mathematical symbols accurately. - Subscripts and superscripts: Convert subscripts and superscripts correctly. - Uppercase and lowercase: Preserve t...

  9. [23]

    formula",

    **Formula-related keys ("formula", "lemma", "theorem", etc.)** indicating the type of mathematical expression; the value is the LaTeX-formatted mathematical expression extracted from the paper

  10. [24]

    expression

    **query**, whose value is a question generated by a large model based on the paper and the mathematical expression. Please process this dataset according to the following steps and requirements. --- ### Step One: For the "expression" and "query" in each piece of data, determin...

  11. [25]

    - If there are any references or citations, follow those as well

    **Find the first occurrence** - Locate where the expression first appears in the paper and check the surrounding context for relevant clues. - If there are any references or citations, follow those as well

  12. [26]

    This may well be the answer to the question

    **Check the appendix and other sections** - Search the paper's appendix or other relevant chapters to see if the proof or derivation steps for that expression are provided. This may well be the answer to the question

  13. [27]

    - If the paper does indeed contain content that can answer the question, extract the relevant content from the original text

    **Confirm feasibility** - If the paper does not include any relevant content addressing the question, you may skip this expression and proceed to the next one. - If the paper does indeed contain content that can answer the question, extract the relevant content from the origin...

  14. [28]

    The original two key-value pairs remain unchanged and must not be modified

  15. [29]

    --- ### Output Requirements:

    Add the`whole_label`key as the third key-value pair. --- ### Output Requirements:

  16. [30]

    **Multi-line JSONL format**: One data entry per line

  17. [31]

    **Accuracy of content**: Formulas must match the original text of the paper exactly, with correct symbols, subscripts, superscripts, and capitalization

  18. [32]

    $$\\pi_{r}(y | x)=\\frac{1}{Z (x)} \\pi_{r e f}(y | x) \\exp (\\frac{1}{\\beta} r (x, y)), $$(4)

    ** Content consistency ** : Only retain the original content in the answer (you can make a small amount of necessary cohesive editing, but do not change the original meaning), and try to avoid adding additional content or descriptions that do not appear in the original. --- ##...

  19. [33]

    - 1: Partially correct with significant flaws

    **Correctness (0-2):** - 0: Fundamentally wrong. - 1: Partially correct with significant flaws. - 2: Fully correct and logically sound

  20. [34]

    - 1: Moderately complete; some steps or justifications are missing

    **Completeness (0-2):** - 0: Incomplete; key steps are missing. - 1: Moderately complete; some steps or justifications are missing. - 2: Fully complete; all necessary steps and justifications are present

  21. [35]

    correctness

    **Similarity (0-2):** - 0: No similarity; completely different from the ground truth. - 1: Some similarity; some steps or justifications are similar. - 2: High similarity; all steps and justifications are identical. Output your evaluation as a JSON object in the format: {"corr...

  22. [2015]

    The lean theorem prover (system description). InCADE. Chenghao Fan, Zhenyi Lu, Sichen Liu, Chengfeng Gu, Xiaoye Qu, Wei Wei, and Yu Cheng. 2025. Make lora great again: Boosting lora with adaptive singular val- ues and mixture-of-experts optimization alignment. Preprint, arXiv:...

    2025

  23. [2021]

    Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer

    Training verifiers to solve math word prob- lems.Preprint, arXiv:2110.14168. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer

    arXiv

  24. [2022]

    InInternational Conference on Learning Representations

    minif2f: a cross-system benchmark for for- mal olympiad-level mathematics. InInternational Conference on Learning Representations. A Workload and Prompts We invested a lot of work, energy, and time in this research. Our goal is to generate high-quality formula derivation and q...

  25. [2023]

    Nuo Chen, Yuhan Li, Jianheng Tang, and Jia Li

    A survey on evaluation of large language mod- els.Preprint, arXiv:2307.03109. Nuo Chen, Yuhan Li, Jianheng Tang, and Jia Li. 2024. Graphwiz: An instruction-following language model for graph computational problems. InProceedings of the 30th ACM SIGKDD Conference on Knowledge D...

    2024 arXiv

  26. [2024]

    [https://huggingface

    Numinamath. [https://huggingface. co/AI-MO/NuminaMath-1.5](https: //github.com/project-numina/ aimo-progress-prize/blob/main/ report/numina_dataset.pdf). Qintong Li, Leyang Cui, Xueliang Zhao, Lingpeng Kong, and Wei Bi. 2024a. GSM-plus: A compre- hensive benchmark for evaluati...

    2025

  27. [2025]

    Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W

    Smollm2: When smol goes big – data- centric training of a small language model.Preprint, arXiv:2502.02737. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. 2023. Proofnet: Autoformalizing and formally proving undergr...

    2023 arXiv

Pith tools

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