Fugu-MT 論文翻訳(概要): Partial Label Learning for Automated Theorem Proving

論文の概要: Partial Label Learning for Automated Theorem Proving

arxiv url: http://arxiv.org/abs/2507.03314v1
Date: Fri, 04 Jul 2025 05:54:27 GMT
ステータス: 翻訳完了
システム内更新日: 2025-07-08 15:46:34.673755
Title: Partial Label Learning for Automated Theorem Proving
Title（参考訳）: 自動定理証明のための部分ラベル学習
Authors: Zsolt Zombori, Balázs Indruck,
Abstract要約: 部分的なラベル学習として自動定理証明を導出した学習を定式化する。 plCoP定理証明器を用いて、部分ラベル学習文献からの手法が学習支援定理証明器の性能を向上させる傾向があることを示す。
参考スコア（独自算出の注目度）: 0.0
License: http://creativecommons.org/licenses/by/4.0/
Abstract: We formulate learning guided Automated Theorem Proving as Partial Label Learning, building the first bridge across these fields of research and providing a theoretical framework for dealing with alternative proofs during learning. We use the plCoP theorem prover to demonstrate that methods from the Partial Label Learning literature tend to increase the performance of learning assisted theorem provers.
Abstract（参考訳）: これらの研究分野にまたがる最初の橋梁を構築し、学習中に代替証明を扱うための理論的枠組みを提供する。 plCoP定理証明器を用いて、部分ラベル学習文献からの手法が学習支援定理証明器の性能を向上させる傾向があることを示す。

関連論文リスト

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)
Learning Rules Explaining Interactive Theorem Proving Tactic Prediction [5.229806149125529]
この問題を帰納論理プログラミング(ILP)タスクとして表現する。 ILP表現を使用することで、追加で計算コストの高いプロパティをエンコードすることで、機能空間を豊かにしました。我々は、このリッチな特徴空間を用いて、与えられた証明状態に戦術がいつ適用されたかを説明する規則を学ぶ。
論文参考訳（メタデータ） (2024-11-02T09:18:33Z)
Decorrelation-based Self-Supervised Visual Representation Learning for Writer Identification [10.55096104577668]
本稿では,自己教師型学習のデコリレーションに基づくパラダイムを探求し,著者識別のための不整合脳卒中の特徴の学習に適用する。提案手法は,著者識別ベンチマークにおいて,現代の自己教師型学習フレームワークよりも優れていることを示す。我々の知る限り、本研究は、著者検証タスクの学習表現に自己教師付き学習を適用した最初のものである。
論文参考訳（メタデータ） (2024-10-02T11:43:58Z)
Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文参考訳（メタデータ） (2024-07-14T01:43:07Z)
Aligning Logits Generatively for Principled Black-Box Knowledge Distillation [49.43567344782207]
Black-Box Knowledge Distillation (B2KD)は、クラウドからエッジへのモデル圧縮において、サーバ上にホストされる見えないデータとモデルによって定式化された問題である。民営化と蒸留による2段階のワークフローを形式化する。そこで本研究では,ブラックボックスの煩雑なモデルを軽量に蒸留するKD (MEKD) を新たに提案する。
論文参考訳（メタデータ） (2022-05-21T02:38:16Z)
Learning to Guide a Saturation-Based Theorem Prover [9.228237801323042]
TRAILは、ニューラルネットワーク内で証明される飽和に基づく定理の中核要素を特徴付ける、深い学習に基づく定理証明のアプローチである。我々の知る限りでは、TRAILは最先端の伝統的な定理証明器の性能を超える最初の強化学習に基づくアプローチである。
論文参考訳（メタデータ） (2021-06-07T18:35:57Z)
TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning [6.764610878007278]
深層強化学習を用いた対話型定理証明(ITP)の新しい手法を提案する。我々は、各状態が潜在的な導出経路の集合を表すマルコフ決定プロセス(MDP)としてITPのプロセスを定式化する。このフレームワークは、人間の専門家を使ったアプローチに匹敵するパフォーマンスを提供する。
論文参考訳（メタデータ） (2021-02-19T06:08:39Z)
Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文参考訳（メタデータ） (2020-02-17T16:06:02Z)
An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic [13.633012068936894]
本研究では,一般的なグラフベースエンコーディングを持つ現行システムに適用されるパターンベースの埋め込みについて,実験的に比較する。実験により、より複雑なグラフベースの埋め込みにより、より単純な実行時の符号化方式の利点が打ち消されることが示された。
論文参考訳（メタデータ） (2020-02-02T16:07:15Z)

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