# Hierarchical Attention Generates Better Proofs

Preprint · Jianlong Chen, Chao Li, Yang Yuan, Andrew C Yao

- Archive id: arxiv:2504.19188
- Published: 2025-04-27
- arXiv: https://arxiv.org/abs/2504.19188
- Source URL: https://arxiv.org/abs/2504.19188
- PDF: https://arxiv.org/pdf/2504.19188
- Provenance: arxiv

## Abstract

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.

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.
