Tutorials
GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research
arXiv:2609.36663v1 Announce Type: new Abstract: We present GenLimitLib, a source-aligned Lean 4 library for language generation in the limit. Introduced by Kleinberg and Mullainathan at NeurIPS 2024,
arXiv:2609.36663v1 Announce Type: new Abstract: 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.
Related
- Continuous Diffusion Models Can Obey Formal Syntax
- Steered Generation via Gradient-Based Optimization on Sparse Query Features
- Destruction is a General Strategy to Learn Generation; Diffusion's Strength is to Take it Seriously; Exploration is the Future
Source: arXiv cs.LG | 2026-09-30