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.
Zheyuan Liu University of Notre Dame, Yixin Wan University of California, Los Angeles, Kai-Wei Chang University of California, Los Angeles, Meng Jiang University of Notre Dame, Jieyu Zhao University of Southern California, Nouha Dziri Cohere Labs, Yuning Mao Meta Superintelligence Labs, Jia-Chen Gu University of California, Los Angeles 等 9 位作者
Controlling the knowledge and behavior of generative AI systems, including large language models (LLMs), multimodal LLMs (MLLMs), and text-to-image (T2I) models, has become critical as they are increasingly used in safety-sensitive and socially impactful applications. These models often encode unintended, biased, or private content, leading to harmful or unethical outputs. Post-training knowledge control has thus emerged as a practical framework for selectively modifying or removing model behaviors without full retraining, offering scalable and interpretable interventions for improving safety, privacy, and fairness. This tutorial introduces the foundations of post-training knowledge control and showcases recent frontier methods, bridging research insights with real-world practices from both academia and industry. We cover: (i) key motivations and failure modes, such as harmful generation and stereotype reinforcement; (ii) core methods such as machine unlearning, knowledge editing, and inference-time interventions for targeted behavior adjustment; and (iii) evaluation protocols for balancing forgetting, retention, and fairness. Case studies will span text and vision–language generation, including privacy preservation, bias mitigation, and factual correction.
尚无 AI 解读，展示原文摘要
cs.CL · cs.CV
Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 5: Tutorial Abstracts) · 2026 · 正式发表