Reliable Use of Lemmas via Eligibility Reasoning and Section-Aware Reinforcement Learning
On the map: LLM reasoning → Reinforcement learning for reasoning
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.
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.
Builds on
18 of 33 references.
Closest ancestors · 1
Same direction, newest first
Other references · 17
- 2023GPT-4 Technical Reportcited by 18,396
- 2024The Llama 3 Herd of Modelscited by 14,715
- 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Modelscited by 9,379
- 2023Efficient Memory Management for Large Language Model Serving with PagedAttentioncited by 5,944
- 2024Qwen2.5-Math Technical Report: Toward Mathematical Expert Model via Self-Improvementcited by 1,090
- 20242 OLMo 2 Furiouscited by 340
- 2025MathArena: Evaluating LLMs on Uncontaminated Math Competitionscited by 297
- 2024Premise Order Matters in Reasoning with Large Language Modelscited by 72
- 2025Self-rewarding correction for mathematical reasoningcited by 70
- 2025A Survey on Large Language Models for Mathematical Reasoningcited by 52
- 2025The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofscited by 30
- 2025DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learningcited by 24
5 more
- 2025Solving Inequality Proofs with Large Language Modelscited by 21
- 2025Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Modelscited by 20
- 2023Large Language Models for Mathematicianscited by 7
- 2025Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Provingcited by 7
- 2025Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Provingcited by 2
Built on by
Not cited yet.
Similar, not cited
Close in wording, no citation either way
- 2026Proof-Carrying Cognition: Closing the Verification Gap with Reality-Settled Reward
- 2025Not All Tokens Matter: Towards Efficient LLM Reasoning via Token Significance in Reinforcement Learning
- 2025A Sober Look at Progress in Language Model Reasoning: Pitfalls and Paths to Reproducibility
- 2025VerifyBench: A Systematic Benchmark for Evaluating Reasoning Verifiers Across Domains
- 2026Rethinking RL for LLM Reasoning: It's Sparse Policy Selection, Not Capability Learning
- 2026Checking the Checkers: A Synthesis of Verifier Noise and Robustness in RLVR
- 2026Training Reasoning Models on Saturated Problems via Failure-Prefix Conditioning
- 2026Step Potential Advantage Estimation: Harnessing Intermediate Confidence and Correctness for Efficient Mathematical Reasoning