論文の概要: GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research

• arxiv url: http://arxiv.org/abs/2609.36663v1
• Date: Tue, 29 Sep 2026 04:06:07 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-30 21:28:47.173183
• Title: GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research
• Title（参考訳）: GenLimitLib: 限界とAI支援数学研究における言語生成のための形式ライブラリ
• Abstract要約: GenLimitLibは、ソース整合型の言語生成用のLean 4ライブラリです。 KleinbergとMullainathanによってNeurIPS 2024で導入された。 GenLimitLibには30の論文の正式な開発が含まれている。
• 参考スコア（独自算出の注目度）: 5.156575847416627
• License: http://creativecommons.org/licenses/by/4.0/
• 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.
• Abstract（参考訳）: GenLimitLibは、ソース整合型の言語生成用のLean 4ライブラリです。 Kleinberg と Mullainathan が NeurIPS 2024 で紹介したこの限界における言語生成は、LLM に動機付けられた理論的問題である、観察された例から有効な新しい文字列を生成する方法である。 この若く急速に進化する分野は、大規模な形式化を研究するための自然なテストベッドを提供する。 GenLimitLibには30の論文の正式な開発が含まれている。 共有定義と再利用可能な証明コンポーネントを抽出し、論文固有の仮定とステートメントを保存し、論文間の関係を記録する。 このようにして、GenLimitLibは、文学の具体的で構造化されたビューを提供する。 我々は、数学的ケーススタディとLLM実験を通して、我々のライブラリが人間の数学的研究とAI支援研究の両方をサポートする方法を示す。 私たちのライブラリ: https://github.com/pengzhang91/ generation-in-the-limit-lib。

関連論文リスト

• SciZoom: A Large-scale Benchmark for Hierarchical Scientific Summarization across the LLM Era [2.2090506971647144]
  SciZoomは、2020年から2025年までの4つのトップレベルのML会場から44,946の論文からなるベンチマークである。 我々の言語学的分析は、句パターンの顕著な変化(式表現の最大10倍)と修辞スタイル(23%のヘッジ減少)を明らかにしている。 SciZoomは、生成AI時代の科学的談話の進化をマイニングするための、挑戦的なベンチマークとユニークなリソースとして機能する。
  論文  参考訳（メタデータ） (2026-03-17T05:34:46Z)
• CodeRAG-Bench: Can Retrieval Augment Code Generation? [78.37076502395699]
  検索拡張生成を用いたコード生成の系統的,大規模な解析を行う。 まず、コード生成タスクの3つのカテゴリを含む総合的な評価ベンチマークであるCodeRAG-Benchをキュレートする。 CodeRAG-Bench上のトップパフォーマンスモデルについて、1つまたは複数のソースから検索したコンテキストを提供することにより検討する。
  論文  参考訳（メタデータ） (2024-06-20T16:59:52Z)
• LimGen: Probing the LLMs for Generating Suggestive Limitations of Research Papers [8.076841611508488]
  本稿では,研究論文におけるSLG(Suggestive Limitation Generation)の新たな課題について紹介する。 我々は textbftextitLimGen というデータセットをコンパイルし、4068 の研究論文とそれに関連する ACL アンソロジーの制限を包含する。
  論文  参考訳（メタデータ） (2024-03-22T17:31:43Z)
• ML-Bench: Evaluating Large Language Models and Agents for Machine Learning Tasks on Repository-Level Code [76.84199699772903]
  ML-Benchは、既存のコードリポジトリを利用してタスクを実行する現実世界のプログラミングアプリケーションに根ざしたベンチマークである。 LLM(Large Language Model)とAIエージェントの両方を評価するために、事前に定義されたデプロイメント環境でLLMのテキスト-コード変換を評価するML-LLM-Benchと、Linuxサンドボックス環境でエンドツーエンドのタスク実行で自律エージェントをテストするML-Agent-Benchの2つの設定が採用されている。
  論文  参考訳（メタデータ） (2023-11-16T12:03:21Z)
• Evaluating, Understanding, and Improving Constrained Text Generation for Large Language Models [49.74036826946397]
  本研究では,大言語モデル(LLM)の制約付きテキスト生成について検討する。 本研究は主に,制約を語彙型,構造型,関係型に分類するオープンソース LLM に重点を置いている。 その結果、LLMの能力と不足を照らし、制約を取り入れ、制約付きテキスト生成における将来の発展に対する洞察を提供する。
  論文  参考訳（メタデータ） (2023-10-25T03:58:49Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。