論文の概要: Structuring Definitions in Mathematical Libraries

• arxiv url: http://arxiv.org/abs/2509.10828v1
• Date: Sat, 13 Sep 2025 14:47:24 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-16 17:26:22.801282
• Title: Structuring Definitions in Mathematical Libraries
• Title（参考訳）: 数理ライブラリーにおける構造的定義
• Authors: Alena Gusakov, Peter Nelson, Stephen Watt,
• Abstract要約: 証明アシスタントや計算機代数システムにおける数学的理論の符号化は難しい課題である。 汎用性、可読性、使いやすさなど、考慮すべきことはたくさんあります。 本稿では、Lean Theorem Proverコミュニティが運営する数学ライブラリMathlibに最終的に追加された定義の精錬プロセスについて、いくつかのケーススタディについて検討する。
• 参考スコア（独自算出の注目度）: 0.6372261626436676
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Codifying mathematical theories in a proof assistant or computer algebra system is a challenging task, of which the most difficult part is, counterintuitively, structuring definitions. This results in a steep learning curve for new users and slow progress in formalizing even undergraduate level mathematics. There are many considerations one has to make, such as level of generality, readability, and ease of use in the type system, and there are typically multiple equivalent or related definitions from which to choose. Often, a definition that is ultimately selected for formalization is settled on after a lengthy trial and error process. This process involves testing potential definitions for usability by formalizing standard theorems about them, and weeding out the definitions that are unwieldy. Inclusion of a formal definition in a centralized community-run mathematical library is typically an indication that the definition is "good." For this reason, in this survey, we make some observations about what makes a definition "good," and examine several case studies of the refining process for definitions that have ultimately been added to the Lean Theorem Prover community-run mathematical library, mathlib. We observe that some of the difficulties are shared with the design of libraries for computer algebra systems, and give examples of related issues in that context.
• Abstract（参考訳）: 証明アシスタントや計算機代数システムにおける数学的理論の符号化は難しい課題であり、最も難しいのは定義を非意図的に構造化することである。 これにより、新入生の学習曲線が急激になり、学部レベルの数学の定式化が遅くなる。 汎用性のレベル、可読性、型システムでの使いやすさなど、考慮すべきことはたくさんあります。 多くの場合、形式化のために最終的に選択される定義は、長い試行錯誤の後に解決される。 このプロセスは、それらの標準的な定理を定式化することで、ユーザビリティに関する潜在的な定義をテストし、扱いにくい定義を取り除くことを含む。 中央集権的なコミュニティが運営する数学図書館における形式的定義の含意は、一般的にこの定義が「良い」ものであることを示す指標である。 このような理由から,本調査では,定義を「よい」ものにするためのいくつかの考察を行い,最終的にLean Theorem Proverコミュニティが運営する数学ライブラリであるmathlibに追加された定義の精錬プロセスについて,いくつかのケーススタディについて検討する。 問題の一部は計算機代数システムのためのライブラリの設計と共有され、その文脈における関連する問題の例を示す。

関連論文リスト

• Automated Formalization via Conceptual Retrieval-Augmented LLMs [19.328918823576153]
  CRAMFは概念駆動のRetrieval-Augmented Mathematical Formalizationフレームワークである。 概念定義知識ベースをMathlib4から自動構築するフレームワークを提案する。 miniF2F, ProofNet, そして新たに提案したAdvancedMathベンチマークでは, CRAMF を LLM ベースのオートフォーマライザにシームレスに統合できることが示されている。
  論文  参考訳（メタデータ） (2025-08-09T10:54:25Z)
• Critical Thinking: Which Kinds of Complexity Govern Optimal Reasoning Length? [72.70486097967124]
  決定論的有限オートマトン(DFAs)を用いたフレームワークの定式化 正しい解を生成する確率が最大になるような推論トークンが最適に存在することを示す。 新たな問題に対する推論トークンの最適個数を予測し、最適でない回答をフィルタリングすることで、一貫した精度の向上が得られる。
  論文  参考訳（メタデータ） (2025-04-02T17:45:58Z)
• A Complexity-Based Theory of Compositionality [53.025566128892066]
  AIでは、構成表現は配布外一般化の強力な形式を可能にすることができる。 ここでは、構成性に関する直観を考慮し、拡張する、表現的構成性と呼ばれる定義を提案する。 私たちは、AIと認知科学の両方において、文学全体から異なる直観を統一する方法を示します。
  論文  参考訳（メタデータ） (2024-10-18T18:37:27Z)
• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。 LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。 これは23のリーンリポジトリにわたる155の定理の正式な証明を生成する。
  論文  参考訳（メタデータ） (2024-10-08T17:11:24Z)
• Graph2Tac: Online Representation Learning of Formal Math Concepts [0.6597195879147557]
  証明において、2つの形式的な数学的概念の間の物理的近接は、それらの相互関係の強い予測因子である。 この局所性特性はオンライン学習技術によって利用でき、オフライン学習者を超えている問題解決エージェントが得られることを示す。 我々は、Coq証明アシスタントのためにTacticianプラットフォームで実装された2つのオンライン解決器をベンチマークした。
  論文  参考訳（メタデータ） (2024-01-05T18:52:09Z)
• Peano: Learning Formal Mathematical Reasoning [35.086032962873226]
  一般的な数学的推論は計算不可能であるが、人間は新しい問題を常に解決している。 両パズルの中心は、数学の基礎となる手続き的抽象の構造であると仮定する。 カーン・アカデミー・プラットフォーム上の始点代数の5つの部分に関するケーススタディにおいて、このアイデアを探求する。
  論文  参考訳（メタデータ） (2022-11-29T01:42:26Z)
• Provable Reinforcement Learning with a Short-Term Memory [68.00677878812908]
  我々はPMDPsの新しいサブクラスについて研究し、その潜在状態は、最近の短い長さ$m$の履歴によって復号化することができる。 特に、リッチ・オブザーブレーション・セッティングにおいて、指数関数的にスケールするサンプル複雑性を持つ新しい「モーメントマッチング」アプローチを用いて、新しいアルゴリズムを開発する。 以上の結果から,これらの環境下での強化学習には短期記憶が十分であることが示唆された。
  論文  参考訳（メタデータ） (2022-02-08T16:39:57Z)
• Sequential composition of answer set programs [0.0]
  本稿では,解集合プログラムの逐次構成を導入,研究することにより,論理プログラミングの数学的基礎に寄与する。 より広い意味では、本論文は、解集合プログラムの代数への第一歩であり、将来的には、この論文の手法をプログラムのより広範なクラスに引き上げる計画である。
  論文  参考訳（メタデータ） (2021-04-25T13:27:22Z)
• Computational linguistic assessment of textbook and online learning media by means of threshold concepts in business education [59.003956312175795]
  言語学的観点では、しきい値の概念は特別な語彙の例であり、特定の言語的特徴を示す。 ビジネス教育における63のしきい値の概念のプロファイルは、教科書、新聞、ウィキペディアで調査されている。 3種類のリソースは、しきい値の概念のプロファイルから区別できる。
  論文  参考訳（メタデータ） (2020-08-05T12:56:16Z)

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

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