論文の概要: 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) 学習ルールを用いて,既存の戦術選択アプローチの出力をフィルタリングし,非フィルタリングアプローチに対する改善を実証的に示す。

関連論文リスト

• 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)
• Efficient Performance Bounds for Primal-Dual Reinforcement Learning from Demonstrations [1.0609815608017066]
  本稿では,コスト関数の不明な大規模マルコフ決定プロセスについて考察し,限られた専門家による実証から政策を学習する問題に対処する。 既存の逆強化学習法には強力な理論的保証があるが、計算上は高価である。 ラグランジアン双対性を利用して理論と実践のギャップを埋める新しい双線型サドルポイントフレームワークを導入する。
  論文  参考訳（メタデータ） (2021-12-28T05:47:24Z)
• Probing as Quantifying the Inductive Bias of Pre-trained Representations [99.93552997506438]
  本稿では,特定のタスクに対する表現の帰納的バイアスを評価することを目的とした,探索のための新しいフレームワークを提案する。 トークン、アーク、文レベルの一連のタスクに我々のフレームワークを適用します。
  論文  参考訳（メタデータ） (2021-10-15T22:01:16Z)
• MCDAL: Maximum Classifier Discrepancy for Active Learning [74.73133545019877]
  近年の最先端のアクティブラーニング手法は, 主にGAN(Generative Adversarial Networks)をサンプル取得に活用している。 本稿では,MCDAL(Maximum Discrepancy for Active Learning)と呼ぶ新しいアクティブラーニングフレームワークを提案する。 特に,両者の差分を最大化することにより,より厳密な決定境界を学習する2つの補助的分類層を利用する。
  論文  参考訳（メタデータ） (2021-07-23T06:57:08Z)
• 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)

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

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