論文の概要: Definition Grounding in Theory-Level Auto-formalization

• arxiv url: http://arxiv.org/abs/2610.19223v1
• Date: Tue, 13 Oct 2026 21:42:35 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-15 21:06:15.817749
• Title: Definition Grounding in Theory-Level Auto-formalization
• Title（参考訳）: 理論レベルオートフォーマライゼーションにおける定義グラウンド
• Abstract要約: 本稿では,定義の形式化を継続的に判断し,改訂する定義基盤を提案する。 テキストから定義を定式化するエージェントは、後述の文では使用できない定義を生成することが多い。 非公式な定義を明確にすることで、すべてのモデルで平均77.5%までこの率を改善することができる。
• 参考スコア（独自算出の注目度）: 13.700877530474017
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: LLM-based auto-formalization systems can now generate formally verified Lean code at unprecedented rates. However, a formalization advances mathematical research only when further mathematical results can be built on it, especially when its definitions and helper lemmas are general enough to be imported and used idiomatically. We propose definition grounding, where definition formalizations are continuously judged and revised, as a method to ensure formalization quality. We find that agents formalizing definitions from textbook text often produce definitions that later statements cannot use, and only 25%-50% of their definition sets are compatible with all later statements. However, clarifying the informal definitions can improve this rate up to 77.5% averaged over all models. Furthermore, stating a small set of basic properties without proving them can improve model judges' capability to detect definitions with compatibility issues, at only about 11% of the definition formalization cost. These results are verified with ReuseBench, a benchmark we curated for formalizing new mathematical fields and theories.
• Abstract（参考訳）: LLMベースの自動形式化システムは、前例のない速度で正式に認証されたリーンコードを生成することができる。 しかし、形式化が数学的研究を前進させるのは、特にその定義とヘルパー補題が、慣用的にインポートされ使われるのに十分な一般性を持つ場合に限られる。 本稿では,定義の定式化を継続的に判断・修正し,定式化の品質を確保する方法として定義基盤を提案する。 教科書のテキストから定義を形式化するエージェントは、後続の文では使用できない定義をしばしば生成し、その定義セットの25%-50%は後続の文と互換性がある。 しかし、非公式な定義を明確にすることで、すべてのモデルの平均77.5%まで改善できる。 さらに、基本的な性質の小さなセットを証明せずに記述することで、モデルの判断者が互換性のある定義を検出できる能力を向上させることができ、定義の定式化コストの11%に過ぎません。 これらの結果は、新しい数学の分野と理論を定式化するためのベンチマークであるReuseBenchで検証される。

関連論文リスト

• Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases [32.96018876882992]
  我々は、理論レベルの自己形式化について論じる: 完全な理論を形式化し、すべての依存関係を構造化ライブラリとして含む。 我々は,このシフトの重要性を検証し,代替の見解に対処し,オープンな課題を特定し,将来性のある3つの経路を提案する。
  論文  参考訳（メタデータ） (2026-07-14T21:58:52Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。 これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。 実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
  論文  参考訳（メタデータ） (2025-10-28T16:22:54Z)
• Structuring Definitions in Mathematical Libraries [0.6372261626436676]
  証明アシスタントや計算機代数システムにおける数学的理論の符号化は難しい課題である。 汎用性、可読性、使いやすさなど、考慮すべきことはたくさんあります。 本稿では、Lean Theorem Proverコミュニティが運営する数学ライブラリMathlibに最終的に追加された定義の精錬プロセスについて、いくつかのケーススタディについて検討する。
  論文  参考訳（メタデータ） (2025-09-13T14:47:24Z)
• 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)
• Reliable Evaluation and Benchmarks for Statement Autoformalization [18.218951526592914]
  改良されたメトリクス、堅牢なベンチマーク、体系的な評価を組み合わせた総合的なアプローチを提案する。 まず、評価指標の質を評価するための新しいデータセットであるProofNetVerifとともに、人間の判断と強く相関する自動メトリクスBEq+を紹介する。 ProofNet#はProofNetの修正版であり、RLM25は6つの形式化プロジェクトから619の新しい研究レベルの数学のペアである。
  論文  参考訳（メタデータ） (2024-06-11T13:01:50Z)
• Pre-training and Diagnosing Knowledge Base Completion Models [58.07183284468881]
  我々は,事実の集合から他の集合への知識伝達へのアプローチを,エンティティや関係マッチングを必要とせずに導入し,分析する。 主な貢献は、構造化されていないテキストから収集された事実の大規模事前学習を利用する方法である。 得られた事前学習モデルをよりよく理解するために,オープン知識ベースコンプリートのための事前学習モデルの解析のための新しいデータセットを導入する。
  論文  参考訳（メタデータ） (2024-01-27T15:20:43Z)
• "Definition Modeling: To model definitions." Generating Definitions With Little to No Semantics [0.4061135251278187]
  我々は、このタスクが期待するほど意味論を含まないかもしれないという証拠を提示する。 文献から得られた先行モデルは、明示的なポリセミズムのような意味的側面にかなり敏感であることを示す。
  論文  参考訳（メタデータ） (2023-06-14T11:08:38Z)
• Prompt Algebra for Task Composition [131.97623832435812]
  素早いチューニングを伴うビジュアル言語モデルを基本分類器として検討する。 合成分類器の性能向上のための制約付きプロンプトチューニングを提案する。 UTZapposでは、最高のベースモデルに対する分類精度を平均8.45%向上させる。
  論文  参考訳（メタデータ） (2023-06-01T03:20:54Z)
• Enriching Disentanglement: From Logical Definitions to Quantitative Metrics [59.12308034729482]
  複雑なデータにおける説明的要素を遠ざけることは、データ効率の表現学習にとって有望なアプローチである。 論理的定義と量的指標の関連性を確立し, 理論的に根ざした絡み合いの指標を導出する。 本研究では,非交叉表現の異なる側面を分離することにより,提案手法の有効性を実証的に実証する。
  論文  参考訳（メタデータ） (2023-05-19T08:22:23Z)
• Lexical Sememe Prediction using Dictionary Definitions by Capturing Local Semantic Correspondence [94.79912471702782]
  セメムは人間の言語の最小の意味単位として定義されており、多くのNLPタスクで有用であることが証明されている。 本稿では,このようなマッチングを捕捉し,セメムを予測できるセメム対応プールモデルを提案する。 我々は,有名なSememe KB HowNetのモデルとベースライン手法を評価し,そのモデルが最先端のパフォーマンスを実現することを発見した。
  論文  参考訳（メタデータ） (2020-01-16T17:30:36Z)

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

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