Large language models have made rapid progress in generating machine-checked proofs for well-defined mathematical problems. Extending this progress to research mathematics requires more than solving isolated theorems. Research involves choosing questions, developing definitions and conjectures, connecting results, and combining formal proofs with expert judgment. This survey examines how LLM-driven systems can support these broader activities. We review formal-mathematics tasks, datasets, and autoformalization, and organize proof-generation methods into three overlapping areas: training strategies, inference-time search and adaptation, and agentic workflows. We then examine benchmark results, selected research projects, and platforms for collaborative mathematical work. A central distinction runs throughout the survey: checking a formal proof does not by itself establish that it captures the intended problem or makes a new mathematical contribution. We therefore distinguish theorem benchmarks, repository tasks, formalization projects, and research claims, and discuss the evidence needed to assess each. Finally, we identify five priorities for progress: better data and evaluation, representations of mathematical relationships, conjecture and concept generation, reliable tool integration, and human--AI collaboration. Together, these perspectives connect advances in proof generation to the practical demands of mathematical research.
Haikang Deng UCLA Computer Science Department, University of California, Los Angeles, Po-Nien Kung Google and UCLA Computer Science Department, University of California, Los Angeles, Nanyun Peng Google and University of California, Los Angeles
Large language models (LLMs) are increasingly adept at solving complex problems, such as mathematical reasoning and automatic evaluation. However, performance often degrades when prompts intertwine task instructions with rigid formatting requirements. This entanglement creates competing goals for the model, hindering its reasoning capabilities. To address this, we introduce Deco-G, a decoding framework that explicitly decouples format adherence from problem solving. Deco-G delegates format adherence to a separate Format Estimation Module (FEM), which performs probabilistic lookahead to estimate future format compliance rate and reweighs token probabilities, allowing the LLM to focus solely on task resolution. To make this approach both practical and efficient, we introduce three key innovations: instruction-aware distillation, a flexible trie-building algorithm, and HMM state pruning. Experiments across mathematical reasoning, event argument extraction, and LLM-as-a-judge demonstrate that Deco-G constantly gains over prompting or structured generation baselines, with guaranteed format compliance.
尚无 AI 解读，展示原文摘要
cs.CL
Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers) · 2026 · 正式发表
Nikhil Kandpal, Haikang Deng, Adam Roberts, Eric Wallace, Colin Raffel
The Internet contains a wealth of knowledge -- from the birthdays of historical figures to tutorials on how to code -- all of which may be learned by language models. However, while certain pieces of information are ubiquitous on the web, others appear extremely rarely. In this paper, we study the relationship between the knowledge memorized by large language models and the information in pre-training datasets scraped from the web. In particular, we show that a language model's ability to answer a fact-based question relates to how many documents associated with that question were seen during pre-training. We identify these relevant documents by entity linking pre-training datasets and counting documents that contain the same entities as a given question-answer pair. Our results demonstrate strong correlational and causal relationships between accuracy and relevant document count for numerous question answering datasets (e.g., TriviaQA), pre-training corpora (e.g., ROOTS), and model sizes (e.g., 176B parameters). Moreover, while larger models are better at learning long-tail knowledge, we estimate that today's models must be scaled by many orders of magnitude to reach competitive QA performance on questions with little support in the pre-training data. Finally, we show that retrieval-augmentation can reduce the dependence on relevant pre-training information, presenting a promising approach for capturing the long-tail.