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. |
Similar Papers
Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions (2025.emnlp-main)
Copied to clipboard
| Challenge: | Large Language Models (LLMs) have demonstrated remarkable potential in assisting with mathematical reasoning on different downstream tasks. |
| Approach: | They propose two new tools for autoformalizing real-world mathematical definitions from Wikipedia and arXiv papers. |
| Outcome: | The proposed methods improve definitions by up to 16% and undefined errors by 43%. |
MASA: LLM-Driven Multi-Agent Systems for Autoformalization (2025.emnlp-demos)
Copied to clipboard
| Challenge: | This paper presents a framework for building multi-agent systems for autoformalization driven by Large Language Models. |
| Approach: | They propose a framework for building multi-agent systems for autoformalization driven by Large Language Models. |
| Outcome: | The proposed framework leverages collaborative agents to convert natural language statements into formal representations. |
Improving Autoformalization Using Direct Dependency Retrieval (2026.acl-long)
Copied to clipboard
| Challenge: | Existing methods for hallucinate formal dependencies lack scalability and precision to leverage ever-growing public datasets. |
| Approach: | They propose a retrieval-augmented framework based on Direct Dependency Retrieval to generate formal dependencies from natural-language mathematical descriptions and verify their existence via an efficient Suffix Array Check (SAC). |
| Outcome: | The proposed framework outperforms state-of-the-art methods in retrieval precision and recall and can be used to validate formal representations in a public dataset. |
AutoAlign: Get Your LLM Aligned with Minimal Annotations (2025.acl-demo)
Copied to clipboard
Xinyu Lu, Dong Xu, Chunkang Zhang, Xinyan Guan, Junxiang Wang, Qingyu Zhang, Pengbo Wang, Yingzhi Mao, Hao Xiang, Xueru Wen, Zichao Li, Yaojie Lu, Hongyu Lin, Le Sun, Xianpei Han
| Challenge: | Automated Alignment (ALM) is a set of algorithms designed to align Large Language Models (LLMs) with human intentions and values while minimizing manual intervention. |
| Approach: | They propose an open-source toolkit that integrates mainstream automated algorithms through a consistent interface and an accessible workflow supporting one-click execution for prompt synthesis and automatic alignment signal construction. |
| Outcome: | The proposed framework enables easy reproduction of existing results through extensive benchmarks and facilitates the development of novel approaches via modular components. |
TEaR: Improving LLM-based Machine Translation with Systematic Self-Refinement (2025.findings-naacl)
Copied to clipboard
Zhaopeng Feng, Yan Zhang, Hao Li, Bei Wu, Jiayu Liao, Wenqiang Liu, Jun Lang, Yang Feng, Jian Wu, Zuozhu Liu
| Challenge: | Large Language Models (LLMs) have achieved impressive results in Machine Translation (MT). human evaluations reveal that LLM-generated translations still contain various errors. |
| Approach: | They propose a LLM-based self-refinement framework that feeds error information back into LLMs to facilitate self-finement, leading to enhanced translation quality. |
| Outcome: | The proposed framework outperforms internal refinement and feedback methods while ensuring a robust translation quality baseline. |
Enabling Large Language Models to Generate Text with Citations (2023.emnlp-main)
Copied to clipboard
| Challenge: | Existing work relies on commercial search engines and human evaluation, making it difficult to reproduce and compare different modeling approaches. |
| Approach: | They propose a new generation paradigm that requires large language models to provide citations to one or a few text passages for any statement they generate. |
| Outcome: | The proposed model improves factual correctness and verifiability of large language models by providing citations to a set of questions and retrieval corpora and generating answers with citation. |
Contextual Refinement of Translations: Large Language Models for Sentence and Document-Level Post-Editing (2024.naacl-long)
Copied to clipboard
| Challenge: | Large language models have demonstrated considerable success in various natural language processing tasks, but their performance in NMT tasks is still underexplored. |
| Approach: | They propose to use LLMs as automatic post-editors rather than direct translators to improve BLEU and COMET performance. |
| Outcome: | The proposed approach improves BLEU but COMET performance compared to in-context learning. |
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. |
What Does LLM Refinement Actually Improve? A Systematic Study on Document-Level Literary Translation (2026.acl-long)
Copied to clipboard
Shaomu Tan, Dawei Zhu, Ke Tran, Michael Denkowski, Sony Trenous, Leonardo F. R. Ribeiro, Bill Byrne, Felix Hieber
| Challenge: | Large language models (LLMs) have made document-level machine translation increasingly practical, enabled by long-context modeling and strong generation quality. |
| Approach: | They propose to use document-level MT followed by segment-level refinement to find the strongest and most stable improvements across six LLMs and seven language pairs. |
| Outcome: | The proposed method outperforms error-specific prompting and evaluate-then-refine schemes in document-level translation. |
LLMs for Mathematical Modeling: Towards Bridging the Gap between Natural and Mathematical Languages (2025.findings-naacl)
Copied to clipboard
| Challenge: | Large Language Models (LLMs) have demonstrated strong performance across various natural language processing tasks, but their proficiency in mathematical reasoning remains a key challenge. |
| Approach: | They propose a process-oriented framework to evaluate LLMs' ability to construct mathematical models, using solvers to compare outputs with ground truth. |
| Outcome: | The proposed framework evaluates LLMs' ability to construct mathematical models, using solvers to compare outputs with ground truth. |