ACL 2025long0 citations
Hierarchical Attention Generates Better Proofs
Jianlong Chen, Chao Li, Yang Yuan, Andrew C Yao
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 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 and models will be available.
BibTeX
@inproceedings{chen-etal-2025-hierarchical,
title = "Hierarchical Attention Generates Better Proofs",
author = "Chen, Jianlong and
Li, Chao and
Yuan, Yang and
Yao, Andrew C",
editor = "Che, Wanxiang and
Nabende, Joyce and
Shutova, Ekaterina and
Pilehvar, Mohammad Taher",
booktitle = "Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)",
month = jul,
year = "2025",
address = "Vienna, Austria",
publisher = "Association for Computational Linguistics",
url = "https://aclanthology.org/2025.acl-long.856/",
doi = "10.18653/v1/2025.acl-long.856",
pages = "17506--17520",
ISBN = "979-8-89176-251-0"
}