Abstract
Recent large language models (LLMs) perform strongly on mathematical benchmarks yet often misapply lemmas, importing conclusions without validating assumptions. We formalize lemmajudging as a structured prediction task: given a statement and a candidate lemma, the model must output a precondition check and a conclusionutility check, from which a usefulness decision is derived. We present RULES, which encodes this specification via a twosection output and trains with reinforcement learning plus sectionaware 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 heldout perturbation suite; and endtoend evaluation spans competitionstyle, perturbationaligned, and theorembased problems across various LLMs. Results show consistent indomain gains over both a vanilla model and a singlelabel RL baseline, larger improvements on applicabilitybreaking perturbations, and parity or modest gains on endtoend tasks; ablations indicate that the twosection outputs and sectionaware reinforcement are both necessary for robustness.