SAIR-Comb : A Structure-Aware Iterative Refinement Framework for Combinatorics Autoformalization (2026.acl-long)
Copied to clipboard
| Challenge: | Large language models (LLMs) have catalyzed advances in mathematical reasoning, propelling the development of automated theorem proving (ATP). |
| Approach: | They propose a Structure-Aware Iterative Refinement framework for Combinatorics powered by Lean 4 and LLMs. |
| Outcome: | The proposed framework achieves strong performance on the specialized CombiBench while remaining highly competitive on general-domain benchmarks. |
Similar Papers
SLR: Automated Synthesis for Scalable Logical Reasoning (2026.acl-long)
Copied to clipboard
Lukas Helff, Ahmad Omar, Felix Friedrich, Antonia Wüst, Hikaru Shindo, Rupert Mitchell, Tim Woydt, Patrick Schramowski, Wolfgang Stammer, Kristian Kersting
| Challenge: | Existing benchmarks intended to evaluate reasoning capabilities emphasize deductive reasoning, where conclusions necessarily follow from given premises. |
| Approach: | They propose an end-to-end framework for systematic evaluation and training of Large Language Models via Scalable Logical Reasoning. |
| Outcome: | The proposed framework doubles Llama-3-8B accuracy on SLR-Bench, achieving parity with Gemini-Flash-Thinking at a fraction of computational cost. |
Reasoning in a Combinatorial and Constrained World: Benchmarking LLMs on Natural-Language Combinatorial Optimization (2026.findings-acl)
Copied to clipboard
| Challenge: | NLCO evaluates large language models for combinatorial optimization (CO) . existing evaluations emphasize relatively simple reasoning competencies . |
| Approach: | They propose a combinatorial optimization benchmark that evaluates large language models on CO reasoning. |
| Outcome: | The proposed model can handle combinatorial optimization without writing code or calling external solvers. |
Reasoning-Based Refinement of Unsupervised Text Clusters with LLMs (2026.findings-acl)
Copied to clipboard
| Challenge: | Unsupervised methods are used to induce latent semantic structure from large text collections, yet their outputs often contain incoherent, redundant, or poorly grounded clusters. |
| Approach: | They propose a framework that leverages large language models as semantic judges to validate and restructure unsupervised clustering algorithms. |
| Outcome: | The proposed framework improves cluster coherence and human-aligned labeling quality over traditional models and representation-based baselines. |
Consistent Autoformalization for Constructing Mathematical Libraries (2024.emnlp-main)
Copied to clipboard
| Challenge: | Autoformalization is the task of automatically translating mathematical content written in natural language to a formal language expression. |
| Approach: | They propose to use three mechanisms to improve autoformalization quality . they propose to combine most-similar retrieval augmented generation, denoising steps and auto-correction with syntax error feedback to improve syntactic, terminological and semantic control. |
| Outcome: | The proposed mechanisms can deliver syntactically, terminologically and semantically more consistent results across different models. |
Probabilistic Soundness Guarantees in LLM Reasoning Chains (2025.emnlp-main)
Copied to clipboard
| Challenge: | Existing methods for detecting propagated errors in reasoning chains are inadequate . author et al. (2017) show that initial errors propagate and undermine reliability of final conclusion . |
| Approach: | They propose a framework that evaluates each reasoning step based solely on previously-verified premises and provides certified statistical guarantees of its soundness. |
| Outcome: | ARES achieves state-of-the-art performance across four benchmarks and demonstrates superior robustness on very long synthetic reasoning chains. |
Unlocking Recursive Thinking of LLMs: Alignment via Refinement (2025.findings-acl)
Copied to clipboard
| Challenge: | Existing methods for recursive reasoning are limited due to lack of expert-curated data. |
| Approach: | They propose a method that unlocks the potential of Large Language Models for recursive reasoning through long-form Chain of Thought. |
| Outcome: | The proposed method outperforms preference optimization methods on the openAI o1-series models by 20% on 3k synthetic samples. |
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. |
LTRAG: Enhancing Autoformalization and Self-refinement for Logical Reasoning with Thought-Guided RAG (2025.findings-acl)
Copied to clipboard
| Challenge: | Large language models (LLMs) have shown promise in natural language reasoning, especially with techniques like chain-of-thought prompting. |
| Approach: | They propose a framework to enhance autoformalization and self-refinement for logical reasoning with Retrieval-Augmented Generation (RAG) by building knowledge bases of thought-guided examples. |
| Outcome: | The proposed framework outperforms Logic-LM and LINC on FOLIO and AR-LSAT, and achieves an accuracy gain of 13% over Logic LM and the proposed methods on GPT-4 and AR LSAT. |
An Empirical Study of Iterative Refinements for Non-autoregressive Translation (2025.acl-long)
Copied to clipboard
| Challenge: | Iterative non-autoregressive (NAR) models have recently demonstrated impressive performance in varied generation tasks, surpassing the autoregressive Transformer. |
| Approach: | They propose a strategy to conduct efficient refinements without performance declines by using two simple metrics to identify potential problems existing in current refinement processes. |
| Outcome: | The proposed model outperforms the autoregressive Transformer by around one BLEU on average. |
Learning to Refine: Self-Refinement of Parallel Reasoning in LLMs (2026.findings-acl)
Copied to clipboard
Qibin Wang, Pu Zhao, Shaohan Huang, Fangkai Yang, Lu Wang, Furu Wei, Qingwei Lin, Saravan Rajmohan, Dongmei Zhang
| Challenge: | Existing approaches to test-time scaling are limited due to the quality of candidate responses. |
| Approach: | They propose a new metric to quantify the relative improvement of self-refinement beyond majority voting. |
| Outcome: | The proposed method achieves state-of-the-art performance across five benchmarks over other methods. |