論文の概要: Predicting the Next State Is Not Enough: JEPA Representations for Lean Theorem Proving

• arxiv url: http://arxiv.org/abs/2609.32908v1
• Date: Sat, 26 Sep 2026 19:59:26 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-06 12:06:34.964786
• Title: Predicting the Next State Is Not Enough: JEPA Representations for Lean Theorem Proving
• Title（参考訳）: 次の状態を予測するだけでは十分ではない - JEPAによるリーン理論の証明
• Abstract要約: 一段階のリーン移行が分岐順序付けのための自己教師付き信号を提供するかどうかを検討する。 JEPAスタイルのモデルは、潜伏した後継表現を予測し、カーネル検証された非終端的な後継のみをスコアする。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Neural theorem provers must both propose tactics and decide which valid successor states to explore. We study whether one-step Lean transitions provide a self-supervised signal for branch ordering. A JEPA-style model predicts latent successor representations and scores only kernel-validated, nonterminal successors generated by a fixed pretrained ByT5 proposer. JEPA achieves higher Top-1 than matched InfoNCE on a same-theorem ranking diagnostic(50.18% versus 31.55%), but averages 282.3 of 987 solved theorems across three seeds versus 308 for proposer ordering, while requiring more tactic checks. In this setting, accurate one-step transition ranking is therefore insufficient as a long-horizon search value. The controlled evaluation separates representation from proposal quality and treats kernel-checked proof completion as the primary endpoint.
• Abstract（参考訳）: ニューラル定理の証明者はどちらも戦術を提案し、どの有効な後継者国家を探索するかを決定する必要がある。 一段階のリーン移行が分岐順序付けのための自己教師付き信号を提供するかどうかを検討する。 JEPAスタイルのモデルは、遅延した後継表現を予測し、固定事前訓練されたBYT5プロジェクタによって生成されるカーネル検証された非終端後継のみをスコアする。 JEPAは、一致したInfoNCEよりも高いTop-1を達成する(50.18%対31.55%)が、平均的な987の282.3は、3つの種にまたがる定理を解いた。 この設定では、長い水平探索値として正確なワンステップ遷移ランキングが不十分である。 制御された評価は、提案品質から表現を分離し、カーネルチェックされた証明完了を一次エンドポイントとして扱う。

関連論文リスト

• The SIGReg Objective as Variational Free Energy: A Theoretical Active-Inference Account of JEPA World Models [47.471225029744424]
  JEPA(Joint-Embedding Predictive Architectures)は、潜在世界モデルの主要な設計である。 本稿では,JEPAのトレーニング目標である予測損失と重み付き埋め込み正規化の選択肢が,有効能動推論(AIF)変動自由エネルギーであるか否かを判定する。
  論文  参考訳（メタデータ） (2026-07-15T08:59:36Z)
• When LLMs Agree, Are They Right? Auditing Self-Consistency and Cross-Model Agreement as Confidence Signals [0.0]
  LLM-as-judgeは、企業パイプラインでAIシステムを評価する上で、ますますデフォルトになっている。 判断者間の整合性、あるいはモデル自身のサンプルが正当性を示していることを示す。 大規模なクロスランナー研究において、合意がいつ有用なプロキシであるかを問う。
  論文  参考訳（メタデータ） (2026-07-09T02:46:51Z)
• Knowledge Index of Noah's Ark [63.143852586221534]
  KINAは,261分野にわたる899項目のベンチマークである。 ボーナス・オン・バートーナメントがFOSDを弱く支配していることを示す。 トップモデルであるGemini-3.1-Pro-Previewは53.17%、Claude-Opus-4.6は49.92%、GPT-5.4は48.55%に達した。
  論文  参考訳（メタデータ） (2026-06-03T17:06:49Z)
• Benchmarking Testing in Automated Theorem Proving [39.65133452374143]
  T は形式定理の意味的正しさを評価する枠組みである。 5つの実世界のLean 4リポジトリからベンチマークを構築します。 実験により、最先端のモデルでは高いコンパイル成功を達成できるが、セマンティック・メトリックでは著しく性能が低下することが示された。
  論文  参考訳（メタデータ） (2026-04-26T13:24:20Z)
• Towards Anytime-Valid Statistical Watermarking [63.02116925616554]
  我々は、任意の時間価推論で最適なサンプリングを統一する、最初のe-value-based watermarking frameworkであるAnchored E-Watermarkingを開発した。 本フレームワークはサンプル効率を大幅に向上させ,最先端のベースラインに対して,検出に必要な平均トークン予算を13～15%削減する。
  論文  参考訳（メタデータ） (2026-02-19T18:32:26Z)
• When Does Confidence-Based Cascade Deferral Suffice? [69.28314307469381]
  カスケードは、推論コストをサンプル毎に適応的に変化させる古典的な戦略である。 deferralルールは、シーケンス内の次の分類子を呼び出すか、または予測を終了するかを決定する。 カスケードの構造に執着しているにもかかわらず、信頼に基づく推論は実際は極めてうまく機能することが多い。
  論文  参考訳（メタデータ） (2023-07-06T04:13:57Z)

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

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