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

arXiv: https://arxiv.org/abs/2602.00998 · HTML: https://mlsanity.com/paper/2602.00998/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Reinforcement learning for reasoning, one of 17 directions in LLM reasoning.
- Builds on 18 of its 33 references that are in the map.
- First posted on arXiv 1 Feb 2026.

## Placed in

- LLM reasoning / [Reinforcement learning for reasoning](https://mlsanity.com/lr/reinforcement-learning-for-reasoning/)

## Builds on (most cited first, 18 of 18)

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [The Llama 3 Herd of Models](https://mlsanity.com/paper/2407.21783/) (2024)
- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Efficient Memory Management for Large Language Model Serving with PagedAttention](https://mlsanity.com/paper/2309.06180/) (2023)
- [Qwen2.5-Math Technical Report: Toward Mathematical Expert Model via Self-Improvement](https://mlsanity.com/paper/2409.12122/) (2024)
- [2 OLMo 2 Furious](https://mlsanity.com/paper/2501.00656/) (2024)
- [MathArena: Evaluating LLMs on Uncontaminated Math Competitions](https://mlsanity.com/paper/2505.23281/) (2025)
- [DeepMath-103K: A Large-Scale, Challenging, Decontaminated, and Verifiable Mathematical Dataset for Advancing Reasoning](https://mlsanity.com/paper/2504.11456/) (2025)
- [Premise Order Matters in Reasoning with Large Language Models](https://mlsanity.com/paper/2402.08939/) (2024)
- [Self-rewarding correction for mathematical reasoning](https://mlsanity.com/paper/2502.19613/) (2025)
- [A Survey on Large Language Models for Mathematical Reasoning](https://mlsanity.com/paper/2506.08446/) (2025)
- [The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs](https://mlsanity.com/paper/2506.21621/) (2025)
- [DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning](https://mlsanity.com/paper/2505.23754/) (2025)
- [Solving Inequality Proofs with Large Language Models](https://mlsanity.com/paper/2506.07927/) (2025)
- [Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Models](https://mlsanity.com/paper/2506.17114/) (2025)
- [Large Language Models for Mathematicians](https://mlsanity.com/paper/2312.04556/) (2023)
- [Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving](https://mlsanity.com/paper/2507.06804/) (2025)
- [Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving](https://mlsanity.com/paper/2503.11657/) (2025)

## Abstract (arXiv)

Recent large language models (LLMs) perform strongly on mathematical benchmarks yet often misapply lemmas, importing conclusions without validating assumptions. We formalize lemma-judging as a structured prediction task: given a statement and a candidate lemma, the model must output a precondition check and a conclusion-utility check, from which a usefulness decision is derived. We present RULES, which encodes this specification via a two-section output and trains with reinforcement learning plus section-aware loss masking to assign penalty to the section responsible for errors. Training and evaluation draw on diverse natural language and formal proof corpora; robustness is assessed with a held-out perturbation suite; and end-to-end evaluation spans competition-style, perturbation-aligned, and theorem-based problems across various LLMs. Results show consistent in-domain gains over both a vanilla model and a single-label RL baseline, larger improvements on applicability-breaking perturbations, and parity or modest gains on end-to-end tasks; ablations indicate that the two-section outputs and section-aware reinforcement are both necessary for robustness.