Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Reliable Use of Lemmas via Eligibility Reasoning and Section$-$Aware Reinforcement Learning

Zhikun Xu, Xiaodong Yu, Ben Zhou, Jiang Liu, Jialian Wu, Ze Wang, Ximeng Sun, Hao Chen, Zicheng Liu

TL;DR

The paper addresses pervasive lemma misapplication by recasting lemma usage as a structured prediction problem that requires explicit precondition and conclusion checks. It introduces RULES, a two-section output framework with section-aware reinforcement learning, to align credit with the responsible step and improve robustness to applicability-breaking perturbations. Across multiple LLMs and diverse datasets, RULES yields consistent in-domain gains and substantial robustness improvements, with ablations confirming the necessity of both the two-section scheme and section-aware credit assignment. The approach enhances safe, reliable mathematical reasoning and offers a scalable path toward integrating eligibility reasoning with end-to-end theorem-proving tasks.

Abstract

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.

Reliable Use of Lemmas via Eligibility Reasoning and Section$-$Aware Reinforcement Learning

TL;DR

The paper addresses pervasive lemma misapplication by recasting lemma usage as a structured prediction problem that requires explicit precondition and conclusion checks. It introduces RULES, a two-section output framework with section-aware reinforcement learning, to align credit with the responsible step and improve robustness to applicability-breaking perturbations. Across multiple LLMs and diverse datasets, RULES yields consistent in-domain gains and substantial robustness improvements, with ablations confirming the necessity of both the two-section scheme and section-aware credit assignment. The approach enhances safe, reliable mathematical reasoning and offers a scalable path toward integrating eligibility reasoning with end-to-end theorem-proving tasks.

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.
Paper Structure (37 sections, 1 figure, 2 tables)

This paper contains 37 sections, 1 figure, 2 tables.

Table of Contents

  1. Introduction
  2. Related Works
  3. Methodology: RULES
  4. Lemma-judging Task
  5. Section-Aware Reinforcement Learning
  6. Experimental Settings
  7. Models
  8. Training Settings
  9. Perturbation Design.
  10. Reward Design.
  11. Evaluation Settings
  12. In-domain Evaluation
  13. Perturbation Test
  14. End-to-end Benchmarks
  15. Analysis
  16. ...and 22 more sections

Figures (1)

  • Figure 1: Overview of RULES Training Framework. As mentioned in Section 3.2, if the fine-grained label (precondition/conclusion check) is provided, we could know which section of tokens are to blame with negative rewarding.