論文の概要: TREAT: Evaluating Access to Formal Knowledge across Equivalent Mathematical Representations

• arxiv url: http://arxiv.org/abs/2608.07540v1
• Date: Wed, 29 Jul 2026 23:02:46 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-08-17 01:32:04.557765
• Title: TREAT: Evaluating Access to Formal Knowledge across Equivalent Mathematical Representations
• Title（参考訳）: TREAT: 等価な数式表現による形式的知識へのアクセスの評価
• Authors: Fateme Mazdarani, Carlos Toxtli,
• Abstract要約: 鍵となる課題は、未知の定式化が既知の形式的対象を表すときを認識することである。 Treatは、大きな言語モデルが既知の定理のアイデンティティを復元できるかどうかを評価するためのベンチマークである。 Treatは、形式的知識への表現不正アクセスを評価するための制御されたテストベッドを提供する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: AI systems increasingly operate between flexible input representations and formal objects used by downstream tools. A key challenge is recognizing when an unfamiliar formulation denotes a known formal object. We study this challenge through theorem recognition: given an equivalence-preserving transformation of a theorem condition, a model must recover the theorem identity associated with the standard statement. We introduce TREAT, a benchmark for evaluating whether large language models can recover known theorem identities from equivalence-preserving formula-level transformations. Rather than paraphrasing theorem text, TREAT changes the mathematical form of theorem conditions themselves, expressing known results through residual equations, witness statements, optimization identities, set relations, operator forms, and proof-intermediate characterizations. Starting from scraped theorem pages, we filter for entries with usable mathematical expression forms, extract canonical theorem conditions, and generate transformed variants with recorded assumptions and inverse mappings. The final corpus contains 737 theorem identities and 29,480 transformed rows. On a test panel, the best model retrieves the correct theorem identity in only 60.73% of cases. Other systems reveal different failure modes, including abstention, wrong detection, and malformed outputs. These suggest that theorem knowledge can be fragile under equivalent changes in representation. TREAT therefore provides a controlled testbed for evaluating representation-robust access to formal knowledge, with broader relevance to domains that require stable target objects, explicit equivalence relations, validation procedures, and auditable scoring.
• Abstract（参考訳）: AIシステムは、フレキシブルな入力表現と、下流ツールで使用されるフォーマルなオブジェクトの間をますます運用している。 重要な課題は、未知の定式化が既知の形式的対象を表すときの認識である。 定理条件の同値保存変換が与えられた場合、モデルは標準文に関連する定理の同一性を取り戻す必要がある。 我々は,大言語モデルが等価保存式レベルの変換から既知の定理のアイデンティティを復元できるかどうかを評価するためのベンチマークであるTREATを紹介する。 定理のテキストを言い換えるのではなく、TREATは定理条件自体の数学的形式を変更し、残差方程式、証人文、最適化ID、集合関係、演算子形式、証明中間的特徴を通して既知の結果を表現している。 スクラップ化された定理ページから、使用可能な数学的表現形式を持つエントリをフィルタリングし、標準定理条件を抽出し、記録された仮定と逆写像で変換された変分を生成する。 最終コーパスは737個の定理IDと29,480個の変換列を含む。 テストパネルでは、最良のモデルは60.73%のケースで正しい定理の恒等性を取得する。 他のシステムでは、棄権、誤検出、不正な出力など、さまざまな障害モードが示される。 これらのことは、定理の知識が表現の等価な変化の下で脆弱であることが示唆される。 したがって、TREATは、安定なターゲットオブジェクト、明示的な等価関係、検証手順、監査可能なスコアリングを必要とするドメインに幅広い関連性を持って、形式的知識への表現-不正アクセスを評価するための制御されたテストベッドを提供する。

関連論文リスト

• Representation Robustness Under Executable Reasoning Constraints in Large Language Models for Mathematical Problem Solving [3.0618862102164996]
  本稿では,大規模言語モデル(LLM)における表現ロバスト性について検討する。 我々は、物語、記号、単語方程式の変種にまたがる非自明なフリップレートで、かなりの表現感度を見出した。 LLMの評価と展開において、表現は第一級インタフェース設計変数として扱われるべきである。
  論文  参考訳（メタデータ） (2026-07-08T17:21:28Z)
• Finite Certificates for In-Context Determinacy and a Threshold Theory of Emergence in Language Models [0.2864713389096699]
  本稿では,文脈条件付き言語モデル行動を検証するためのモデル理論フレームワークを開発する。 有限コンテキスト証明書、ペアセパレータのヒットセット、クエリ教育のディメンション、プロンプト保存基準、スケール制限証人を提供する。
  論文  参考訳（メタデータ） (2026-05-30T14:07:58Z)
• What are the Right Symmetries for Formal Theorem Proving? [23.981613344642152]
  意味論的に等価な文は、非常に異なる証明成功率を示すことを示す。 これは中心的な疑問を提起する: 形式的定理証明の適切な対称性は何か? 証明戦術によって誘導される構成的、一般的には非可逆な変換をキャプチャーするカテゴリ理論フレームワークである書字カテゴリを導入する。
  論文  参考訳（メタデータ） (2026-05-21T10:00:47Z)
• Benchmarking Testing in Automated Theorem Proving [39.65133452374143]
  T は形式定理の意味的正しさを評価する枠組みである。 5つの実世界のLean 4リポジトリからベンチマークを構築します。 実験により、最先端のモデルでは高いコンパイル成功を達成できるが、セマンティック・メトリックでは著しく性能が低下することが示された。
  論文  参考訳（メタデータ） (2026-04-26T13:24:20Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。 DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。 我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
  論文  参考訳（メタデータ） (2025-05-29T17:59:39Z)
• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
  本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。 本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。 現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
  論文  参考訳（メタデータ） (2025-05-05T15:37:00Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)

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

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