Pith. sign in

REVIEW 4 major objections 3 minor 17 references

SPARQ: Synthetic Problem Generation for Reasoning via Quality-Diversity Algorithms

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

Pith's one-line read Filtering synthetic math problems by solve-rate—keeping only problems in a middle difficulty band—raises MATH pass@1 from 38% to 47%.

desk verdict Solid, honest empirical work on difficulty-filtered synthetic math data; the 9-point gain is plausible but a missing control and a few reporting slips need addressing. read the letter →

arxiv 2506.06499 v2 pith:3EFEB6YT submitted 2025-06-06 cs.LG cs.AI

classification cs.LGcs.AI
keywords syntheticdatagenerationquality-diversityalgorithmssolve-ratemathematicalreasoningself-improvementLLMfine-tuningout-of-distributiongeneralizationfiltering
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

SPARQ claims that a language model can bootstrap its own reasoning training data by mutating seed problems, scoring each new problem by the fraction of times the student model solves it (its solve-rate), and keeping only problems in a middle difficulty band. Fine-tuning the same student on this filtered, self-generated data improves MATH pass@1 from 38% to 47%, a 9-point absolute gain. The paper further argues that problem quality (difficulty) is the main driver of in-distribution gains, while problem diversity (coverage of skill combinations) improves out-of-distribution performance at higher inference budgets. It also reports scaling behavior: more generated data and larger generators yield better downstream models, and a model can self-improve by generating and verifying its own problems.

What carries the argument

The load-bearing object is the solve-rate score. For a generated problem-solution pair $(Q,A)$, the student model rolls out $K=16$ solutions $S_1,\ldots,S_K$; the solve-rate is the fraction of rollouts whose final numerical answer matches $A$. This number simultaneously serves as a difficulty estimate and, through successful rollouts, supplies the training solutions, so the final training pairs $(Q,S_k)$ are entirely self-generated. Around this score the paper builds a quality-diversity pipeline: a working set of parent problems is mutated by a generator, the archive accumulates all mutations, and update rules that keep the highest-quality items per skill-set niche (dynamic diverse) or uniformly (static uniform) produce differentiated data. The diversity measure is the count of unique skill-sets, where a skill-set is the combination of up to three semantic skills (e.g., algebra and pigeonhole principle) the solution uses.

What would settle it

Take the static-uniform generated archive and train two identical students on fixed sample budgets: one on the solve-rate band $0.1 \le \mathrm{SR} \le 0.9$ (SPARQ's filter) and one on an equal number of randomly sampled problems from the archive, with the MATH test set held out. If the random sample matches or beats the filtered model's pass@1, the solve-rate band is not the causal driver.

Watch

Extended reading notes

Core claim

The central claim is that solve-rate—the rate at which the student model $S_{\theta_2}$ reaches the intended numerical answer when sampling $K$ rollouts on a generated problem—is an effective, parameter-free proxy for the quality of a synthetic problem-solution pair. The paper defines $\mathrm{QUALITY}((Q,A),S_\theta) = 1 - \mathrm{SOLVERATE}((Q,A),S_\theta)$ for solve-rates between thresholds $T_l=0.1$ and $T_u=0.9$, and zero otherwise, then fine-tunes the student only on problems with positive quality, pairing each question with a successful self-generated verification. Applying this to the MATH seed set with a Gemma-2-9B student, static uniform generation improves pass@1 from 38% to 47%. Ablations with a fixed sample budget show that filtering for high quality (mean solve-rate around 0.2) improves in-distribution accuracy by over 2.5 points versus low-quality filtering, while filtering for diversity (maximizing unique skill-sets) gives the best OOD pass@96, suggesting quality and diversity play distinct roles.

Load-bearing premise

The whole pipeline depends on treating 'the student's rollout ends in the same number as the submitted solution' as a correct solution; the paper itself shows harder problems are more often logically invalid, so if this agreement check is miscalibrated the difficulty ranking is noise and the filter may be selecting for something other than quality.

Editorial extensions

If this is right

  • Training on solve-rate-filtered synthetic problems improves MATH pass@1 by 9 absolute points over the SFT baseline (38% to 47%), and the gain appears across all generation methods tested.
  • Scaling helps: tripling the number of generated problems yields roughly 1.5% additional accuracy, and increasing generator size from 2B to 27B adds cumulative relative gains on top of the 5% from a 2B generator.
  • The recipe is self-sustaining: a single 9B model generating, verifying, and training on its own problems improves by ~20% relative over its own SFT baseline.
  • Data diversity, measured by unique skill-sets, does not strongly help in-distribution performance but does improve OOD pass@96 (from 19% to 25% over random filtering), with the gap widening as inference budget increases.

Reading between the lines

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

  • The paper's own validity analysis shows harder problems are less likely to be logically valid, so the quality filter may in practice be selecting a difficulty curriculum rather than a correctness signal; if so, the same gain might be obtainable by adding noise or hard negatives in other domains.
  • Because the solve-rate uses final-numerical-answer agreement, the method will likely degrade on open-ended reasoning where no single final answer exists; a natural extension is to use verifier-based rewards or rubrics.
  • The OOD diversity benefit only appears at higher inference budgets, implying that studies reporting a single pass@1 may miss diversity's value; reporting pass@n curves could change conclusions about what data mixture to use.
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. This paper introduces SPARQ, a pipeline in which a single LLM (Gemma-2-9B) mutates seed math problems, evaluates each generated problem by its solve-rate under K=16 student rollouts, filters by a difficulty window, and fine-tunes the same student on successful rollouts. Using MATH as seed and test, the authors report an absolute 9% pass@1 gain (38% to 47%) over the SFT baseline, plus data and generator scaling laws, ablations of quality and diversity, and self-improvement results for 2B and 9B models. The paper also reports that dynamic quality-diversity variants generate more diverse data but underperform static uniform generation, and that harder problems are less likely to be logically valid.

Significance. The main result — that a single model can bootstrap its own reasoning data by filtering on solve-rate — is potentially significant for scaling synthetic data without a stronger teacher. The Section 3.2 fixed-budget ablations and the OOD inference-scaling analysis are thoughtful and go beyond a simple accuracy comparison, and the paper is unusually candid about the validity limitations of its quality measure (Section 3.1, Figure 5). However, the empirical support rests on single training runs without seeds, and the central comparison lacks an unfiltered control, so the strength of the claim is currently uncertain.

major comments (4)
  1. [Section 3, Experiments] Every reported number is a single fine-tuning run with no seeds, no error bars, and no significance testing. Differences as small as 1.5–3 percentage points are used to draw conclusions about data scaling, quality filtering, and OOD behavior (Figures 2, 6, 7). Without variance estimates, the 38% to 47% headline gain and the ranking of methods cannot be distinguished from noise. Please provide multiple seeds for the headline runs and key ablations, or otherwise quantify uncertainty.
  2. [Section 2, Measuring data quality; Section 3.1] The quality score is computed by agreement with the intended solution A, and the training set is constructed from the student's own successful rollouts; the main comparison is static uniform generation plus quality filtering versus SFT on the original 7.5K seed. This conflates two effects: selection by difficulty and the sheer volume of self-generated correct solutions. The Section 3.2 ablations start from a pool that has already been filtered to QUALITY>0 and compare within that pool; they do not provide the missing control of training on an equal-size random sample of successful rollouts without the solve-rate thresholds (or of an unfiltered archive). I request such a control to support the causal claim that difficulty filtering, not scale, drives the improvement.
  3. [Section 3.1, Figure 5] The paper reports a strong inverse correlation between solve-rate and validity; QUALITY = 1 - SOLVERATE therefore preferentially selects logically invalid problems. The authors acknowledge this and argue fine-tuning is robust to invalid noise, but no experiment directly compares training on valid versus invalid high-quality samples, or conditions on validity within a fixed difficulty level. Without such an analysis, the claim that 'higher quality, as measured by problem difficulty, facilitates better in-distribution performance' (Section 3.2) leaves open the possibility that the effect is driven by problem difficulty alone, while the quality score adds an uncontrolled validity confound. Please add a validity-controlled ablation.
  4. [Section 3.1; Appendix B] The dynamic generation methods, which optimize the solve-rate quality score, underperform static uniform generation; the paper attributes this to 'reward hacking' the QUALITY measure. This is an acknowledged failure mode of the proposed quality signal in the generation loop. It does not invalidate the static filtering result, but it does weaken the contribution that solve-rate is 'an effective way of measuring and filtering by synthetic problem quality' (Contribution 1). The paper should either restrict that contribution claim to the static filtering setting or provide a variant that mitigates the validity hacking; the perturbative verification attempted in Appendix B currently shows no separation between valid and invalid parents, so it does not yet resolve the concern.
minor comments (3)
  1. [Abstract; Section 3] The abstract states 'generate over 20 million new problem-solution pairs,' but Section 3 reports 320K generated problems and 5 million verification solutions per method; the 20M figure appears to count verifications across all four methods and should be clarified.
  2. [Section 2, Measuring data quality] The threshold rationale (b) says it 'attempt[s] to remove problems which are sometimes verified by S_theta2 but contain reasoning errors,' yet no threshold value is shown to achieve this; Figure 5 shows the opposite relationship. Please clarify this rationale in light of Figure 5.
  3. [Appendix G, Table 2] The 'Easy, invalid sample (SR=0.5625)' falls inside the accepted quality window (T_l=0.1, T_u=0.9), which nicely illustrates the inverse-validity problem; consider moving this example or its discussion into the main text.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the solve-rate quality filter is empirically validated on external benchmarks (MATH test, AIME), and no load-bearing step reduces to its own inputs by construction.

full rationale

SPARQ's load-bearing chain is: (1) define QUALITY = 1 - SOLVERATE using the student model's own rollouts, (2) filter generated problems by this score, (3) fine-tune the same student on surviving (Q, S) pairs where S is a successful self-generated verification, and (4) measure MATH/AIME performance. Step (3) is indeed a self-training loop, but every downstream claim is evaluated on held-out external benchmarks (MATH test, AIME) that are not used to construct the filter or the training set. The observed gains (38% to 47% on MATH pass@1) are therefore empirically established, not forced by the definitions. The paper itself documents an inverse correlation between solve-rate and logical validity (Section 3.1, Figure 5), which weakens the quality proxy but does not make the derivation circular; it is an empirical limitation acknowledged by the authors. Self-citations (e.g., Havrilla et al. 2024a, Samvelyan et al. 2024b) provide context or algorithmic inspiration rather than load-bearing evidence, and no equation in the paper is equivalent to its inputs by construction. The result is self-contained against external benchmarks, so the appropriate finding is no significant circularity.

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

The central claim rests on a small set of hand-chosen thresholds (T_l, T_u, K, M, k) and on three domain assumptions about answer matching, skill labeling, and mutation quality. No new physical entities or fitted constants are introduced beyond these choices.

free parameters (4)
  • Solve-rate threshold window T_l, T_u = 0.1, 0.9
    Hand-chosen bounds to discard impossible and trivial problems; no sensitivity analysis is reported (Section 3, setup).
  • Verification rollouts K = 16
    Number of Monte Carlo rollouts used per problem to estimate solve-rate; chosen without stated justification (Section 3).
  • Skill vocabulary size M and max skills k = M=100, k=3
    Diversity measure uses the 100 most frequent skills and at most 3 skills per problem (Section 3).
  • Gaussian filter standard deviation = 0.1
    In the fixed-budget ablations, samples are drawn around a target mean quality with standard deviation 0.1; this bandwidth is not motivated (Section 3.2).
assumptions (4)
  • domain assumption Final-answer matching is a valid correctness check (is_correct in Section 2).
    The solve-rate and therefore all quality scores depend on checking whether a sampled solution ends at the same numerical answer as the intended solution; reasoning errors that preserve the final answer are invisible.
  • domain assumption Gemma-2-9b-it skill classifier labels skill-sets accurately.
    Diversity is computed from classifier-assigned skills; mislabeled skill-sets would change coverage and redundancy numbers (Section 3).
  • domain assumption Mutations of MATH seed problems by Gemma-2-27b-it sample the space of useful math problems.
    The whole pipeline assumes the mutation prompt in Appendix F produces novel, solvable problems rather than paraphrases or nonsense.
  • domain assumption MATH and AIME are appropriate in-distribution and OOD proxies.
    In-distribution conclusions are measured on MATH test, which is close to the MATH train seed set, so in-distribution gains may partly reflect distribution overlap.

how reviews work

0 comments
Cite this review

Pith. "Pith review of SPARQ: Synthetic Problem Generation for Reasoning via Quality-Diversity Algorithms." pith.science (2026). https://pith.science/paper/3EFEB6YT

@misc{pith2026250606499,
  author       = {Pith},
  title        = {Pith review of: SPARQ: Synthetic Problem Generation for Reasoning via Quality-Diversity Algorithms},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/3EFEB6YT}},
  note         = {Machine review of arXiv:2506.06499}
}
read the original abstract

Large language model (LLM) driven synthetic data generation has emerged as a powerful method for improving model reasoning capabilities. However, most methods either distill large state-of-the-art models into small students or use natural ground-truth problem statements to guarantee problem statement quality. This limits the scalability of these approaches to more complex and diverse problem domains. To address this, we present SPARQ: Synthetic Problem Generation for Reasoning via Quality-Diversity Algorithms, a novel approach for generating high-quality and diverse synthetic math problem and solution pairs using only a single model by measuring a problem's solve-rate: a proxy for problem difficulty. Starting from a seed dataset of 7.5K samples, we generate over 20 million new problem-solution pairs. We show that filtering the generated data by difficulty and then fine-tuning the same model on the resulting data improves relative model performance by up to 24\%. Additionally, we conduct ablations studying the impact of synthetic data quantity, quality and diversity on model generalization. We find that higher quality, as measured by problem difficulty, facilitates better in-distribution performance. Further, while generating diverse synthetic data does not as strongly benefit in-distribution performance, filtering for more diverse data facilitates more robust OOD generalization. We also confirm the existence of model and data scaling laws for synthetically generated problems, which positively benefit downstream model generalization.

Figures

Figures reproduced from arXiv: 2506.06499 by the authors.

Figure 1
Figure 1. Diagram of the synthetic training data generation pipeline with [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Performance of the downstream Gemma-2-9B models trained on synthetic data generated with SPARQ. Left: In-distribution performance of students on MATH test. On the x-axis is the number of synthetically generated problem-solution pairs. On the y-axis is MATH performance. Each curve plots the performance of a different data generation strategy. Right: OOD performance of downstream students on the AIME benchmark after t… view at source ↗
Figure 3
Figure 3. Coverage (number of unique skill-sets discovered) vs. number of problems generated. The [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figures from the paper (7 more)
Figure 4
Figure 4. Figure 4: % of easy verifications kept versus downstream math accuracy. Filtering out easy verifica [PITH_FULL_IMAGE:figures/full_fig_p006_4.png]
Figure 5
Figure 5. Figure 5: Average problem solve-rate versus problem validity. A higher solve-rate strongly correlates [PITH_FULL_IMAGE:figures/full_fig_p007_5.png]
Figure 6
Figure 6. Figure 6: Left: In-distribution data scaling curves for various filtering strategies. On the x-axis is the number of training samples N (distinct from the number of generated problems in [PITH_FULL_IMAGE:figures/full_fig_p008_6.png]
Figure 7
Figure 7. Figure 7: Left: AIME pass@96 performance of filter methods versus number of training samples. Right: Mean training sample quality versus MATH test performance. plots the MATH test performance of models trained on subsets with different mean levels of quality. For training sets w…
Figure 8
Figure 8. Figure 8: Left:% improvement of end-to-end static self-problem generation (same model as generator and verifier). Right: Improvement from scaling problem generator model size. Gemma-2-9B acts as the student Sθ2 . In our previous experiments we used Gemma-2-27B-it as the generato…
Figure 9
Figure 9. Figure 9: Child score distributions for valid and invalid samples. [PITH_FULL_IMAGE:figures/full_fig_p014_9.png]
Figure 10
Figure 10. Figure 10: Left: Solve-rate distribution of statically generated problems. Right: Solve-rate distribu￾tion of QD generated problems. The vast majority of generated problems are either too hard (SR = 0) or too easy (SR = 1). from D to produce Dsmall. We run both algorithms to pro…

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

17 extracted references · 16 linked inside Pith

  1. [3]

    URLhttps://arxiv.org/abs/2502.00212. Alex Havrilla, Andrew Dai, Laura O’Mahony, Koen Oostermeijer, Vera Zisler, Alon Albalak, Fabrizio Milo, Sharath Chandra Raparthy, Kanishk Gandhi, Baber Abbasi, Duy Phung, Maia Iyer, Dakota Mahan, Chase Blagden, Srishti Gureja, Mohammed Hamdy, Wen-Ding Li, Giovanni Paolini, Pawan Sasanka Ammanamanchi, and Elliot Meyerso...

  2. [7]

    11 Haipeng Luo, Qingfeng Sun, Can Xu, Pu Zhao, Jianguang Lou, Chongyang Tao, Xiubo Geng, Qingwei Lin, Shifeng Chen, Yansong Tang, and Dongmei Zhang

    URLhttps://arxiv.org/abs/2401.09003. 11 Haipeng Luo, Qingfeng Sun, Can Xu, Pu Zhao, Jianguang Lou, Chongyang Tao, Xiubo Geng, Qingwei Lin, Shifeng Chen, Yansong Tang, and Dongmei Zhang. Wizardmath: Empowering mathematical reasoning for large language models via reinforced evol-instruct,

  3. [8]

    Elliot Meyerson, Mark J Nelson, Herbie Bradley, Arash Moradi, Amy K Hoover, and Joel Lehman

    URL https://arxiv.org/abs/2308.09583. Elliot Meyerson, Mark J Nelson, Herbie Bradley, Arash Moradi, Amy K Hoover, and Joel Lehman. Language model crossover: Variation through few-shot prompting.arXiv preprint arXiv:2302.12170,

  4. [10]

    Julien Pourcel, Cédric Colas, Gaia Molinaro, Pierre-Yves Oudeyer, and Laetitia Teodorescu

    URLhttps://arxiv.org/abs/2407.00695. Julien Pourcel, Cédric Colas, Gaia Molinaro, Pierre-Yves Oudeyer, and Laetitia Teodorescu. Aces: Generating diverse programming puzzles with with autotelic generative models,

  5. [11]

    Mikayel Samvelyan, Sharath Chandra Raparthy, Andrei Lupu, Eric Hambro, Aram H

    URL https://arxiv.org/abs/2310.10692. Mikayel Samvelyan, Sharath Chandra Raparthy, Andrei Lupu, Eric Hambro, Aram H. Markosyan, Manish Bhatt, Yuning Mao, Minqi Jiang, Jack Parker-Holder, Jakob Foerster, Tim Rocktäschel, and Roberta Raileanu. Rainbow teaming: Open-ended generation of diverse adversarial prompts. InAdvances in Neural Information Processing ...

  6. [12]

    URL https: //arxiv.org/abs/2312.06585. Gemma Team, Morgane Riviere, Shreya Pathak, Pier Giuseppe Sessa, Cassidy Hardin, Surya Bhupatiraju, Léonard Hussenot, Thomas Mesnard, Bobak Shahriari, Alexandre Ramé, Johan Ferret, Peter Liu, Pouya Tafti, Abe Friesen, Michelle Casbon, Sabela Ramos, Ravin Kumar, Charline Le Lan, Sammy Jerome, Anton Tsitsulin, Nino Vie...

  7. [13]

    URL https://arxiv.org/abs/2408.00118. Open Ended Learning Team, Adam Stooke, Anuj Mahajan, Catarina Barros, Charlie Deck, Jakob Bauer, Jakub Sygnowski, Maja Trebacz, Max Jaderberg, Michael Mathieu, Nat McAleese, Nathalie Bradley-Schmieg, Nathaniel Wong, Nicolas Porcel, Roberta Raileanu, Steph Hughes-Fitt, Valentin Dalibard, and Wojciech Marian Czarnecki. ...

  8. [14]

    Shubham Toshniwal, Wei Du, Ivan Moshkov, Branislav Kisacanin, Alexan Ayrapetyan, and Igor Gitman

    URLhttps://arxiv.org/abs/2107.12808. Shubham Toshniwal, Wei Du, Ivan Moshkov, Branislav Kisacanin, Alexan Ayrapetyan, and Igor Gitman. Openmathinstruct-2: Accelerating ai for math with massive open-source instruction data, 2024a. URLhttps://arxiv.org/abs/2410.01560. Shubham Toshniwal, Ivan Moshkov, Sean Narenthiran, Daria Gitman, Fei Jia, and Igor Gitman....

Show all 17 references
  1. [15]

    Longhui Yu, Weisen Jiang, Han Shi, Jincheng Yu, Zhengying Liu, Yu Zhang, James T

    URL https://arxiv.org/abs/ 2401.10034. Longhui Yu, Weisen Jiang, Han Shi, Jincheng Yu, Zhengying Liu, Yu Zhang, James T. Kwok, Zhenguo Li, Adrian Weller, and Weiyang Liu. Metamath: Bootstrap your own mathematical questions for large language models,

  2. [16]

    Xiang Yue, Xingwei Qu, Ge Zhang, Yao Fu, Wenhao Huang, Huan Sun, Yu Su, and Wenhu Chen

    URLhttps://arxiv.org/abs/2309.12284. Xiang Yue, Xingwei Qu, Ge Zhang, Yao Fu, Wenhao Huang, Huan Sun, Yu Su, and Wenhu Chen. Mammoth: Building math generalist models through hybrid instruction tuning,

  3. [17]

    Jenny Zhang, Joel Lehman, Kenneth Stanley, and Jeff Clune

    URL https://arxiv.org/abs/2309.05653. Jenny Zhang, Joel Lehman, Kenneth Stanley, and Jeff Clune. Omni: Open-endedness via models of human notions of interestingness.arXiv preprint arXiv:2306.01711,

  4. [2015]

    Gabriel Poesia, David Broman, Nick Haber, and Noah D

    URL https://arxiv.org/abs/1504.04909. Gabriel Poesia, David Broman, Nick Haber, and Noah D. Goodman. Learning formal mathematics from intrinsic motivation,

  5. [2021]

    Joel Lehman, Jonathan Gordon, Shawn Jain, Kamal Ndousse, Cathy Yeh, and Kenneth O

    URL https://arxiv.org/abs/2103.03874. Joel Lehman, Jonathan Gordon, Shawn Jain, Kamal Ndousse, Cathy Yeh, and Kenneth O. Stanley. Evolution through large models,

  6. [2022]

    Chengpeng Li, Zheng Yuan, Hongyi Yuan, Guanting Dong, Keming Lu, Jiancan Wu, Chuanqi Tan, Xiang Wang, and Chang Zhou

    URLhttps://arxiv.org/abs/2206.08896. Chengpeng Li, Zheng Yuan, Hongyi Yuan, Guanting Dong, Keming Lu, Jiancan Wu, Chuanqi Tan, Xiang Wang, and Chang Zhou. Mugglemath: Assessing the impact of query and response augmentation on math reasoning,

  7. [2023]

    Wang Chao, Jiaxuan Zhao, Licheng Jiao, Lingling Li, Fang Liu, and Shuyuan Yang

    URLhttps://arxiv.org/abs/2310.13032. Wang Chao, Jiaxuan Zhao, Licheng Jiao, Lingling Li, Fang Liu, and Shuyuan Yang. A match made in consistency heaven: when large language models meet evolutionary algorithms.arXiv preprint arXiv:2401.10510,

  8. [2024]

    Zi Lin, Sheng Shen, Jingbo Shang, Jason Weston, and Yixin Nie

    URLhttps://arxiv.org/abs/2310.05506. Zi Lin, Sheng Shen, Jingbo Shang, Jason Weston, and Yixin Nie. Learning to solve and verify: A self-play framework for code and test generation,

  9. [2025]

    Kefan Dong and Tengyu Ma

    URLhttps://arxiv.org/abs/2501.12948. Kefan Dong and Tengyu Ma. Stp: Self-play llm theorem provers with iterative conjecturing and proving,

Pith tools

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