Elamur Research⌕
☰
home / papers / 2026 / Reliable Use of Lemmas via Eligibility Reasoning and Section-Aware Reinforcement Learning

Reliable Use of Lemmas via Eligibility Reasoning and Section-Aware Reinforcement Learning

Paper · 2026 · Zhikun Xu, Xiaodong Yu, Ben Zhou et al.

Summary

Large language models can score well on math benchmarks yet still invoke lemmas whose hypotheses do not hold in the given context. The authors frame this as a lemma-judging task. For each pairing of a statement with a proposed lemma, the model produces two distinct sections. One checks whether the lemma's preconditions are satisfied, and the other checks whether its conclusion helps the goal. The final usefulness label is the logical AND of the two. Their framework, RULES, trains this two-part output with GRPO plus section-aware loss masking. When an error can be traced to one section, only that section's tokens are penalized. Training uses NaturalProofs, NLPS, Isabelle premise selection and IMO-lemmas, plus a small set of perturbations that make lemmas inapplicable. Across four base models, RULES beats both the untrained model and single-label GRPO on in-domain judging. The biggest gains appear on a held-out DeepTheorem perturbation suite. Results on end-to-end math benchmarks are mixed, which the authors attribute to a precision/recall tradeoff. The work matters as a targeted way to make models verify before they apply a lemma.

Key points

  • Base models are DeepMath-1.5B, OLMo-2-1124-7B-Instruct, Qwen2.5-Math-7B-Instruct and Llama-3.1-8B-Instruct. Each is compared in three versions: vanilla, single-label GRPO and RULES.
  • The training set includes 744 filtered applicability-breaking examples that carry only precondition labels. Fine-grained masking therefore covers roughly 5.7% of the core corpus scale. Rewards are +1 for correct, −1 for incorrect, and −2 for outputs that fail to parse.
  • On the deeptheorem-perturbation test, RULES gains up to about 23 points. For example, DeepMath rises from 24 (vanilla) and 35.6 (GRPO) to 47, and OLMo2 rises from 46.8 (GRPO) to 60.5.
  • In ablations on Qwen2.5-Math, removing perturbation data drops the perturbation score to 19.1, compared with 87.8 for full RULES. Emitting both judgments at the end ("two-section-onetime") lowers it by 14.7 points.
  • End-to-end benchmarks (Putnam-Axiom, CounterMATH, IneqMath, MATH-Perturb, TheoremQA) show parity with or small gains over GRPO, with some regressions. The study is limited to English and mid-sized models.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Arizona State UniversityTempe · United States54 works · 2,356 citations🏢Advanced Micro DevicesSunnyvale · United States3 works

 Fields, topics and concepts

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 18,614 worksArtificial Intelligence · 17,965 worksArts and Humanities · 17,450 worksLanguage and Linguistics · 17,296 worksInformation Systems · 1,730 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,685 works

💡 Concepts 1Key ideas and methods explained on our concept pages.Lemma · 24 works

Cite

Cite as Zhikun Xu, Xiaodong Yu, Ben Zhou, Jiang Liu, Jialian Wu, Ze Wang, Ximeng Sun, Hao Chen and Zicheng Liu. 2026. Reliable Use of Lemmas via Eligibility Reasoning and Section-Aware Reinforcement Learning. Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 2: Short Papers).

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.18653/v1/2026.acl-short.20

@inproceedings{xu2026reliable,
  title = {{Reliable Use of Lemmas via Eligibility Reasoning and Section-Aware Reinforcement Learning}},
  author = {Zhikun Xu, Xiaodong Yu, Ben Zhou, Jiang Liu, Jialian Wu, Ze Wang, Ximeng Sun, Hao Chen and Zicheng Liu},
  booktitle = {Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 2: Short Papers)},
  year = {2026},
  doi = {10.18653/v1/2026.acl-short.20},
  url = {https://doi.org/10.18653/v1/2026.acl-short.20}
}

References

35 references, 14 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Mislav Balunovic, Jasper Dekoninck, Ivo Petrov, Nikola Jovanović, and Martin Vechev. 2025. Matharena: Evaluating LLMs on uncontaminated math competitions. In The Thirty-ninth Annual Conference on Neural Information Processing Systems Datasets and Benchmarks Track.
  2. Wenhu Chen, Ming Yin, Max Ku, Pan Lu, Yixin Wan, Xueguang Ma, Jianyu Xu, Xinyi Wang, and Tony Xia. 2023. TheoremQA: A theorem-driven question answering dataset. In Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, pages 7889–7901, Singapore. Association for Comp…
  3. Xinyun Chen, Ryan A Chi, Xuezhi Wang, and Denny Zhou. 2024. Premise order matters in reasoning with large language models. In Proceedings of the 41st International Conference on Machine Learning, pages 6596–6620. find
  4. Jasper Dekoninck, Ivo Petrov, Kristian Minchev, Miroslav Marinov, Maria Drencheva, Lyuba Konova, Milen Milenov Shumanov, Kaloyan Tsvetkov, Nikolay Drenchev, Lazar D. Todorov, Kalina Nikolova, Nikolay Georgiev, Vanesa Kalinkova, Margulan Ismoldayev, Mislav Balunovic, and Martin Vechev. 2025. The open…
  5. Deborah Ferreira and André Freitas. 2020. Natural language premise selection: Finding supporting statements for mathematical text. In Proceedings of the Twelfth Language Resources and Evaluation Conference, pages 2175–2182, Marseille, France. European Language Resources Association. find
  6. Simon Frieder, Julius Berner, Philipp Petersen, and Thomas Lukasiewicz. 2024. Large language models for mathematicians. Preprint, arXiv:2312.04556. — [arXiv:2312.04556](https://arxiv.org/abs/2312.04556) find
  7. Aaron Grattafiori, Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Alex Vaughan, Amy Yang, Angela Fan, Anirudh Goyal, Anthony Hartshorn, Aobo Yang, Archi Mitra, Archie Sravankumar, Artem Korenev, Arthur Hinsvark, and 542 o… — The Llama 3 Herd of Models
  8. Aryan Gulati, Brando Miranda, Eric Chen, Emily Xia, Kai Fronsdal, Bruno de Moraes Dumont, and Sanmi Koyejo. 2024. Putnam-AXIOM: A functional and static benchmark for measuring higher level mathematical reasoning. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24. find
  9. Dadi Guo, Jiayu Liu, Zhiyuan Fan, Zhitao He, Haoran Li, Yumeng Wang, and Yi R. Fung. 2025. Mathematical proof as a litmus test: Revealing failure modes of advanced large reasoning models. Preprint, arXiv:2506.17114.
  10. Zhiwei He, Tian Liang, Jiahao Xu, Qiuzhi Liu, Xingyu Chen, Yue Wang, Linfeng Song, Dian Yu, Zhenwen Liang, Wenxuan Wang, Zhuosheng Zhang, Rui Wang, Zhaopeng Tu, Haitao Mi, and Dong Yu. 2025. Deepmath-103k: A large-scale, challenging, decontaminated, and verifiable mathematical dataset for advancing…
  11. Kaixuan Huang, Jiacheng Guo, Zihao Li, Xiang Ji, Jiawei Ge, Wenzhe Li, Yingqing Guo, Tianle Cai, Hui Yuan, Runzhe Wang, Yue Wu, Ming Yin, Shange Tang, Yangsibo Huang, Chi Jin, Xinyun Chen, Chiyuan Zhang, and Mengdi Wang. 2025. MATH-perturb: Benchmarking LLMs’ math reasoning abilities against hard pe… find
  12. Woosuk Kwon, Zhuohan Li, Siyuan Zhuang, Ying Sheng, Lianmin Zheng, Cody Hao Yu, Joseph E. find
  13. Gonzalez, Hao Zhang, and Ion Stoica. 2023. Efficient memory management for large language model serving with pagedattention. In Proceedings of the ACM SIGOPS 29th Symposium on Operating Systems Principles.
  14. Vincent Li, Tim Knappe, Yule Fu, Kevin Han, and Kevin Zhu. 2025a. Automating mathematical proof generation using large language model agents and knowledge graphs. arXiv preprint arXiv:2503.11657. find
  15. Yinghui Li, Jiayi Kuang, Haojing Huang, Zhikun Xu, Xinnian Liang, Yi Yu, Wenlian Lu, Yangning Li, Xiaoyu Tan, Chao Qu, Ying Shen, Hai-Tao Zheng, and Philip S. Yu. 2025b. One example shown, many concepts known! counterexample-driven conceptual reasoning in mathematical LLMs. In Forty-second Internati… find
  16. Zhenwen Liang, Linfeng Song, Yang Li, Tao Yang, Feng Zhang, Haitao Mi, and Dong Yu. 2025. Towards solving more challenging imo problems via decoupled reasoning and proving. arXiv preprint. find
  17. Maciej Mikuła, Szymon Antoniak, Szymon Tworkowski, Bartosz Piotrowski, Albert Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu. 2023. Magnushammer: A transformer-based approach to premise selection. In The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS… find
  18. Sagnik Mukherjee, Abhinav Chinta, Takyoung Kim, Tarun Anoop Sharma, and Dilek Hakkani Tur. 2025. Premise-augmented reasoning chains improve error identification in math reasoning with llms. In Forty-second International Conference on Machine Learning. find
  19. Team OLMo, Pete Walsh, Luca Soldaini, Dirk Groeneveld, Kyle Lo, Shane Arora, Akshita Bhagia, Yuling Gu, Shengyi Huang, Matt Jordan, Nathan Lambert, Dustin Schwenk, Oyvind Tafjord, Taira Anderson, David Atkinson, Faeze Brahman, Christopher Clark, Pradeep Dasigi, Nouha Dziri, and 21 others. 2025. 2 ol… find
  20. OpenAI, Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, Red Avila, Igor Babuschkin, Suchir Balaji, Valerie Balcom, Paul Baltescu, Haiming Bao, Mohammad Bavarian, Jeff Belgum, and 262 others.… — GPT-4 Technical Report
  21. Zhuoshi Pan, Yu Li, Honglin Lin, Qizhi Pei, Zinan Tang, Wei Wu, Chenlin Ming, H. Vicky Zhao, Conghui He, and Lijun Wu. 2025. LEMMA: Learning from errors for MatheMatical advancement in LLMs. In Findings of the Association for Computational Linguistics: ACL 2025, pages 11615–11639, Vienna, Austria. A… find
  22. Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, Y. K. Li, Y. Wu, and Daya Guo. 2024. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. Preprint, arXiv:2402.03300.
  23. Guangming Sheng, Chi Zhang, Zilingfeng Ye, Xibin Wu, Wang Zhang, Ru Zhang, Yanghua Peng, Haibin Lin, and Chuan Wu. 2025a. Hybridflow: A flexible and efficient rlhf framework. In Proceedings of the Twentieth European Conference on Computer Systems, EuroSys ’25, page 1279–1297, New York, NY, USA. Asso…
  24. Jiayi Sheng, Luna Lyu, Jikai Jin, Tony Xia, Alex Gu, James Zou, and Pan Lu. 2025b. Solving inequality proofs with large language models. In The Thirty-ninth Annual Conference on Neural Information Processing Systems Datasets and Benchmarks Track. find
  25. Yicheng Tao, Haotian Liu, Shanwen Wang, and Hongteng Xu. 2025. Learning an effective premise retrieval model for efficient mathematical formalization. In 2nd AI for Math Workshop @ ICML 2025. find
  26. Peng-Yuan Wang, Tian-Shuo Liu, Chenyang Wang, Yi-Di Wang, Shu Yan, Cheng-Xing Jia, Xu-Hui Liu, Xin-Wei Chen, Jia-Cheng Xu, Ziniu Li, and 1 others. 2025a. A survey on large language models for mathematical reasoning. arXiv preprint arXiv:2506.08446. find
  27. Mingfeng Xue, Runji Lin, Tianyu Liu, Xingzhang Ren, and Zhenru Zhang. 2024. Qwen2.5-math technical report: Toward mathematical expert model via self-improvement. Preprint, arXiv:2409.12122.
  28. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. 2023. Leandojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems, 36:21573–21612.
  29. Ziyin Zhang, Jiahao Xu, Zhiwei He, Tian Liang, Qiuzhi Liu, Yansi Li, Linfeng Song, Zhenwen Liang, Zhuosheng Zhang, Rui Wang, Zhaopeng Tu, Haitao Mi, and Dong Yu. 2025. Deeptheorem: Advancing llm reasoning for theorem proving through natural language and reinforcement learning. Preprint, arXiv:2505.2… — [arXiv:2505.23754](https://arxiv.org/abs/2505.23754) find
  30. A Pinzheng Wang, Juntao Li, Zecheng Tang, Haijia Gui, and 1 others. 2025b. Improving rationality in the reasoning process of language models through self-playing game. In Forty-second International Conference on Machine Learning. find
  31. Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, and Kyunghyun Cho. 2021. Naturalproofs: Mathematical theorem proving in natural language. In Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 1).
  32. Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, and Yejin Choi. 2022. Naturalprover: Grounded mathematical proof generation with language models. In Advances in Neural Information Processing Systems, volume 35, pages 4913–4927. Curran Associates, Inc.
  33. Wei Xiong, Hanning Zhang, Chenlu Ye, Lichang Chen, Nan Jiang, and Tong Zhang. 2025. Self-rewarding correction for mathematical reasoning. arXiv preprint arXiv:2502.19613. — [arXiv:2502.19613](https://arxiv.org/abs/2502.19613) find
  34. Yuchen Yan, Jin Jiang, Yang Liu, Yixin Cao, Xin Xu, Mengdi Zhang, Xunliang Cai, and Jian Shao. 2025. Sˆ 3cmath: Spontaneous step-level self-correction makes large language models better mathematical reasoners. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 39, pages 25588–… find
  35. An Yang, Beichen Zhang, Binyuan Hui, Bofei Gao, Bowen Yu, Chengpeng Li, Dayiheng Liu, Jianhong Tu, Jingren Zhou, Junyang Lin, Keming Lu, Prompts Two-Section Prompt Lemma: {lemma} Statement: {statement} Please analyze step by step whether the lemma is useful for proving or disproving the given statem… find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/xu-2026-reliable-use-lemmas-eligibility-reasoning/