GenLimitLib：极限语言生成和人工智能辅助数学研究的形式库

摘要

我们推出 GenLimitLib，一个源对齐的 Lean 4 库，用于限制语言生成。 Kleinberg 和 Mullainathan 在 NeurIPS 2024 上提出，极限语言生成研究由大语言模型引发的理论问题：如何从观察到的示例生成有效的新字符串。这个年轻且快速发展的领域为研究大规模形式化提供了一个天然的试验平台。 GenLimitLib 包含 30 篇论文的正式进展。它提取共享的定义和可重用的证明组件，同时保留特定于论文的假设和陈述，并记录论文之间的关系。通过这种方式，GenLimitLib 提供了具体且结构化的文献视图。我们通过数学案例研究和大语言模型实验展示我们的图书馆如何支持人类数学研究和人工智能辅助研究。我们的图书馆：https://github.com/pengzhang91/generation-in-the-limit-lib.