基于资格推理和章节感知强化学习的可靠引理使用
计算与语言
2026-02-03 v1
摘要
最近的大型语言模型（LLMs）在数学基准测试中表现强劲，但常常错误地应用引理，将结论导入而不验证假设。我们将引理判断 formalized 为一种结构化预测任务：给定一条语句和一个候选引理，模型必须输出 precondition check 和 conclusion-utility check，据此推导出 usefulness decision。我们提出了RULES，通过 two-section output 编码该规范，并使用 reinforcement learning 加 section-aware loss masking 进行训练，以对负责错误的章节施加惩罚。训练和评估依赖多样化的自然语言和形式证明语料库；鲁棒性通过 held-out perturbation suite 进行评估；端到端评估涵盖 competition-style、perturbation-aligned 和 theorem-based problems，适用于各种LLMs。结果显示，相较于 vanilla model 和 single-label RL baseline，RULES在所有领域内均实现一致的收益，对 applicability-breaking perturbations 的改进更大，在端到端任务上实现持平或适度的提升；ablation 实验表明，two-section outputs 和 section-aware reinforcement 对于鲁棒性至关重要。
引用
@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}
}