Saved in:
| Main Authors: | , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2602.00998 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912866747023360 |
|---|---|
| author | Xu, Zhikun Yu, Xiaodong Zhou, Ben Liu, Jiang Wu, Jialian Wang, Ze Sun, Ximeng Chen, Hao Liu, Zicheng |
| author_facet | Xu, Zhikun Yu, Xiaodong Zhou, Ben Liu, Jiang Wu, Jialian Wang, Ze Sun, Ximeng Chen, Hao Liu, Zicheng |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_00998 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Reliable Use of Lemmas via Eligibility Reasoning and Section$-$Aware Reinforcement Learning Xu, Zhikun Yu, Xiaodong Zhou, Ben Liu, Jiang Wu, Jialian Wang, Ze Sun, Ximeng Chen, Hao Liu, Zicheng Computation and Language 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. |
| title | Reliable Use of Lemmas via Eligibility Reasoning and Section$-$Aware Reinforcement Learning |
| topic | Computation and Language |
| url | https://arxiv.org/abs/2602.00998 |