論文の概要: On Compositional Learning Behaviours in Formal Mathematics

• arxiv url: http://arxiv.org/abs/2605.28512v1
• Date: Wed, 27 May 2026 14:15:04 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-28 17:38:56.100873
• Title: On Compositional Learning Behaviours in Formal Mathematics
• Title（参考訳）: 形式数学における構成学習行動について
• Authors: Kevin Yandoka Denamganaï,
• Abstract要約: textbfS2B-LMはシンボリックビヘイビアベンチマークの適応である。 CLB能力は必須であるが,形式的数学的検証の難しさには十分でないことを示す。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Self-evolving scientific agents capable of conquering the hard tail of formal mathematics require Compositional Learning Behaviours (CLBs) -- the capacity to ground and recombine novel symbolic structures in context, beyond mere recombination of prelearned atoms. We propose \textbf{S2B-LM}, an adaptation of the Symbolic Behaviour Benchmark that removes numerical processing as a confound and adds chain-of-thought scaffolding to elicit rather than merely probe latent CLB competency. Cross-evaluating ten Lean~4 theorem provers on CLB competency (adj-ZSCT) and miniF2F whole-proof performance, exact permutation tests establish a hierarchical necessity structure: search-heavy models cover the tractable bulk without detectable CLBs, yet every model breaking into the Olympiad-level tier (miniF2F $>75\%$) is among the five highest CLB scorers ($p=0.004$). After ruling out model scale as a confound, our results show that CLB competency is \emph{necessary but not sufficient} for the hard tail of formal mathematical verification.
• Abstract（参考訳）: 形式数学のハードテールを征服することのできる自己進化型科学エージェントは、合成学習行動(CLB)を必要とする。 本稿では,記号的振る舞いベンチマークの適応である‘textbf{S2B-LM} を提案する。 CLB 能力 (adj-ZSCT) と miniF2F に対する10のリーン–4 の定理プローバーを横断的に評価し、完全置換テストは階層的な必要構造を確立する: 探索重大モデルは検出不可能な CLB を包含するが、オリンピアードレベル層(miniF2F $>75\%$)に侵入する全てのモデルは5つの高いCLBスコアラーのうちの1つである(p=0.004$)。 この結果から,形式的数式検証のハードテールに対して,CLB の能力は 'emph{necessary, not not enough} であることが示唆された。

関連論文リスト

• Controlling Logical Collapse in LLMs via Algebraic Ontology Projection over F2 [0.0]
  代数オントロジー計画(Algebraic Ontology Projection, AOP)を導入し, LLM隠れ状態をガロアフィールドF2に投影する。 AOPは、目に見えないコンセプトペアに対して最大93.33%のゼロショットインクルージョン精度を達成する。 本稿では,F2制約満足度を定量化する指標であるSemantic Crystallisation(SC)を紹介する。
  論文  参考訳（メタデータ） (2026-05-13T04:01:29Z)
• BOFA: Bridge-Layer Orthogonal Low-Rank Fusion for CLIP-Based Class-Incremental Learning [84.56022893225422]
  CIL(Class-Incremental Learning)は,従来の知識を忘れずに,新たなカテゴリを継続的に学習することを目的としている。 CLIP から CIL への視覚言語モデルの適用には,次の2つの大きな課題がある。(1) 下流タスクへの適応には,新たな学習可能なモジュールを必要とする場合が多いこと,2) モデル複雑性の増大と忘れやすいこと,2) マルチモーダル表現は相補的な長所を提供する一方で,既存の手法では,視覚的およびテキスト的モダリティを効果的に統合する可能性を完全には実現できていない。
  論文  参考訳（メタデータ） (2025-11-14T15:51:40Z)
• FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory [44.64175433092553]
  大規模言語モデル (LLM) は、最近、形式定理の証明において顕著な進歩を見せている。 しかし、数学者の実践的なアシスタントとして機能する能力は、複雑な証明の中で欠落したステップを埋めるものであり、まだ解明されていない。 機械学習の基礎理論に基づいて構築された、リーン4ベンチマークであるFormalMLを紹介します。
  論文  参考訳（メタデータ） (2025-09-26T14:40:14Z)
• 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)
• Solving Formal Math Problems by Decomposition and Iterative Reflection [30.54275542622631]
  textbfDelta Proverは汎用LLMとLean 4の実証環境とのインタラクションを編成します。 bftextDelta Proverは、miniF2F-testベンチマークで、最先端の95.9%の成功率を達成した。
  論文  参考訳（メタデータ） (2025-07-21T03:56:35Z)
• A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation [3.003569769097376]
  コンビニティクスは数学の基盤であり、離散構造の分析と問題解決に不可欠なツールを提供する。 これを解決するために、手動でLeanCombを構築しました。 我々は,自己改善型大規模言語モデルによって提案される候補戦略と,予測のための強化学習木探索アプローチを組み合わせた,コンビニアル・アイデンティティのための自動定理ジェネレータATG4CIを開発した。
  論文  参考訳（メタデータ） (2025-02-25T04:41:49Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Theory on Mixture-of-Experts in Continual Learning [72.42497633220547]
  継続学習(CL)は、時間とともに現れる新しいタスクに適応する能力のため、大きな注目を集めている。 モデルが新しいタスクに適応するにつれて、(古いタスクの)破滅的な忘れがCLの大きな問題として認識されるようになった。 MoEモデルは近年,ゲーティングネットワークを用いることで,CLの破滅的忘れを効果的に軽減することが示されている。
  論文  参考訳（メタデータ） (2024-06-24T08:29:58Z)

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

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