論文の概要: Automated Planning Techniques for Elementary Proofs in Abstract Algebra

• arxiv url: http://arxiv.org/abs/2312.06490v1
• Date: Mon, 11 Dec 2023 16:17:43 GMT
• ステータス: 処理完了
• システム内更新日: 2023-12-12 14:52:21.056087
• Title: Automated Planning Techniques for Elementary Proofs in Abstract Algebra
• Title（参考訳）: 抽象代数における初等証明の自動計画手法
• Authors: Alice Petrov, Christian Muise
• Abstract要約: 抽象代数学における基本証明を構築するための計画法について検討する。 我々は、決定論的領域と非決定論的領域の両方において、基本的な意味、平等、および規則を実装している。 この初期実装の成功は、自動計画で見られる確立されたテクニックが、比較的新しい自動定理証明分野に適用可能であることを示唆している。
• 参考スコア（独自算出の注目度）: 5.379968204052965
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This paper explores the application of automated planning to automated theorem proving, which is a branch of automated reasoning concerned with the development of algorithms and computer programs to construct mathematical proofs. In particular, we investigate the use of planning to construct elementary proofs in abstract algebra, which provides a rigorous and axiomatic framework for studying algebraic structures such as groups, rings, fields, and modules. We implement basic implications, equalities, and rules in both deterministic and non-deterministic domains to model commutative rings and deduce elementary results about them. The success of this initial implementation suggests that the well-established techniques seen in automated planning are applicable to the relatively newer field of automated theorem proving. Likewise, automated theorem proving provides a new, challenging domain for automated planning.
• Abstract（参考訳）: 本稿では, 自動定理証明への自動計画の適用について検討する。これは, 数学的証明を構築するためのアルゴリズムとコンピュータプログラムの開発に関する自動推論の一分野である。 特に, 群, 環, 体, 加群といった代数構造を研究するための厳密で公理的な枠組みを提供する抽象代数学における初等的証明を構築するための計画法の使用について検討する。 我々は、可換環をモデル化し、それらの基本的な結果を推測するために、決定論的および非決定論的領域の両方に基本的な意味、等性、規則を実装する。 この初期実装の成功は、自動化計画に見られる確立されたテクニックが、比較的新しい自動定理証明分野に適用可能であることを示唆している。 同様に、自動定理証明は、自動計画のための新しい挑戦的な領域を提供する。

関連論文リスト

• LLM-Generated Heuristics for AI Planning: Do We Even Need Domain-Independence Anymore? [87.71321254733384]
  大規模言語モデル(LLM)は、特定の計画問題に適した計画手法を生成することができる。 LLMは、いくつかの標準IPCドメインで最先端のパフォーマンスを達成することができる。 これらの結果がパラダイムシフトを意味するのか、既存の計画手法をどのように補完するかについて議論する。
  論文  参考訳（メタデータ） (2025-01-30T22:21:12Z)
• Learning Quantitative Automata Modulo Theories [17.33092604696224]
  本稿では,学習者が帰納的推論によって有効なオートマトンを推論する,能動的学習アルゴリズムQUINTICを提案する。 本評価では, 累積, 減算, 積, 量的オートマトンを学習するために, 有理理論を利用する。
  論文  参考訳（メタデータ） (2024-11-15T21:51:14Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。 1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。 自己形式化定理文の自動意味評価を行う。
  論文  参考訳（メタデータ） (2024-05-27T14:35:10Z)
• A Hybrid System for Systematic Generalization in Simple Arithmetic Problems [70.91780996370326]
  本稿では,記号列に対する合成的および体系的推論を必要とする算術的問題を解くことができるハイブリッドシステムを提案する。 提案システムは,最も単純なケースを含むサブセットでのみ訓練された場合においても,ネストした数式を正確に解くことができることを示す。
  論文  参考訳（メタデータ） (2023-06-29T18:35:41Z)
• Reformulation Techniques for Automated Planning: A Systematic Review [4.83420384410068]
  ドメインに依存しない計画の基盤は、計画ロジックと知識モデルとの分離である。 過去数十年にわたり、改革技術の設計に多大な研究努力が注がれている。 本稿では,古典的計画の改革手法に関する大規模研究の体系的なレビューを行う。
  論文  参考訳（メタデータ） (2023-01-24T15:33:37Z)
• Goal Agnostic Planning using Maximum Likelihood Paths in Hypergraph World Models [1.370633147306388]
  本稿では,ハイパーグラフに基づく機械学習アルゴリズム,データ構造駆動型メンテナンス手法,およびDijkstraのアルゴリズムの確率的応用に基づく計画アルゴリズムを提案する。 このアルゴリズムが問題空間内の最適解を決定すること、数学的に有界な学習性能を証明し、時間を通してシステム状態の進行を解析する数学的モデルを提供する。
  論文  参考訳（メタデータ） (2021-10-18T16:22:33Z)
• Refining Labelled Systems for Modal and Constructive Logics with Applications [0.0]
  この論文は、モーダル論理や構成論理のセマンティクスを「経済的な」証明システムに変換する手段として機能する。 精製法は、ラベル付きおよびネストされたシーケント計算の2つの証明理論パラダイムを結合する。 導入された洗練されたラベル付き電卓は、デオン性STIT論理に対する最初の証明探索アルゴリズムを提供するために使用される。
  論文  参考訳（メタデータ） (2021-07-30T08:27:15Z)
• Induction and Exploitation of Subgoal Automata for Reinforcement Learning [75.55324974788475]
  本稿では,Regressed Learning (RL)タスクにおけるサブゴールの学習と活用のためのISAを提案する。 ISAは、タスクのサブゴールによってエッジがラベル付けされたオートマトンであるサブゴールオートマトンを誘導することで強化学習をインターリーブする。 サブゴールオートマトンはまた、タスクの完了を示す状態と、タスクが成功せずに完了したことを示す状態の2つの特別な状態で構成されている。
  論文  参考訳（メタデータ） (2020-09-08T16:42:55Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)
• A General Framework for Consistent Structured Prediction with Implicit Loss Embeddings [113.15416137912399]
  構造化予測のための理論的・アルゴリズム的な枠組みを提案し,解析する。 問題に対して適切な幾何を暗黙的に定義する、損失関数の大規模なクラスについて検討する。 出力空間を無限の濃度で扱うとき、推定子の適切な暗黙の定式化が重要であることが示される。
  論文  参考訳（メタデータ） (2020-02-13T10:30:04Z)

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

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