用分层注意力提升大模型证明数学定理的能力
Hierarchical Attention Generates Better Proofs
- 设计五层结构化注意力，匹配数学证明的层级逻辑
- 在miniF2F和ProofNet上成功率分别提升2.05%和1.69%
- 适合关注形式化证明与模型推理结构的研究者
大型语言模型（LLMs）在形式化定理证明中展现出潜力，但其逐标记处理方式难以捕捉数学证明固有的层级结构。我们提出 extbf{分层注意力}（Hierarchical Attention），一种正则化方法，使LLM的注意力机制与数学推理结构对齐。该方法构建了从基础元素到高层概念的五级层次结构，确保证明生成中的信息流动有序。实验表明，该方法在miniF2F上将证明成功率提升2.05%，在ProofNet上提升1.69%，同时分别降低证明复杂度23.81%和16.50%。代码已开源：https://github.com/Car-pe/HAGBP。
原文摘要 · Abstract (English)
Large language models (LLMs) have shown promise in formal theorem proving, but their token-level processing often fails to capture the inherent hierarchical nature of mathematical proofs. We introduce \textbf{Hierarchical Attention}, a regularization method that aligns LLMs' attention mechanisms with mathematical reasoning structures. Our approach establishes a five-level hierarchy from foundational elements to high-level concepts, ensuring structured information flow in proof generation. Experiments demonstrate that our method improves proof success rates by 2.05\% on miniF2F and 1.69\% on ProofNet while reducing proof complexity by 23.81\% and 16.50\% respectively. The code is available at https://github.com/Car-pe/HAGBP.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。