Pith. sign in

REVIEW 4 major objections 4 minor 43 references

Towards Generating Controllable and Solvable Geometry Problem by Leveraging Symbolic Deduction Engine

T0 review · 4 major / 4 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 A pipeline built on a symbolic deduction engine generates Euclidean geometry problems that are readable, solvable, and controllable by the choice of knowledge points and difficulty level.

desk verdict A useful new task and a working pipeline that overclaims controllability; the checking-function results don't match the stated guarantees. read the letter →

arxiv 2506.02565 v1 pith:BV62EWMK submitted 2025-06-03 cs.AI

Zhuoxuan Jiang , Tianyang Zhang , Peiyan Peng , Jing Chen , Yinong Xun , Haotian Zhang , Lichi Li , Yong Li
show 1 more author
Shaohua Zhang
This is my paper
classification cs.AI
keywords geometryproblemgenerationsymbolicdeductionengineeducationalquestioncontrollablesolvabilityEuclideanknowledgepointmappingAlpha
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

Geometry problems are hard to generate automatically because they require multi-modal output (text plus diagram) and a strict chain of theorem applications. This paper claims that a symbolic deduction engine, an automated program that proves geometry facts by applying formal rules step by step, can be run in reverse to create such problems with controlled knowledge points and difficulty. The proposed SDE-GPG pipeline samples formal definitions from a precomputed mapping table, lets the engine deduce a conclusion, and then applies a checking function that keeps only problems whose proof path is shortest, complete, and difficulty-consistent. The upshot would be a practical generator for teachers and students that produces a textual problem, a diagram, and a step-by-step answer on demand.

What carries the argument

The load-bearing machinery is the Knowledge Point-to-exDefinition Mapping Table (K2exD-MT) together with the checking function. The table is built offline by sampling minimal combinations of 68 formal definitions, running the engine over 100,000 iterations, and recording which of 43 knowledge points were used in each deduction; it lets the generator sample formal inputs that are already correlated with target knowledge points, avoiding natural-language-to-formal translation bias. The checking function then enforces four quality constraints on deduced reasoning paths, namely shortest path, completeness of knowledge points, completeness of clauses, and difficulty consistency, so that only controllable and solvable problems proceed to text and diagram generation.

What would settle it

Take a knowledge-point combination whose natural proof requires a theorem outside the engine's 43 rules (Appendix A's Example 3 is such a case) and run the full pipeline with the checking function on it; if the pipeline either outputs nothing or needs many more steps than an independent prover such as a full JGEX search to reach the conclusion, the completeness assumption that grounds the checker's shortest-path guarantee is violated.

Watch

Extended reading notes

Core claim

The central claim is that the SDE-GPG framework can generate readable, solvable, and controllable geometry problems. Starting from a user-chosen set of knowledge points and a difficulty level, the pipeline looks up candidate formal definitions in a knowledge point-to-extended-definition mapping table, runs a symbolic deduction engine to derive a conclusion, and filters the resulting reasoning paths: only shortest paths that use all required knowledge points, use all clauses, and match the difficulty level survive. The survivors are translated into natural-language clauses and a question through templates, and into a diagram by rule-based sequential drawing. On knowledge-point combinations curated from two public datasets, human evaluation found that the checked method reaches native solvability 1.00 on JGEX-AG-231 and 0.96 on GeoQA, with higher completeness of clauses and knowledge points than an LLM baseline and an unchecked version.

Load-bearing premise

The pipeline assumes that the fixed 43-rule symbolic engine contains every theorem any generated problem could need, because if a needed intermediate theorem is missing, the engine either finds a longer path and the checker rejects the problem, or fails to produce a conclusion at all.

Editorial extensions

If this is right

  • With the checking function enabled, every generated problem on the JGEX-AG-231 combination set came with a shortest, solvable proof path, and all clauses were used in the proof.
  • Because generation starts from formal definitions rather than natural language, the pipeline sidesteps the autoformalization errors that plague LLM-based problem generation; the paper's GPT-4o baseline produced logically incorrect problems.
  • The mapping table's one-to-many structure means a single knowledge point can yield thousands of distinct problem instances, supporting large-scale variation for practice or assessment.
  • Controlling knowledge points and difficulty makes the generator usable for targeted exercise design: a teacher can request a problem exercising a specific theorem at a chosen difficulty.

Reading between the lines

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

  • The checking function is a general quality filter, not tied to SDE generation; feeding LLM-generated problems through the same shortest-path and completeness checks could flag unsolvable or redundant exercises, a testable use beyond this paper.
  • Because the mapping table is built by random sampling with n=2 and 100,000 iterations, knowledge points with few recorded entries may be underrepresented; increasing sampling or using targeted sampling should raise generation yield for those points.
  • The guarantee of solvability is relative to the engine's 43-rule library, not absolute; an independent prover with more theorems could find a shorter path than the engine, as Appendix A's Example 3 illustrates. Verifying generated proofs with a second, richer prover would measure how often the shortest-path claim is conservative.
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 / 4 minor

Summary. The paper introduces a pipeline, SDE-GPG, for generating Euclidean geometry problems with user-specified knowledge points and difficulty levels. The pipeline samples extended definitions via a precomputed mapping table, runs an AlphaGeometry-style symbolic deduction engine to derive conclusions and proof paths, filters candidate problems through a checking function, and translates the formal results into natural-language text and diagrams. The authors evaluate the generated problems on two curated datasets (JGEX-AG-231 and a subset of GeoQA) via human scoring of readability, solvability, and controllability, comparing with GPT-4o and with the pipeline without checking. The central claim is that the method effectively generates readable, solvable, and controllable geometry problems, with the checking function purportedly guaranteeing completeness of knowledge points and difficulty consistency.

Significance. If the pipeline worked as claimed, it would be a useful contribution to educational question generation and synthetic data augmentation for geometry, areas where few generative systems exist. The paper's strengths include leveraging a symbolic deduction engine to tie problem generation to formal proofs, releasing code/data/resources, and providing detailed case studies that honestly acknowledge failures. However, the central claim of controllability is weakened by the reported metrics: the checking function is stated to enforce completeness of knowledge points and difficulty consistency, yet human-rated scores on these very dimensions are far from perfect (CKP=0.62, CD=0.63 on JGEX-AG-231; CKP=0.94, CD=0.47 on GeoQA). Additionally, Example 3 shows that the symbolic engine's incompleteness can cause non-shortest, flawed proofs to pass the checking function. These issues are load-bearing for the paper's main message, but they are addressable through more careful claims and additional analyses.

major comments (4)
  1. [§4.3, Tables 1–2] The checking function fcheck is described as accepting only reasoning paths that are shortest, involve all required knowledge points, involve all exDefinitions, and match the requested difficulty by path length. If these constraints were enforced, the human-rated CKP and CD for SDE-PGP w/ checking should be near 1.00. Instead, Table 1 reports CKP=0.62 and CD=0.63 on JGEX-AG-231, and Table 2 reports CKP=0.94 and CD=0.47 on GeoQA. This discrepancy is not addressed in the paper. The authors must explain how a problem can pass fcheck yet be judged by expert annotators as lacking required knowledge points or as having inconsistent difficulty. Possible resolutions include: fcheck does not actually enforce constraints (2) and (4) as written; the formal rule codes do not correspond to human-understood knowledge points; or the path-length-based difficulty bands do not align with expert judgment. Without such an explanation, the abstract's claim of "guarantees to control ... knowledge points and difficulties" is not supported.
  2. [Appendix A, Example 3] Example 3 demonstrates that the checking function's shortest-path requirement is only valid relative to the symbolic deduction engine's fixed rule set. The engine misses a one-step theorem, so the generated problem has an unnecessarily long proof that nevertheless passes the shortest-path filter. The paper acknowledges this as an "occasional problematic output," but it directly limits the core guarantee that filtered problems are solvable in the intended way or have minimal proofs. The authors should either restrict generation to knowledge-point combinations for which the engine's rule set is known to be complete, or add a verification step that checks proof minimality with respect to a more complete theorem repository. Otherwise, the filtering step cannot guarantee the quality it is claimed to provide.
  3. [§5.2, §5.3] The evaluation lacks basic statistical rigor. Only average scores are reported, with no confidence intervals, significance tests, or inter-annotator agreement. The paper states that one problem is generated per input test sample, but it does not report how many generated problems survived the checking filter and were actually evaluated. Without this information, the high native solvability scores (1.00 and 0.96) and other metrics cannot be assessed for stability, and the comparisons between methods (GPT-4o, SDE-PGP with/without checking) are not supported by any measure of uncertainty. The authors should report per-sample scores, variance, and agreement statistics, and specify the exact evaluation set sizes.
  4. [§5.2.1, §5.3] The difficulty control is empirically weak: CD=0.63 on JGEX-AG-231 and CD=0.47 on GeoQA for the checking method mean that a large fraction of problems are judged inconsistent with the requested difficulty. The difficulty bands (Easy: <10 steps, Moderate: 10–20 steps, Difficult: >20 steps) are arbitrary and not validated against human perception. The low CD scores suggest that path length is not a reliable proxy for difficulty. This undermines the controllability claim, and the paper should either develop a more principled difficulty model, calibrate the thresholds with human judgments, or explicitly limit the claim to formal path-length difficulty rather than perceived difficulty.
minor comments (4)
  1. [Throughout] There are several typos and inconsistencies: "anew" should be "a new" (Contributions); "automatically drew" should be "automatically drawn" (Abstract); the framework is called SDE-GPG in the title/abstract but SDE-PGP in Tables 1–2 and elsewhere; "w/ checking" vs "with checking" is used inconsistently.
  2. [§5.1] The dataset description is incomplete: for GeoQA, the paper says 100 problems are selected from the plane geometry subset, but it does not specify how many generated problems were actually produced and evaluated, nor how many source problems from JGEX-AG-231 yielded qualified problems after checking.
  3. [§5.2.2] The human evaluation protocol would benefit from a clearer description of how the independent judges were calibrated, whether the arbiter resolved all disagreements, and whether the evaluators were blinded to the generating method. This would help assess the reliability of the reported scores.
  4. [Appendix A, Example 3] The paper states that the problematic output in Example 3 is "occasional" but provides no frequency estimate. Given that the checking function was designed to filter exactly such cases, the authors should quantify how often the SDE's incompleteness leads to accepted non-shortest paths, since this affects the practical reliability of the framework.

Circularity Check

2 steps flagged · score 6.0 of 10

Solvability and controllability scores are written into the checking function's acceptance predicates, and the CKP/CD results actually show the formal filter does not match expert judgment.

  1. self definitional [Section 4.3 (Problem Qualification Checking) and Section 5.3 (Results for Solvability)]
    "After obtaining candidate problems, based on control variables, unqualified problems would be filtered out, which means that the qualified reasoning paths should (1) be shortest paths, (2) involve all the required knowledge points (i.e., completeness of knowledge points), (3) involve all the exDefinitions to reach conclusions (i.e., completeness of clauses), and (4) be consistent with the given difficulty degree (i.e., consistency of difficulty) in terms of the length of paths."

    Algorithm 2 applies f_check only to outputs of f_engine and proceeds only when the qualified-reasoning-path set is non-empty, so every accepted problem carries a formal deduction from its exDefinitions to the question. Native Solvability is defined as 'whether the generated problem can be solved,' and Section 5.3 cites NS=1.00/0.96 as evidence. This is the filter's own acceptance condition restated as an experimental result; the formal deduction was not independently predicted but was required before the problem was emitted.

  2. self definitional [Section 4.3 and Section 5.2.1 / 5.3]
    "Completeness of Knowledge Points (CKP): Whether all the required knowledge points are involved in solving the problem. ... Consistency of Difficulty (CD): Whether the length of reasoning path is consistent with the required difficulty degree. ... SDE-PGP w/ checking consistently achieves higher completeness of knowledge points (CKP) and consistency of difficulty (CD) than the baselines on both datasets, validating the effectiveness of the proposed checking function."

    CKP and CD are the same predicates that f_check was built to enforce: Section 4.3 requires paths to 'involve all the required knowledge points (i.e., completeness of knowledge points)' and to be 'consistent with the given difficulty degree (i.e., consistency of difficulty) in terms of the length of paths.' The generated problem's answer is the accepted reasoning path, so these metrics inspect the filter's own output rather than an independent generative property. The non-perfect human scores (Table 1: CKP=0.62, CD=0.63; Table 2: CKP=0.94, CD=0.47) show the formal filter and expert judgment diverge, so the claimed 'guarantee' of knowledge-point and difficulty control is neither a theorem nor an empirically established property.

full rationale

The two central quantitative claims that the generated problems are solvable and controllable reduce, at the formal level, to the checking function's own filter predicates. f_check rejects any candidate whose SDE run has no conclusion, then only those accepted candidates are translated and evaluated; hence near-perfect Native Solvability is an artifact of acceptance sampling rather than an independent generative discovery. Likewise, the controllability metrics CKP and CD are word-for-word the constraints enumerated in Section 4.3, so using them to 'validate' the checking function is circular: if the filter worked perfectly the scores would be 1.0 by construction, and the reported sub-1.0 values show the formal rule codes do not coincide with human-understood knowledge points and difficulty. Appendix A, Example 3 additionally concedes that the engine's missing intermediate theorems produce non-shortest paths that the checker must reject, so solvability itself depends on external engine coverage rather than on the generator's guarantee. There is no load-bearing self-citation: the SDE is AlphaGeometry's public engine and the datasets are public. The human readability ratings and rule-based translation are independent contributions, but they do not make the solvability/controllability evaluation non-circular. Overall partial circularity in the central claim: score 6.

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

The evaluation depends on external AlphaGeometry resources plus hand-chosen thresholds. The 'checking function' is a rejection filter rather than a fitted model, so there is no parameter fitting to data; however, the difficulty thresholds (10 and 20 steps) and table construction parameters n and T are hand-set and directly affect the controllability results.

free parameters (4)
  • Difficulty step thresholds = 10 and 20 reasoning steps
    Empirically set: Easy is less than 10 steps, Moderate is 10 to 20 steps, Difficult is more than 20 steps (Section 5.2.1). These thresholds define the difficulty control variable and the Consistency of Difficulty metric.
  • Number of definitions sampled per table-building iteration = n=2
    Algorithm 1 samples n=2 definitions from D in each of T iterations to construct the K2exD-MT (Section 4.1).
  • Number of table construction iterations = T=100,000
    Algorithm 1 runs 100,000 iterations to build the K2exD-MT (Section 4.1).
  • Knowledge points sampled per source problem = Fewer than 5
    For JGEX-AG-231, the authors randomly sample fewer than five knowledge points per problem to reduce complexity (Section 5.1), which shapes the evaluation difficulty distribution.
assumptions (4)
  • domain assumption AlphaGeometry SDE correctness and coverage
    The pipeline relies on f_engine from AlphaGeometry (Trinh et al., 2024) with 68 definitions and 43 rules. Example 3 in Appendix A shows the engine misses intermediate theorems, so coverage is partial.
  • domain assumption K2exD-MT completeness
    The mapping table is built by random sampling for 100,000 iterations; if a given knowledge point lacks a usable exDefinition set in the table, no problem is generated for that control input.
  • domain assumption Template translation correctness
    f_text and f_diagram use predefined templates and rule-based drawing; Section 4.4 admits diagrams sometimes do not align with human conventions, and DC scores are low.
  • domain assumption Human evaluation validity
    Three expert judges with an arbiter score the generated problems; no inter-annotator agreement or statistical significance is reported.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Towards Generating Controllable and Solvable Geometry Problem by Leveraging Symbolic Deduction Engine." pith.science (2026). https://pith.science/paper/BV62EWMK

@misc{pith2026250602565,
  author       = {Pith},
  title        = {Pith review of: Towards Generating Controllable and Solvable Geometry Problem by Leveraging Symbolic Deduction Engine},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/BV62EWMK}},
  note         = {Machine review of arXiv:2506.02565}
}
read the original abstract

Generating high-quality geometry problems is both an important and challenging task in education. Compared to math word problems, geometry problems further emphasize multi-modal formats and the translation between informal and formal languages. In this paper, we introduce a novel task for geometry problem generation and propose a new pipeline method: the Symbolic Deduction Engine-based Geometry Problem Generation framework (SDE-GPG). The framework leverages a symbolic deduction engine and contains four main steps: (1) searching a predefined mapping table from knowledge points to extended definitions, (2) sampling extended definitions and performing symbolic deduction, (3) filtering out unqualified problems, and (4) generating textual problems and diagrams. Specifically, our method supports to avoid inherent biases in translating natural language into formal language by designing the mapping table, and guarantees to control the generated problems in terms of knowledge points and difficulties by an elaborate checking function. With obtained formal problems, they are translated to natural language and the accompanying diagrams are automatically drew by rule-based methods. We conduct experiments using real-world combinations of knowledge points from two public datasets. The results demonstrate that the SDE-GPG can effectively generate readable, solvable and controllable geometry problems.

Figures

Figures reproduced from arXiv: 2506.02565 by the authors.

Figure 1
Figure 1. A typical geometry problem consists of a [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Pipeline of proposed Symbolic Deduction Engine-based Geometry Problem Generation Framework [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

43 extracted references · 28 canonical work pages

  1. [1]

    Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan, and Anand Tadipatri. 2022. Towards a mathematics formalisation assistant using large language models. arXiv preprint arXiv:2211.07524

    arXiv 2022

  2. [2]

    Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q Jiang, Jia Deng, Stella Biderman, and Sean Welleck. 2023. Llemma: An open language model for mathematics. arXiv preprint arXiv:2310.10631

    arXiv 2023

  3. [3]

    Kshitij Bansal and Christian Szegedy. 2020. Learning alignment between formal & informal mathematics. In 5th Conference on Artificial Intelligence and Theorem Proving

    work page 2020

  4. [4]

    Matthew L Bernacki and Candace Walkington. 2018. The role of situational interest in personalized learning. Journal of Educational Psychology, 110(6):864

    work page 2018

  5. [5]

    Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. 2020. Language models are few-shot learners. NeurIPS, 33:1877--1901

    work page 2020

  6. [6]

    Tianyang Cao, Shuang Zeng, Xiaodan Xu, Mairgup Mansur, and Baobao Chang. 2022. Disk: Domain-constrained instance sketch for math word problem generation. arXiv preprint arXiv:2204.04686

    work page Pith review arXiv 2022

  7. [7]

    Shang-Ching Chou, Xiao-Shan Gao, and Jing-Zhong Zhang. 2000. A deductive database approach to automated geometry theorem proving and discovering. Journal of Automated Reasoning, 25(3):219--246

    work page 2000

  8. [8]

    Bryan Christ, Jonathan Kropko, and Thomas Hartvigsen. 2024. Mathwell: Generating educational math word problems using teacher annotations. In EMNLP 2024, pages 11914--11938

    work page 2024

Show all 43 references
  1. [9]

    Garett Cunningham, Razvan C Bunescu, and David Juedes. 2023. Towards autoformalization of mathematics and code correctness: Experiments with elementary proofs. arXiv preprint arXiv:2301.02195

    2023 arXiv

  2. [10]

    Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. 2015. The lean theorem prover (system description). In CADE, pages 378--388

    2015

  3. [11]

    Vlad Firoiu, Eser Aygun, Ankit Anand, Zafarali Ahmed, Xavier Glorot, Laurent Orseau, Lei Zhang, Doina Precup, and Shibl Mourad. 2021. Training a first-order theorem prover from synthetic data. arXiv preprint arXiv:2103.03798

    2021 arXiv

  4. [12]

    Siddhartha Gadgil, Anand Rao Tadipatri, Ayush Agrawal, Ashvni Narayanan, and Navin Goyal. 2022. Towards automating formalisation of theorem statements using large language models. In NeurIPS 2022 Workshop on MATH-AI

    2022

  5. [13]

    Guher Gorgun and Okan Bulut. 2024. Instruction-tuned large-language models for quality control in automatic item generation: A feasibility study. Educational Measurement: Issues and Practice

    2024

  6. [14]

    Wu-Yuin Hwang and Ika Qutsiati Utami. 2024. Using gpt and authentic contextual recognition to generate math word problems with difficulty levels. Education and Information Technologies, pages 1--29

    2024

  7. [15]

    Tetsuo Ida and Jacques Fleuriot. 2013. Automated Deduction in Geometry. Springer

    2013

  8. [16]

    Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timoth \'e e Lacroix, Yuhuai Wu, and Guillaume Lample. 2022. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210.12283

    2022 arXiv

  9. [17]

    Ying Jiao, Kumar Shridhar, Peng Cui, Wangchunshu Zhou, and Mrinmaya Sachan. 2023. Automatic educational question generation with difficulty level controls. In AIED, pages 476--488

    2023

  10. [18]

    Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. 2022. Hypertree proof search for neural theorem proving. NeurIPS, 35:26337--26349

    2022

  11. [19]

    Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, et al. 2022. Solving quantitative reasoning problems with language models. NeurIPS, 35:3843--3857

    2022

  12. [20]

    cone of experience

    Sannyuya Liu, Jintian Feng, Zongkai Yang, Yawei Luo, Qian Wan, Xiaoxuan Shen, and Jianwen Sun. 2024. Comet:“cone of experience” enhanced large multimodal model for mathematical problem generation. Science China Information Sciences, 67(12):1--2

    2024

  13. [21]

    Tianqiao Liu, Qiang Fang, Wenbiao Ding, Hang Li, Zhongqin Wu, and Zitao Liu. 2020. Mathematical word problem generation from commonsense knowledge graph and equations. arXiv preprint arXiv:2010.06196

    2020 arXiv

  14. [22]

    Leonardo de Moura and Sebastian Ullrich. 2021. The lean 4 theorem prover and programming language. In CADE, pages 625--635

    2021

  15. [23]

    Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si. 2024. Autoformalizing euclidean geometry. arXiv preprint arXiv:2405.17216

    2024 arXiv

  16. [24]

    Kole Norberg, Husni Almoubayyed, Stephen E Fancsali, Logan De Ley, Kyle Weldon, April Murphy, and Steve Ritter. 2023. Rewriting math word problems with large language models. Grantee Submission

    2023

  17. [25]

    Nilay Patel, Rahul Saha, and Jeffrey Flanigan. 2023. A new approach towards autoformalization. arXiv preprint arXiv:2310.07957

    2023 arXiv

  18. [26]

    Auguste Poiroux, Gail Weiss, Viktor Kun c ak, and Antoine Bosselut. 2024. Improving autoformalization using type checking. arXiv preprint arXiv:2406.07222

    2024

  19. [27]

    Oleksandr Polozov, Eleanor O'Rourke, Adam M Smith, Luke Zettlemoyer, Sumit Gulwani, and Zoran Popovi \'c . 2015. Personalized mathematical word problem generation. In IJCAI

    2015

  20. [28]

    Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. 2022. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344

    2022 arXiv

  21. [29]

    Longhu Qin, Jiayu Liu, Zhenya Huang, Kai Zhang, Qi Liu, Binbin Jin, and Enhong Chen. 2023. A mathematical word problem generator with structure planning and knowledge enhancement. In SIGIR, pages 1750--1754

    2023

  22. [30]

    Wei Qin, Xiaowei Wang, Zhenzhen Hu, Lei Wang, Yunshi Lan, and Richang Hong. 2024. Math word problem generation via disentangled memory retrieval. ACM TKDD, 18(5):1--21

    2024

  23. [31]

    Colin Raffel, Noam Shazeer, Adam Roberts, Katherine Lee, Sharan Narang, Michael Matena, Yanqi Zhou, Wei Li, and Peter J Liu. 2020. Exploring the limits of transfer learning with a unified text-to-text transformer. JMLR, 21(140):1--67

    2020

  24. [32]

    Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. 2024. Solving olympiad geometry without human demonstrations. Nature, 625(7995):476--482

    2024

  25. [33]

    Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, et al. 2023. Lego-prover: Neural theorem proving with growing libraries. arXiv preprint arXiv:2310.00656

    2023 arXiv

  26. [34]

    Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. 2018. First experiments with neural translation of informal to formal mathematics. In Intelligent Computer Mathematics, pages 255--270

    2018

  27. [35]

    Zichao Wang, Andrew S Lan, and Richard G Baraniuk. 2021. Math word problem generation with mathematical consistency and problem context constraints. arXiv preprint arXiv:2109.04546

    2021 arXiv

  28. [36]

    Qinzhuo Wu, Qi Zhang, and Xuanjing Huang. 2022 a . Automatic math word problem generation with topic-expression co-attention mechanism and reinforcement learning. TASLP, 30:1061--1072

    2022

  29. [37]

    Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. 2022 b . Autoformalization with large language models. NeurIPS, 35:32353--32368

    2022

  30. [38]

    Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. 2024. Leandojo: Theorem proving with retrieval-augmented language models. NeurIPS, 36

    2024

  31. [39]

    Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. 2024. Lean workbook: A large-scale lean problem set formalized from natural language math problems. arXiv preprint arXiv:2406.03847

    2024 arXiv

  32. [40]

    Xueliang Zhao, Lin Zheng, Haige Bo, Changran Hu, Urmish Thakker, and Lingpeng Kong. 2024. Subgoalxl: Subgoal-based expert learning for theorem proving. arXiv preprint arXiv:2408.11172

    2024 arXiv

  33. [41]

    Zihao Zhou, Maizhen Ning, Qiufeng Wang, Jie Yao, Wei Wang, Xiaowei Huang, and Kaizhu Huang. 2023. Learning by analogy: Diverse questions generation in math word problem. arXiv preprint arXiv:2306.09064

    2023 arXiv

  34. [42]

    online" 'onlinestring :=

    ENTRY address archivePrefix author booktitle chapter edition editor eid eprint eprinttype howpublished institution journal key month note number organization pages publisher school series title type volume year doi pubmed url lastchecked label extra.label sort.label short.list...

  35. [43]

    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 7, 2026 · model on record in the stance chip above.