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.
@article{arxiv.2602.00998,
title = {Reliable Use of Lemmas via Eligibility Reasoning and Section$-$Aware Reinforcement Learning},
author = {Zhikun Xu and Xiaodong Yu and Ben Zhou and Jiang Liu and Jialian Wu and Ze Wang and Ximeng Sun and Hao Chen and Zicheng Liu},
journal= {arXiv preprint arXiv:2602.00998},
year = {2026}
}