論文の概要: Learning Rules Explaining Interactive Theorem Proving Tactic Prediction

• arxiv url: http://arxiv.org/abs/2411.01188v1
• Date: Sat, 02 Nov 2024 09:18:33 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-11-05 14:49:15.694528
• Title: Learning Rules Explaining Interactive Theorem Proving Tactic Prediction
• Title（参考訳）: 対話的理論を用いた戦術予測の学習ルール
• Authors: Liao Zhang, David M. Cerna, Cezary Kaliszyk,
• Abstract要約: この問題を帰納論理プログラミング(ILP)タスクとして表現する。 ILP表現を使用することで、追加で計算コストの高いプロパティをエンコードすることで、機能空間を豊かにしました。 我々は、このリッチな特徴空間を用いて、与えられた証明状態に戦術がいつ適用されたかを説明する規則を学ぶ。
• 参考スコア（独自算出の注目度）: 5.229806149125529
• License:
• Abstract: Formally verifying the correctness of mathematical proofs is more accessible than ever, however, the learning curve remains steep for many of the state-of-the-art interactive theorem provers (ITP). Deriving the most appropriate subsequent proof step, and reasoning about it, given the multitude of possibilities, remains a daunting task for novice users. To improve the situation, several investigations have developed machine learning based guidance for tactic selection. Such approaches struggle to learn non-trivial relationships between the chosen tactic and the structure of the proof state and represent them as symbolic expressions. To address these issues we (i) We represent the problem as an Inductive Logic Programming (ILP) task, (ii) Using the ILP representation we enriched the feature space by encoding additional, computationally expensive properties as background knowledge predicates, (iii) We use this enriched feature space to learn rules explaining when a tactic is applicable to a given proof state, (iv) we use the learned rules to filter the output of an existing tactic selection approach and empirically show improvement over the non-filtering approaches.
• Abstract（参考訳）: 数学的証明の正しさを形式的に検証することは、これまで以上に容易に行えるが、最先端の対話的定理証明者(ITP)の多くにとって、学習曲線は急勾配のままである。 その後の最も適切な証明手順を導き、その可能性の多さを考えると、初心者ユーザーにとっては大変な作業だ。 状況を改善するため、いくつかの調査が戦術選択のための機械学習に基づくガイダンスを開発した。 このようなアプローチは、選択された戦術と証明状態の構造の間の非自明な関係を学習し、それらを象徴的な表現として表すのに苦労する。 これらの問題に対処するために (i)帰納的論理プログラミング(ILP)タスクとして問題を表現する。 2) ILP表現を用いて, 背景知識の述語として, 計算コストのかかる付加的特性を符号化することにより, 特徴空間を充実させた。 三 この充実した特徴空間を用いて、ある戦術が所定の証明状態に適用されたときのルールを学習する。 (4) 学習ルールを用いて,既存の戦術選択アプローチの出力をフィルタリングし,非フィルタリングアプローチに対する改善を実証的に示す。

関連論文リスト

• Online inductive learning from answer sets for efficient reinforcement learning exploration [52.03682298194168]
  エージェントポリシーの近似を説明可能な近似を表す論理規則の集合を学習するために,帰納的な解集合プログラムの学習を利用する。 次に、学習ルールに基づいて回答セット推論を行い、次のバッチで学習エージェントの探索をガイドします。 本手法は,初回トレーニングにおいても,エージェントが達成した割引リターンを著しく向上させる。
  論文  参考訳（メタデータ） (2025-01-13T16:13:22Z)
• On the Loss of Context-awareness in General Instruction Fine-tuning [101.03941308894191]
  教師付き微調整後の文脈認識の喪失について検討した。 性能低下は,会話指導の微調整中に学んだ異なる役割に対する偏見と関連していることがわかった。 一般命令微調整データセットから文脈依存例を識別する指標を提案する。
  論文  参考訳（メタデータ） (2024-11-05T00:16:01Z)
• Interpretable Anomaly Detection via Discrete Optimization [1.7150329136228712]
  本稿では,シーケンシャルデータから本質的に解釈可能な異常検出を学習するためのフレームワークを提案する。 この問題は計算的に困難であることを示し,制約最適化に基づく2つの学習アルゴリズムを開発した。 プロトタイプ実装を用いて,提案手法は精度とF1スコアの点で有望な結果を示す。
  論文  参考訳（メタデータ） (2023-03-24T16:19:15Z)
• Lexicographic Multi-Objective Reinforcement Learning [65.90380946224869]
  このような問題を解決するために,アクション値アルゴリズムとポリシー勾配アルゴリズムの両方のファミリを提案する。 エージェントの動作に安全制約を課すのに我々のアルゴリズムをどのように使用できるかを示し、この文脈でのそれらの性能を他の制約付き強化学習アルゴリズムと比較する。
  論文  参考訳（メタデータ） (2022-12-28T10:22:36Z)
• Reinforcement Learning in Presence of Discrete Markovian Context Evolution [7.467644044726776]
  a) 直接観測不可能な文脈の未知の有限個の数、b) エピソード中に突然発生する(不連続な)文脈変化、c) マルコフ的文脈進化を特徴とする文脈依存強化学習環境を考える。 我々はモデル学習に先立って、粘着した階層的ディリクレプロセス(HDP)を適用する。 これら2つのコンポーネントの組み合わせによって、コンテキストの濃度仮定を扱うデータからコンテキストの数を推測することが可能である、と我々は主張する。
  論文  参考訳（メタデータ） (2022-02-14T08:52:36Z)
• TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning [6.764610878007278]
  深層強化学習を用いた対話型定理証明(ITP)の新しい手法を提案する。 我々は、各状態が潜在的な導出経路の集合を表すマルコフ決定プロセス(MDP)としてITPのプロセスを定式化する。 このフレームワークは、人間の専門家を使ったアプローチに匹敵するパフォーマンスを提供する。
  論文  参考訳（メタデータ） (2021-02-19T06:08:39Z)
• Multi-Agent Reinforcement Learning with Temporal Logic Specifications [65.79056365594654]
  本研究では,時間論理仕様を満たすための学習課題を,未知の環境下でエージェントのグループで検討する。 我々は、時間論理仕様のための最初のマルチエージェント強化学習手法を開発した。 主アルゴリズムの正確性と収束性を保証する。
  論文  参考訳（メタデータ） (2021-02-01T01:13:03Z)
• Learning Implicitly with Noisy Data in Linear Arithmetic [94.66549436482306]
  PAC-セマンティックスにおける暗黙学習を拡張し、線形算術の言語における間隔としきい値の不確実性を扱う。 最適線形プログラミング対象制約の学習に対する我々の暗黙的アプローチは、実際的な明示的アプローチよりも著しく優れていることを示す。
  論文  参考訳（メタデータ） (2020-10-23T19:08:46Z)
• Can We Learn Heuristics For Graphical Model Inference Using Reinforcement Learning? [114.24881214319048]
  我々は、強化学習を用いて、高次条件ランダム場(CRF)における推論を解くためのプログラム、すなわち、ポリシーを学習できることを示します。 本手法は,ポテンシャルの形式に制約を加えることなく,推論タスクを効率的に解く。
  論文  参考訳（メタデータ） (2020-04-27T19:24:04Z)

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

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