Reliable Use of Lemmas via Eligibility Reasoning and Section-Aware Reinforcement Learning
Zhikun Xu Arizona State University, Xiaodong Yu Snowflake, Ben Zhou Arizona State University, Jiang Liu Advanced Micro Devices, Jialian Wu Advanced Micro Devices, Ze Wang Luma AI, Ximeng Sun Advanced Micro Devices, Hao Chen Google DeepMind 等 9 位作者
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.
尚无 AI 解读，展示原文摘要
Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 2: Short Papers) · 2026 · 正式发表