GenLimitLib：极限语言生成与AI辅助数学研究的正式库
GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research
查看机构详情
- Yale University（耶鲁大学）
- Rutgers University（罗格斯大学）
机构由 AI 辅助整理，请以论文原文为准。
浏览论文内容
中文总结 AI 辅助
GenLimitLib是一个Lean 4形式化库，用于极限语言生成，涵盖30篇论文，提取共享组件并记录关系，支持人类与AI辅助数学研究。
中文摘要 AI 辅助
我们提出了GenLimitLib，一个面向极限语言生成的源对齐的Lean 4库。极限语言生成由Kleinberg和Mullainathan在NeurIPS 2024上提出，研究了一个由大语言模型（LLM）驱动的理论问题：如何从观察到的示例中生成有效的新字符串。这个年轻且快速发展的领域为研究大规模形式化提供了天然的试验场。GenLimitLib包含30篇论文的形式化开发。它提取共享定义和可复用的证明组件，同时保留每篇论文特有的假设和陈述，并记录论文之间的关系。通过这种方式，GenLimitLib提供了对文献的具体且结构化的视图。我们通过数学案例研究和LLM实验展示了我们的库如何支持人类数学研究和AI辅助研究。我们的库：此https URL。
英文摘要
We present GenLimitLib, a source-aligned Lean 4 library for language generation in the limit. Introduced by Kleinberg and Mullainathan at NeurIPS 2024, language generation in the limit studies a theoretical question motivated by LLMs: how to generate valid new strings from observed examples. This young and rapidly evolving field offers a natural testbed for studying large-scale formalization. GenLimitLib contains formal developments for 30 papers. It extracts shared definitions and reusable proof components while preserving paper-specific assumptions and statements, and records relationships across papers. In this way, GenLimitLib provides a concrete and structured view of the literature. We show through mathematical case studies and LLM experiments how our library can support both human mathematical research and AI-assisted research. Our Library: https://github.com/pengzhang91/generation-in-the-limit-lib.
