mlsanityData to 14 Oct 2026

Hierarchical Attention Generates Better Proofs

arXiv 2504.19188 ↗First posted 27 Apr 2025cs.LG cs.AI cs.CLcited by 1

Not on the map. Why?

Abstract (arXiv)

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 is available at https://github.com/Car-pe/HAGBP.

Key facts. Cited by 1 paper in the map (data through 14 Oct 2026). Builds on 39 of its 74 references that are in the map. First posted on arXiv 27 Apr 2025.

Builds on

39 of 74 references.

References · 39

  1. 2017Attention Is All You Needcited by 60,361
  2. 2023Pythia: A Suite for Analyzing Large Language Models Across Training and Scalingcited by 1,786
  3. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
  4. 2020Generative Language Modeling for Automated Theorem Provingcited by 388
  5. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
  6. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 234
  7. 2022HyperTree Proof Search for Neural Theorem Provingcited by 197
  8. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 192
  9. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 180
  10. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 132
  11. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 122
  12. 2024InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoningcited by 119
27 more
  1. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 109
  2. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 109
  3. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 98
  4. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 84
  5. 2016DeepMath - Deep Sequence Models for Premise Selectioncited by 81
  6. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 79
  7. 2019Graph Representations for Higher-Order Logic and Theorem Provingcited by 55
  8. 2023FIMO: A Challenge Formal Dataset for Automated Theorem Provingcited by 55
  9. 2018First Experiments with Neural Translation of Informal to Formal Mathematicscited by 53
  10. 2023Magnushammer: A Transformer-Based Approach to Premise Selectioncited by 50
  11. 2018GamePad: A Learning Environment for Theorem Provingcited by 48
  12. 2017Deep Network Guided Proof Searchcited by 47
  13. 2024Process-Driven Autoformalization in Lean 4cited by 45
  14. 2017Premise Selection for Theorem Proving by Deep Graph Embeddingcited by 44
  15. 2019Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizarcited by 40
  16. 2019Generating Correctness Proofs with Neural Networkscited by 37
  17. 2023Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Provingcited by 37
  18. 2023LLMSTEP: LLM proofstep suggestions in Leancited by 32
  19. 2024Proving Theorems Recursivelycited by 26
  20. 2022Passport: Improving Automated Formal Verification Using Identifierscited by 19
  21. 2021Learning to Guide a Saturation-Based Theorem Provercited by 15
  22. 2020Natural Language Premise Selection: Finding Supporting Statements for Mathematical Textcited by 13
  23. 2020Learning to Prove from Synthetic Theoremscited by 13
  24. 2023MLFMF: Data Sets for Machine Learning for Mathematical Formalizationcited by 10
  25. 2023Graph Sequence Learning for Premise Selectioncited by 5
  26. 2023An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representationscited by 4
  27. 2018Premise selection with neural networks and distributed representation of featurescited by 2

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2026: 1.

1 paper.

  1. 2026Grading the Graders: Verification Autonomy Levels (L0-L5) for LLM Reasoningcited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2024Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically
  2. 2025ProofCompass: Enhancing Specialized Provers with LLM Guidance
  3. 2025Steering LLMs for Formal Theorem Proving
  4. 2026Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness
  5. 2026AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification
  6. 2026MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis
  7. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoning
  8. 2024MathGAP: Out-of-Distribution Evaluation on Problems with Arbitrarily Complex Proofs