Pith. sign in

REVIEW 4 major objections 3 minor 57 references

PuzzleClone: A DSL-Powered Framework for Synthesizing Verifiable Data

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

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

Pith's one-line read PuzzleClone claims that DSL-encoded, SMT-solved puzzle generation can produce 83,657 verifiable problems, and training on them lifts a 7B model from 14.4 to 56.2 on the benchmark and up to 12.5 points on external math and logic tests.

desk verdict A real DSL-driven synthesis pipeline and a useful new benchmark, but validity of individual 83K variants is not demonstrated and the empirical reporting is inconsistent. read the letter →

arxiv 2508.15180 v3 pith:ZFIJSM4V submitted 2025-08-21 cs.AI

Kai Xiong , Yanwei Huang , Rongjunchen Zhang , Kun Chen , Haipang Wu , Yingcai Wu This is my paper
classification cs.AI
keywords PuzzleClonePC-83KSMTsolvingdomain-specificlanguageverifiabledatasynthesislogicalreasoningbenchmarkLLMpost-trainingaugmentation
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 claims that trustworthy reasoning data does not have to be hand-curated and small: a puzzle can be encoded as a logical template plus parameters, and software can then produce tens of thousands of variants whose answers are computed by a solver rather than guessed by a model. Its framework, PuzzleClone, encodes 86 seed puzzles in a purpose-built domain-specific language, randomizes variables and constraints to generate 83,657 deduplicated puzzles (PC-83K), derives ground truth with the Z3 SMT solver, and certifies the encoding by reproducing the original seed puzzles from their configs. The resulting benchmark is hard for current models — Qwen2.5-7B-Instruct scores 14.4 and GPT-4o 27.7 — and the central empirical claim is that training on it transfers: after supervised fine-tuning, the same 7B model reaches 56.2 on PC-83K and improves six of seven external logic and math benchmarks, with AMC2023 rising from 52.5 to 65.0. If this holds, the main bottleneck in reasoning-data creation — trustworthy labels at scale — can be replaced by a formal pipeline whose cost structure permits essentially unbounded expansion.

What carries the argument

The machinery is the specification/config pair (Qs, Qc): a structured DSL description of a puzzle's variables, symbols, conditions, queries, and description template, paired with a config file pinning concrete values. A generator re-randomizes the config; the Z3 SMT solver turns the symbolic constraints into solver-derived answers; and a validation script deterministically reproduces the seed puzzle from its config, certifying the encoding. The load-bearing idea is that the template/parameter split turns puzzle synthesis into a search over a formal space, so ground truth comes from a solver rather than a language model, and seed reproduction substitutes for per-instance human review.

What would settle it

Take a random sample of variants from the hard subset (difficulty > 0.5), where the paper notes solvability drops as complexity grows, and run the generation script for each variant's own config: check that the solver finds at least one solution, that the number of solutions is compatible with the stored answer (exactly one where the spec asserts uniqueness), and that the rendered question text does not state the answer explicitly. The validator in the paper only reproduces the seed puzzle, so if more than a small fraction of sampled variants fail any of these checks, the claim that all 83,657

Watch

Extended reading notes

Core claim

PuzzleClone's central claim: a puzzle can be split into a universal logical template plus parameters, captured in a purpose-built DSL (a domain-specific language describing variables, symbols, condition templates, queries, and the natural-language wrapper). Randomizing a spec's config generates new puzzles; the Z3 SMT (Satisfiability Modulo Theories) solver computes ground-truth answers from the symbolic constraints; and a config-based validator re-runs the pipeline on the seed config to confirm the encoding reproduces the seed's known answer. Applied to 86 curated seeds this produced PC-83K (83,657 deduplicated puzzles). The paper further claims the data is both hard and instructive: a 7B b

Load-bearing premise

Every one of the 83,657 generated puzzles is treated as verified because the pipeline successfully reproduces the one seed puzzle from its config; the randomized variants themselves are not individually checked to be faithful, non-leaking, and uniquely answered.

Editorial extensions

If this is right

  • SFT on the 4,300-sample SFT subset lifts Qwen2.5-7B-Instruct's PC-83K average from 14.4 to 56.2 (normal 63.5, hard 49.0), showing the harder half remains a real challenge.
  • The same SFT transfers to external benchmarks: AMC2023 52.5→65.0, SATBench 52.8→65.0, AIME25 6.7→23.3, MATH500 75.2→81.2, OlympiadBench 42.5→46.4, AIME24 16.7→20.0; BBEH-mini drops from 11.3 to 9.8, which the paper attributes to duplicated generations in the SFT set.
  • Reinforcement learning (GRPO) alone also lifts the baseline — 14.4 to 47.7 — and is the better stage for BBEH-mini (13.3 vs 9.8), but it trails SFT on every math benchmark, so the two stages are not substitutes.
  • Because randomization and answer derivation are programmatic and LLM-free after encoding, the marginal cost of additional puzzles is low — the framework's route to much larger datasets is different from LLM-based augmentation.
  • Config-level deduplication plus per-seed, difficulty-stratified splits mean the test set is structurally distinct from training variants, not just reworded copies.

Reading between the lines

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

  • The 'verified' claim is only as strong as the seed-reproduction check: per-variant fidelity, answer uniqueness, and non-leakage are assumed from careful spec design, not measured. A per-config validation sweep over all 83,657 instances would convert that assumption into data; the paper does not run it.
  • The backward generation strategy the paper recommends — synthesize a solution first, then constraints certifying it — is the component most likely to transfer to other NP-complete puzzle families (scheduling, packing, graph problems), where it would guarantee solvability by construction.
  • If the transfer gains are real, the framework suggests a general recipe: any puzzle family expressible in SMT can be turned into ground-truth-checkable training data, which may matter more for reasoning skill acquisition than the puzzle surface itself.
  • The dynamic rephrasing feature (same config, new language or scenario) offers a ready test of whether the trained gains survive surface changes; the paper provides the mechanism but reports no experiment on it.
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 / 3 minor

Summary. The paper introduces PuzzleClone, a DSL-based framework for synthesizing large numbers of logical/mathematical puzzles from manually encoded seed puzzles. A seed puzzle is encoded into a formal specification plus a configuration; a generator uses Z3 to produce randomized variants, and a config-based reproduction step validates that the seed puzzle can be regenerated. The authors construct PC-83K, a dataset of 83,657 puzzles, and report post-training (SFT and RL) of Qwen2.5-7B-Instruct on PuzzleClone data. The central empirical claim is that such training improves both in-distribution PuzzleClone accuracy and out-of-distribution logic/mathematics benchmarks. The paper also includes extensive DSL schema details, dataset construction and partitioning, difficulty analysis, and benchmark evaluations of many proprietary and open-source models.

Significance. If the main claims hold, the paper makes a useful contribution: it provides a scalable, Z3-backed pipeline for generating verifiable reasoning data and demonstrates transfer to external benchmarks. The DSL design, the use of SMT solving for answer derivation, the seed-reproduction checker, and the public release of code/data are notable strengths. The construction of 83K diverse, formally derived puzzles is potentially valuable to the LLM reasoning community. However, the empirical inconsistencies and the gap between 'programmatically validated' and per-variant verification materially affect the strength of the central claims. The external-benchmark transfer results, if reliable, are the most compelling evidence, but the reported numbers need correction before the claims can be accepted.

major comments (4)
  1. [Abstract vs. §Experiments (Table 3)] The headline numbers are inconsistent. The abstract reports PuzzleClone average improving from 14.5 to 66.0 and SATBench from 51.6 to 70.0, while the body (Table 3 and surrounding text) reports 14.4 to 56.2 and SATBench 52.8 to 65.0. These are different results, and the abstract cannot be reconciled with the table. This is load-bearing because the central claim is specifically about the magnitude of improvement. The authors must identify and correct the discrepancy.
  2. [§Experiments, 'Post Training' and Table 3] The claim of 'consistent improvements across 7 logic and mathematical benchmarks' is contradicted by the paper's own data. Table 3 shows that SFT lowers BBEH-mini from 11.3 to 9.8. The text acknowledges this but still uses 'consistent improvements' in the abstract and elsewhere. The claim needs qualification or the experiments need to be reconciled. Also, the explanation that duplicated generations caused the BBEH-mini drop is not supported by any experiment.
  3. [§2.3, §6, Table 10/Table 11] The claim that all 83,657 variants are 'programmatically validated' is not supported. Section 2.3 describes a validation script that only reproduces the seed puzzle from the seed config, not per-variant checks. For multiple-choice items, the DSL has 'cond: any' and 'cond: all' but no demonstrated mechanism that exactly one option is entailed or that no option leaks the answer. Section 6 itself states that redundancy/leakage 'should be designed against' and that harder variants are more likely to be unsolvable. Thus, the paper treats per-variant semantic validity as an assumption, not a verified property. Please provide either per-instance uniqueness/leakage checks, a statistical audit, or a formal argument covering all generated variants.
  4. [Table 1] The dataset partitioning table is internally inconsistent. The row sums and column interpretation are unclear: 4,300 + 74,354 + 860 = 79,514, not 83,657; the 'Test' column contains values 50,738 and 24,046 that do not sum to the stated test total of 8,443. The relationship between SFT, RL-Train, RL-Val, and Test counts needs a clear and correct presentation, because the paper's post-training numbers depend on these subsets.
minor comments (3)
  1. [§3.4 and Figure 8] The difficulty model is acknowledged as imperfect in §6, and Figure 8 shows hard variants sometimes outperforming normal variants. This is acceptable as a limitation, but the Normal/Hard stratification in Table 2 and Table 3 should be interpreted with this caveat in mind.
  2. [Throughout] Minor typos and wording issues: 'paramter,' 'curated' vs. 'curated,' 'SMT-solvable problems' etc. A careful proofread is needed.
  3. [Reproducibility Checklist] The checklist contains several placeholder responses such as 'Type your response here'; these should be completed before publication.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the central claims rest on external benchmarks and independent evidence.

full rationale

PuzzleClone's core derivation chain is: manually encode seed puzzles into a DSL; generate variants by randomizing variables and constraints; use Z3 to obtain answers; post-train models; evaluate on the PuzzleClone test set and on independent logic/math benchmarks. None of these steps reduces to its own inputs in the sense required for circularity. The Z3-derived answers are internally consistent with the DSL constraints by construction, but this is a benchmark-design property, not a scientific prediction being passed off as independent confirmation. The paper's actual predictive claim—that SFT/RL on PuzzleClone improves LLM reasoning—is evaluated on external benchmarks (AMC2023, AIME, SATBench, etc.) that are not generated by PuzzleClone. The config-based reproduction check (Sec. 2.3) validates only the seed encoding, not every randomized variant; the paper itself notes in Sec. 6 that solvability decreases with complexity and that leakage must be designed against. This is a limitation in per-instance verification, not circularity. There are no load-bearing self-citations: the cited works (Z3, prior puzzle datasets, GRPO, etc.) are external, and no 'uniqueness theorem' is imported from the authors' prior work. No fitted parameter is renamed as a prediction. The internal test split follows standard train/test partitioning for a generated benchmark; it is not a circular validation of the framework's scientific value, which is independently supported by the external-benchmark gains. Therefore the paper receives a circularity score of 0.

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

The central claim of 'verifiable data at scale' rests on manually authored DSL specifications and on Z3 as an oracle. The reproduction step checks only the seed config, so random variants inherit the assumption that sampling stays within the semantically valid region. Difficulty-related hyperparameters are hand-set and admitted by the authors to be imperfect.

free parameters (4)
  • difficulty threshold (normal/hard) = 0.5
    Section 3.5: puzzles classified as normal (difficulty <= 0.5) or hard (> 0.5). The threshold is arbitrary and affects all Normal/Hard performance splits.
  • variable diff_factor weights = +1, -1, 0 per variable
    Section 3.4: each variable is assigned a difficulty factor by hand and used to compute var_scale and the composite difficulty score. The paper itself says this 3-value scheme fails to capture nuanced relationships.
  • SFT and RL subset sizes per seed = 25 normal + 25 hard SFT; 5 + 5 RL-val per seed
    Section 3.5: these hand-chosen sampling sizes determine which samples enter the SFT and RL validation sets and therefore shape the reported post-training numbers.
  • per-spec variable domains and constraint count ranges = e.g., s_num [4,7], f_num [3,5], domain '[1, s_num * f_num // 2]'
    Hand-set in each DSL spec; they determine the puzzle space and difficulty distribution. Figure 4 shows that changing only the p_num domain for 9-vase materially changes the number of valid generated puzzles.
assumptions (4)
  • domain assumption Z3 is sound and complete for the SMT formulas used, and its solutions match the intended puzzle semantics.
    Invoked in Section 2.2 (puzzle generation) and Section 2.3 (validation). The entire verifiability claim depends on Z3 being a correct oracle for the encoded constraints.
  • ad hoc to paper The manually written DSL spec Qs faithfully captures the semantics of the seed puzzle, including implicit assumptions.
    Section 2.1 describes manual encoding. The reproduction validator checks only one specific seed config, so semantic fidelity for all random configs is assumed rather than proven.
  • ad hoc to paper Randomly sampled variables and conditions produce puzzles that are solvable, unambiguous, and non-leaking.
    Sections 2.2, 2.3, and 6. The paper admits solvability probability diminishes with complexity and that leakage must be explicitly designed against, so this assumption is load-bearing.
  • domain assumption LLM-based seed filtering with Qwen2.5-72B plus human review yields a representative and diverse seed set.
    Section 3.1: seeds are selected by a prompted LLM and manual curation. There are no objective metrics for representativeness or inter-annotator agreement.

how reviews work

0 comments
Cite this review

Pith. "Pith review of PuzzleClone: A DSL-Powered Framework for Synthesizing Verifiable Data." pith.science (2026). https://pith.science/paper/ZFIJSM4V

@misc{pith2026250815180,
  author       = {Pith},
  title        = {Pith review of: PuzzleClone: A DSL-Powered Framework for Synthesizing Verifiable Data},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ZFIJSM4V}},
  note         = {Machine review of arXiv:2508.15180}
}
read the original abstract

High-quality mathematical and logical datasets with verifiable answers are essential for strengthening the reasoning capabilities of large language models (LLMs). While recent data augmentation techniques have facilitated the creation of large-scale benchmarks, existing LLM-generated datasets often suffer from limited reliability, diversity, and scalability. To address these challenges, we introduce PuzzleClone, a formal framework for synthesizing verifiable data at scale using a novel DSL-driven approach. Our approach features three key innovations: (1) encoding seed puzzles into structured logical specifications, (2) generating scalable variants through systematic variable and constraint randomization, and (3) ensuring validity via a reproduction mechanism. Applying PuzzleClone, we construct PC-83K, a benchmark comprising over 83K diverse and programmatically validated puzzles. The generated puzzles span a wide spectrum of difficulty and formats, posing significant challenges to current state-of-the-art models. Experimental results show that post training (SFT and RL) on PC-83K yields substantial improvements not only on the testset but also on various logic and mathematical benchmarks. Post training raises average performance on PC-83K from 14.5 to 66.0 and delivers consistent improvements across 7 logic and mathematical benchmarks up to 18.4 absolute percentage points (SATBench from 51.6 to 70.0). Our code and data are available at https://github.com/HiThink-Research/PuzzleClone.

Figures

Figures reproduced from arXiv: 2508.15180 by the authors.

Figure 1
Figure 1. Overview of the PuzzleClone framework. systematically modifying existing “seed” instances (Feng et al. 2021; Lu et al. 2024). This strategy has the poten￾tial to vastly expand the size and diversity of reasoning datasets while reducing the manual effort involved in their creation. However, current augmentation pipelines largely rely on LLMs to annotate new problems, generate solutions, and verify the answers (Lu et … view at source ↗
Figure 2
Figure 2. The data synthesis pipeline of PuzzleClone. (A) An example seed puzzle. (B, C) The DSL specification and the config [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Puzzle difficulty distribution before and after dedu [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figures from the paper (5 more)
Figure 4
Figure 4. Figure 4: Number of valid puzzles (after de-duplication) [PITH_FULL_IMAGE:figures/full_fig_p007_4.png]
Figure 5
Figure 5. Figure 5: Seed Puzzle Selection Prompt for filtering seed puzzles via the Qwen2.5-72B-Instruct model. [PITH_FULL_IMAGE:figures/full_fig_p014_5.png]
Figure 6
Figure 6. Figure 6: Question-Type Prompt Wrappers for LLM reason [PITH_FULL_IMAGE:figures/full_fig_p018_6.png]
Figure 7
Figure 7. Figure 7: Distribution of duplicated instances across 32 seed puzzles. Only seed puzzles with at least one duplicate are shown. [PITH_FULL_IMAGE:figures/full_fig_p022_7.png]
Figure 8
Figure 8. Figure 8: The average accuracy of all models on the PuzzleClone test set grouped by the seed puzzles. [PITH_FULL_IMAGE:figures/full_fig_p023_8.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

57 extracted references · 30 canonical work pages

  1. [1]

    , " * write output.state after.block = add.period write newline

    ENTRY address archivePrefix author booktitle chapter edition editor eid eprint howpublished institution isbn journal key month note number organization pages publisher school series title type volume year label extra.label sort.label short.list INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.a...

  2. [2]

    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 global.max substring 't := if while FUNCTION word.in bbl.in capitalize " " * FUNCT...

  3. [3]

    Anthropic . 2024. Introducing Claude 3.5 Sonnet. https://www.anthropic.com/news/claude-3-5-sonnet. Announcement; see also model card addendum

    work page 2024

  4. [4]

    Anthropic . 2025. Claude Opus 4 & Claude Sonnet 4: System Card. https://www.anthropic.com/claude-4-system-card. Model referenced in paper as Claude-4-sonnet

    work page 2025

  5. [5]

    Barrett, C.; Stump, A.; Tinelli, C.; et al. 2010. The smt-lib standard: Version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, UK), volume 13, 14

    work page 2010

  6. [6]

    Bayer, M.; Kaufhold, M.-A.; and Reuter, C. 2022. A survey on data augmentation for text classification. ACM Computing Surveys, 55(7): 1--39

    work page 2022

  7. [7]

    P.; Liu, C.; Bing, L.; Zhao, D.; Luu, A

    Chen, G.; Xu, W.; Zhang, H.; Chan, H. P.; Liu, C.; Bing, L.; Zhao, D.; Luu, A. T.; and Rong, Y. 2025 a . FINEREASON : Evaluating and Improving LLMs ' Deliberate Reasoning through Reflective Puzzle Solving . ArXiv:2502.20238 [cs]

    arXiv 2025

  8. [8]

    Chen, J.; Wei, Z.; Ren, Z.; Li, Z.; and Zhang, J. 2025 b . LR 2 Bench : Evaluating Long -chain Reflective Reasoning Capabilities of Large Language Models via Constraint Satisfaction Problems . ArXiv:2502.17848 [cs]

    work page Pith review arXiv 2025

Show all 57 references
  1. [9]

    K.; Zhang, X.; and Tao, D

    Chen, M. K.; Zhang, X.; and Tao, D. 2025. JustLogic: A Comprehensive Benchmark for Evaluating Deductive Reasoning in Large Language Models. arXiv preprint arXiv:2501.14851

    2025 arXiv

  2. [10]

    F.; and Mellish, C

    Clocksin, W. F.; and Mellish, C. S. 2003. Programming in PROLOG. Springer Science & Business Media

    2003

  3. [11]

    Csan \'a dy, B.; Muzsai, L.; Vedres, P.; N \'a dasdy, Z.; and Luk \'a cs, A. 2024. LlamBERT: Large-scale low-cost data annotation in NLP. arXiv preprint arXiv:2403.15938

    2024 arXiv

  4. [12]

    De Moura, L.; and Bj rner, N. 2008. Z3: an efficient SMT solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'08/ETAPS'08, 337–340. Berlin, Heidelberg: Springer-...

    2008

  5. [13]

    Ding, N.; Chen, Y.; Xu, B.; Qin, Y.; Zheng, Z.; Hu, S.; Liu, Z.; Sun, M.; and Zhou, B. 2023. Enhancing chat language models by scaling high-quality instructional conversations. arXiv preprint arXiv:2305.14233

    2023 arXiv

  6. [14]

    Y.; Gangal, V.; Wei, J.; Chandar, S.; Vosoughi, S.; Mitamura, T.; and Hovy, E

    Feng, S. Y.; Gangal, V.; Wei, J.; Chandar, S.; Vosoughi, S.; Mitamura, T.; and Hovy, E. 2021. A Survey of Data Augmentation Approaches for NLP . In Zong, C.; Xia, F.; Li, W.; and Navigli, R., eds., Findings of the Association for Computational Linguistics: ACL-IJCNLP 2021, 968...

    2021

  7. [15]

    Gemini Team . 2025 a . Gemini 2.0 Flash. https://cloud.google.com/vertex-ai/generative-ai/docs/models/gemini/2-0-flash. Model referenced in paper as Gemini-2.0-flash

    2025

  8. [16]

    Gemini Team . 2025 b . Gemini 2.5: Pushing the Frontier with Advanced Reasoning, Multimodality, Long Context, and Next Generation Agentic Capabilities. Technical report, Google DeepMind. Covers Gemini 2.5 Pro (and 2.5 Flash); model referenced in paper as Gemini-2.5-pro

    2025

  9. [17]

    Gui, J.; Liu, Y.; Cheng, J.; Gu, X.; Liu, X.; Wang, H.; Dong, Y.; Tang, J.; and Huang, M. 2024. Logicgame: Benchmarking rule-based reasoning abilities of large language models. arXiv preprint arXiv:2408.15778

    2024 arXiv

  10. [18]

    Guo, D.; Yang, D.; Zhang, H.; Song, J.; Zhang, R.; Xu, R.; Zhu, Q.; Ma, S.; Wang, P.; Bi, X.; Zhang, X.; Yu, X.; Wu, Y.; Wu, Z.; Gou, Z.; Shao, Z.; Li, Z.; Gao, Z.; DeepSeek-AI Team ; et al. 2025. DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learni...

    2025 arXiv

  11. [19]

    L.; Shen, J.; Hu, J.; Han, X.; Huang, Y.; Zhang, Y.; et al

    He, C.; Luo, R.; Bai, Y.; Hu, S.; Thai, Z. L.; Shen, J.; Hu, J.; Han, X.; Huang, Y.; Zhang, Y.; et al. 2024. Olympiadbench: A challenging benchmark for promoting agi with olympiad-level bilingual multimodal scientific problems. arXiv preprint arXiv:2402.14008

    2024 arXiv

  12. [20]

    Hendrycks, D.; Burns, C.; Kadavath, S.; Arora, A.; Basart, S.; Tang, E.; Song, D.; and Steinhardt, J. 2021 a . Measuring Mathematical Problem Solving With the MATH Dataset. arXiv preprint arXiv:2103.03874

    2021 arXiv

  13. [21]

    Hendrycks, D.; Burns, C.; Kadavath, S.; Arora, A.; Basart, S.; Tang, E.; Song, D.; and Steinhardt, J. 2021 b . Measuring Mathematical Problem Solving With the MATH Dataset. NeurIPS

    2021

  14. [22]

    Huang, Y.; Wu, S.; Gao, C.; Chen, D.; Zhang, Q.; Wan, Y.; Zhou, T.; Xiao, C.; Gao, J.; Sun, L.; et al. 2024. Datagen: Unified synthetic dataset generation via large language models. In The Thirteenth International Conference on Learning Representations

    2024

  15. [23]

    D.; Aglietti, V.; Jindal, D.; Chen, P.; Dikkala, N.; Tyen, G.; Liu, X.; Shalit, U

    Kazemi, M.; Fatemi, B.; Bansal, H.; Palowitch, J.; Anastasiou, C.; Mehta, S.; Jain, L. D.; Aglietti, V.; Jindal, D.; Chen, P.; Dikkala, N.; Tyen, G.; Liu, X.; Shalit, U. S.; Tay, Y.; Tran, V. Q.; Le, Q. V.; and Firat, O. 2025. BIG‑Bench Extra Hard. arXiv preprint arXiv:2502.19187

    2025 arXiv

  16. [24]

    Leang, J. O. J.; Hong, G.; Li, W.; and Cohen, S. B. 2025. Theorem Prover as a Judge for Synthetic Data Generation

    2025

  17. [25]

    F.; Liu, Z.; and Yang, D

    Li, M.; Shi, T.; Ziems, C.; Kan, M.-Y.; Chen, N. F.; Liu, Z.; and Yang, D. 2023. Coannotating: Uncertainty-guided work allocation between human and large language models for data annotation. arXiv preprint arXiv:2310.15638

    2023 arXiv

  18. [26]

    Li, N.; Liu, P.; Liu, Z.; Dai, T.; Jiang, Y.; and Xia, S.-T. 2025. Logic-of-Thought: Empowering Large Language Models with Logic Programs for Solving Puzzles in Natural Language. arXiv preprint arXiv:2505.16114

    2025 arXiv

  19. [27]

    Liu, J.; Fan, Y.; Jiang, Z.; Ding, H.; Hu, Y.; Zhang, C.; Shi, Y.; Weng, S.; Chen, A.; Chen, S.; Huang, Y.; Zhang, M.; Zhao, P.; Yan, J.; and He, J. 2025 a . SynLogic: Synthesizing Verifiable Reasoning Data at Scale for Learning Logical Reasoning and Beyond. arXiv:2505.19641

    2025 arXiv

  20. [28]

    Liu, J.; Lin, X.; Bayer, J.; Dillies, Y.; Jiang, W.; Liang, X.; Soletskyi, R.; Wang, H.; Xie, Y.; Xiong, B.; et al. 2025 b . CombiBench: Benchmarking LLM capability for combinatorial mathematics. arXiv preprint arXiv:2505.03171

    2025 arXiv

  21. [29]

    Lu, Y.; Shen, M.; Wang, H.; Wang, X.; van Rechem, C.; Fu, T.; and Wei, W. 2023. Machine learning for synthetic data generation: a review. arXiv preprint arXiv:2302.04062

    2023 arXiv

  22. [30]

    Lu, Z.; Zhou, A.; Ren, H.; Wang, K.; Shi, W.; Pan, J.; Zhan, M.; and Li, H. 2024. MathGenie: Generating Synthetic Data with Question Back-translation for Enhancing Mathematical Reasoning of LLMs . In Proceedings of the 62nd Annual Meeting of the Association for Computational L...

    2024

  23. [31]

    Luo, M.; Kumbhar, S.; Parmar, M.; Varshney, N.; Banerjee, P.; Aditya, S.; Baral, C.; et al. 2023. Towards logiglue: A brief survey and a benchmark for analyzing logical reasoning capabilities of language models. arXiv preprint arXiv:2310.00836

    2023 arXiv

  24. [32]

    MAA; and users, B. 2023. AMC 2023 benchmark (American Mathematics Competition 2023). Used as evaluation benchmark in LLM reasoning research

    2023

  25. [33]

    MAA; and users, B. 2024. AIME 2024 benchmark (American Invitational Mathematics Examination 2024). Used as evaluation benchmark in LLM reasoning research

    2024

  26. [34]

    MAA; and users, B. 2025. AIME 2025 benchmark (American Invitational Mathematics Examination 2025). Used in recent benchmarks like SATBench analysis, etc

    2025

  27. [35]

    L.; Trivedi, A.; and Somenzi, F

    Maiya, A.; Alghamdi, R.; Pacheco, M. L.; Trivedi, A.; and Somenzi, F. 2025. Explaining Puzzle Solutions in Natural Language: An Exploratory Study on 6x6 Sudoku. arXiv preprint arXiv:2505.15993

    2025 arXiv

  28. [36]

    math ai. 2025. AIME25 Dataset. Accessed: 2025-07-01

    2025

  29. [37]

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

    2024 arXiv

  30. [38]

    Mittal, C.; Kartik, K.; Mausam; and Singla, P. 2024. PuzzleBench : Can LLMs Solve Challenging First - Order Combinatorial Reasoning Problems ? ArXiv:2402.02611 [cs] version: 2

    2024 arXiv

  31. [39]

    OpenAI . 2024. GPT-4o System Card. https://arxiv.org/abs/2410.21276. Model referenced in paper as ChatGPT-4o

    2024 arXiv

  32. [40]

    OpenAI . 2025. OpenAI o3 and o4-mini System Card. https://openai.com/index/o3-o4-mini-system-card/. Model referenced in paper as ChatGPT-o3

    2025

  33. [41]

    Pan, L.; Albalak, A.; Wang, X.; and Wang, W. 2023. Logic- LM : Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning. In Bouamor, H.; Pino, J.; and Bali, K., eds., Findings of the Association for Computational Linguistics: EMNLP 2023, 3806--3824...

    2023

  34. [42]

    Parmar, M.; Patel, N.; Varshney, N.; Nakamura, M.; Luo, M.; Mashetty, S.; Mitra, A.; and Baral, C. 2024. LogicBench: Towards systematic evaluation of logical reasoning ability of large language models. arXiv preprint arXiv:2404.15522

    2024 arXiv

  35. [43]

    R.; Mozer, M.; Bengio, Y.; Arora, S.; and Goyal, A

    Shah, V.; Yu, D.; Lyu, K.; Park, S.; Ke, N. R.; Mozer, M.; Bengio, Y.; Arora, S.; and Goyal, A. 2024. AI-Assisted Generation of Difficult Math Questions

    2024

  36. [44]

    K.; Wu, Y.; and Guo, D

    Shao, Z.; Wang, P.; Zhu, Q.; Xu, R.; Song, J.; Bi, X.; Zhang, H.; Zhang, M.; Li, Y. K.; Wu, Y.; and Guo, D. 2024. DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models. arXiv preprint arXiv:2402.03300. Introduces Group Relative Policy Optimization (GRPO)

    2024 arXiv

  37. [45]

    Sugiyama, A.; and Yoshinaga, N. 2019. Data augmentation using back-translation for context-aware neural machine translation. In Proceedings of the fourth workshop on discourse in machine translation (DiscoMT 2019), 35--44

    2019

  38. [46]

    Tan, Z.; Li, D.; Wang, S.; Beigi, A.; Jiang, B.; Bhattacharjee, A.; Karami, M.; Li, J.; Cheng, L.; and Liu, H. 2024. Large Language Models for Data Annotation and Synthesis: A Survey. In Al-Onaizan, Y.; Bansal, M.; and Chen, Y.-N., eds., Proceedings of the 2024 Conference on E...

    2024

  39. [47]

    THUDM . 2025. GLM-Z1-32B-0414. https://huggingface.co/THUDM/GLM-Z1-32B-0414. GLM-Z1 reasoning model series (incl. 9B/32B); model card

    2025

  40. [48]

    Wang, K.; Zhu, J.; Ren, M.; Liu, Z.; Li, S.; Zhang, Z.; Zhang, C.; Wu, X.; Zhan, Q.; Liu, Q.; and Wang, Y. 2024 a . A Survey on Data Synthesis and Augmentation for Large Language Models , volume 1. Association for Computing Machinery

    2024

  41. [49]

    Wang, Y.; Stevens, D.; Shah, P.; Jiang, W.; Liu, M.; Chen, X.; Kuo, R.; Li, N.; Gong, B.; Lee, D.; et al. 2024 b . Model-in-the-Loop (MILO): Accelerating Multimodal AI Data Annotation with LLMs. arXiv preprint arXiv:2409.10702

    2024 arXiv

  42. [51]

    Wei, A.; Wu, Y.; Wan, Y.; Suresh, T.; Tan, H.; Zhou, Z.; Koyejo, S.; Wang, K.; and Aiken, A. 2025 b . SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas. arXiv preprint arXiv:2505.14615

    2025

  43. [52]

    Xu, C.; Sun, Q.; Zheng, K.; Geng, X.; Zhao, P.; Feng, J.; Tao, C.; Lin, Q.; and Jiang, D. 2024 a . WizardLM: Empowering large pre-trained language models to follow complex instructions. In The Twelfth International Conference on Learning Representations

    2024

  44. [53]

    Xu, Z.; Jiang, F.; Niu, L.; Deng, Y.; Poovendran, R.; Choi, Y.; and Lin, B. Y. 2024 b . Magpie: Alignment data synthesis from scratch by prompting aligned llms with nothing. arXiv preprint arXiv:2406.08464

    2024 arXiv

  45. [54]

    Yang, A.; Li, A.; Yang, B.; Zhang, B.; Hui, B.; Zheng, B.; Yu, B.; Gao, C.; Huang, C.; Lv, C.; Zheng, C.; Liu, D.; Zhou, F.; Huang, F.; Hu, F.; Ge, H.; Wei, H.; Lin, H.; Tang, J.; Yang, J.; Tu, J.; Zhang, J.; Yang, J.; Yang, J.; Zhou, J.; Zhou, J.; Lin, J.; Dang, K.; Bao, K.; ...

    2025 arXiv

  46. [55]

    Yang, A.; Yang, B.; Zhang, B.; Hui, B.; Zheng, B.; Yu, B.; Li, C.; Liu, D.; Huang, F.; Wei, H.; Lin, H.; Yang, J.; Tu, J.; Zhang, J.; Yang, J.; Yang, J.; Zhou, J.; Lin, J.; Dang, K.; Lu, K.; Bao, K.; Yang, K.; Yu, L.; Li, M.; Xue, M.; Zhang, P.; Zhu, Q.; Men, R.; Lin, R.; Li, ...

    2024 arXiv

  47. [56]

    Zhang, R.; Li, Y.; Ma, Y.; Zhou, M.; and Zou, L. 2023. Llmaaa: Making large language models as active annotators. arXiv preprint arXiv:2310.19596

    2023 arXiv

  48. [57]

    Zhang, S.; Jafari, O.; and Nagarkar, P. 2021. A survey on machine learning techniques for auto labeling of video, audio, and text data. arXiv preprint arXiv:2109.03784

    2021 arXiv

  49. [58]

    Zhu, Z.; Wang, Y.; Yang, S.; Long, L.; Wu, R.; Tang, X.; Zhao, J.; and Wang, H. 2024. CORAL: Collaborative Automatic Labeling System Based on Large Language Models. Proc. VLDB Endow., 17(12): 4401–4404

    2024

Pith tools

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