arXiv:2504.19188v1 类别：交叉学科 摘要：大型语言模型（LLMs）在形式定理证明方面显示出潜力，但它们的标记级处理往往未能捕捉到数学证明的固有层次结构。我们引入了**层次注意力**作为一种正则化方法，使LLMs的注意力机制与数学推理结构对齐。我们的方法建立了从基本元素到高级概念的五级层次结构，确保了证明生成中的结构化信息流。实验表明，我们的方法在miniF2F上将证明成功率提高了2.05%，在ProofNet上提高了1.69%，同时分别减少了23.81%和16.50%的证明复杂性。相关代码可从https://github.com/Car-pe/HAGBP获取。