| Challenge: | 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. |
| Approach: | They propose a regularization method that aligns LLMs’ attention mechanisms with mathematical reasoning structures and establishes a five-level hierarchy from foundational elements to high-level concepts. |
| Outcome: | The proposed 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. |
Similar Papers
Self-Attention Networks Can Process Bounded Hierarchical Languages (2021.acl-long)
Copied to clipboard
| Challenge: | Existing models that can process formal languages with hierarchical structure are limited in their performance. |
| Approach: | They propose to use a subset of Dyck-k with depth bounded by D to train self-attention networks. |
| Outcome: | The proposed model can process Dyck-(k, D) with depth bounded by D, which better captures the hierarchical structure of natural language. |
ProofInfer: Generating Proof via Iterative Hierarchical Inference (2022.emnlp-main)
Copied to clipboard
| Challenge: | Existing proof generation models focus on generating several proof paths instead of a whole tree. |
| Approach: | They propose a method that generates the proof tree via iterative hierarchical inference . they propose coding the proof as plain text without losing structure information . |
| Outcome: | The proposed proof generation model significantly improves performance on widely-used datasets. |
Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations (2025.acl-long)
Copied to clipboard
| Challenge: | Recent work has shown that the interaction of large language models (LLMs) with theorem provers (TPs) can help verify and improve the validity of NLI explanations. |
| Approach: | They propose to use logical expressions to guide LLMs in generating structured proof sketches and to use them to improve their accuracy. |
| Outcome: | The proposed strategies improve autoformalisation, syntactic errors and explanation refinement over the state-of-the-art model. |
Visual Attention Reasoning via Hierarchical Search and Self-Verification (2026.acl-long)
Copied to clipboard
| Challenge: | Multimodal Large Language Models (MLLMs) often hallucinate due to fragile, linear reasoning and weak visual grounding. |
| Approach: | They propose a framework that reformulates reasoning as a hierarchical search with self-verification and replaces linear Chain-of-Thought with a tree-search policy capable of backtracking to correct logical errors. |
| Outcome: | The proposed framework outperforms state-of-the-art methods on hallucination and safety benchmarks. |
Exploring the Role of Reasoning Structures for Constructing Proofs in Multi-Step Natural Language Reasoning with Large Language Models (2024.emnlp-main)
Copied to clipboard
| Challenge: | Large language models (LLMs) are essential for performing complex multi-step reasoning tasks, such as multi-hop reasoning tasks. |
| Approach: | They propose to use large language models to derive structured intermediate proof steps to improve their performance by using examples. |
| Outcome: | The proposed models can derive correct proof steps with in-context learning. |
Sentence-Level Evidence Embedding for Claim Verification with Hierarchical Attention Networks (P19-1)
Copied to clipboard
| Challenge: | Claim verification is cumbersome and inefficient for human fact-checkers to find consistent pieces of evidence. |
| Approach: | They propose an end-to-end hierarchical attention network that learns to represent coherent evidence and their semantic relatedness with the claim. |
| Outcome: | The proposed model outperforms state-of-the-art models on three datasets . it is based on a coherence-based attention layer and entailment-based one . |
ART: Adaptive Reasoning Trees for Explainable Claim Verification (2026.findings-eacl)
Copied to clipboard
Sahil Wadhwa, Himanshu Kumar, Guanqun Yang, Abbaas Alif Mohamed Nishar, Pranab Mohanty, Swapnil Shinde, Yue Wu
| Challenge: | Large Language Models (LLMs) are powerful candidates for complex decision-making, leveraging vast encoded knowledge and remarkable zero-shot abilities. |
| Approach: | They propose a hierarchical method for claim verification that uses a root claim and a pairwise tournament of its children to determine an argument's strength. |
| Outcome: | The proposed method outperforms baseline methods on multiple datasets and shows that it is more reliable and clearer than existing methods. |
Theoretical Analysis of Hierarchical Language Recognition and Generation by Transformers without Positional Encoding (2025.acl-long)
Copied to clipboard
| Challenge: | Existing studies show that Transformers can recognize hierarchical structures without a specific positional encoding. |
| Approach: | They show that Transformers can generate hierarchical languages without a positional encoding . they also suggest that explicit positional encoders might have a detrimental effect on generalization . |
| Outcome: | The proposed model can generate hierarchical languages with respect to model size without encoding . |
Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving (2025.emnlp-main)
Copied to clipboard
Chuxue Cao, Mengze Li, Juntao Dai, Jinluan Yang, Zijian Zhao, Shengyu Zhang, Weijie Shi, Chengzhong Liu, Sirui Han, Yike Guo
| Challenge: | Large language models (LLMs) have shown promising first-order logic (FOL) reasoning capabilities with applications in various areas, but their effectiveness in complex mathematical reasoning involving multi-step FOL deductions remains under-explored. |
| Approach: | They propose a self-adaptive solution that enhances the Diversity and REAsonability of LLMs’ generation strategies by introducing an Axiom-Driven Strategy Diversification mechanism and a Sub-Proposition Error Feedback to help LLM reflect on and correct their proofs. |
| Outcome: | The proposed model improves diversity and REAsonability of LLMs’ generation strategies by introducing an Axiom-Driven Strategy Diversification mechanism and a Sub-Proposition Error Feedback to help LLM reflect on and correct proofs. |
Towards Hierarchical Multi-Step Reward Models for Enhanced Reasoning in Large Language Models (2026.findings-acl)
Copied to clipboard
Teng Wang, Jiang Zhangyi, Zhenqi He, Hailei Gong, Shenyang Tong, Wenhan Yang, Zeyu Li, Yanan Zheng, Zifan He, Zewen Ye, Shengjie Ma, Jianping Zhang
| Challenge: | Existing Process Reward Models (PRMs) are vulnerable to reward hacking and require expensive, large-scale annotation of reasoning steps. |
| Approach: | They propose a reward model approach which evaluates both individual and consecutive reasoning steps from fine-grained and coarse-grounded level. |
| Outcome: | Empirical results show that the proposed model performs better than existing PRMs and is more robust than existing models. |