論文の概要: Agent-Based Proof Design via Lemma Flow Diagram
- arxiv url: http://arxiv.org/abs/2002.00666v1
- Date: Mon, 3 Feb 2020 12:03:05 GMT
- ステータス: 処理完了
- システム内更新日: 2023-01-04 09:24:21.037346
- Title: Agent-Based Proof Design via Lemma Flow Diagram
- Title(参考訳): Lemma Flow Diagramによるエージェントベース証明設計
- Authors: Keehang Kwon and Daeseong Kang
- Abstract要約: エージェントによる証明設計と実装のアプローチを議論し、それをLemma Flow Diagram(LFD)と呼ぶ。
このアプローチは$shared$ cutsのマルチカットルールに基づいている。
- 参考スコア(独自算出の注目度): 1.90365714903665
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We discuss an agent-based approach to proof design and implementation, which
we call {\it Lemma Flow Diagram} (LFD). This approach is based on the multicut
rule with $shared$ cuts. This approach is modular and easy to use, read and
automate. Thus, we consider LFD an appealing alternative to `flow proof' which
is popular in mathematical education. Some examples are provided.
- Abstract(参考訳): 本稿では, エージェントによる証明設計と実装のアプローチについて論じ, LFD(it Lemma Flow Diagram) と呼ぶ。
このアプローチは$shared$ cutsのマルチカットルールに基づいている。
このアプローチはモジュール化されており、使いやすく、読みやすく、自動化できます。
そこで我々はlfdを,数理教育で普及している「フロー証明」の代替案と考える。
いくつか例を挙げる。
関連論文リスト
- MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [88.72298746872396]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳(メタデータ) (2024-02-14T05:57:58Z) - Learning Distributions on Manifolds with Free-form Flows [2.0891120283967264]
トレーニングは、最近提案されたフリーフォームフローフレームワークの適応によって達成される。
中心となる考え方は、接空間で評価されたトレースを通して負の対数様の勾配を推定することである。
従来の作業に比べて、競争性能での推測が大幅に速いことが分かりました。
論文 参考訳(メタデータ) (2023-12-15T14:58:34Z) - Amortizing intractable inference in large language models [56.92471123778389]
難治性後部分布のサンプルとして, 償却ベイズ推定を用いる。
我々は,LLMファインチューニングの分散マッチングパラダイムが,最大習熟の代替となることを実証的に実証した。
重要な応用として、チェーン・オブ・ソート推論を潜在変数モデリング問題として解釈する。
論文 参考訳(メタデータ) (2023-10-06T16:36:08Z) - Large Language Model Programs [74.31873455763275]
近年,大規模な事前学習型言語モデル (LLM) は,いくつかの例から指示に従うことや,新しいタスクを実行する能力を示している。
本稿では,この推論の行を拡張し,アルゴリズムやプログラムに組み込んでLLMの機能をさらに拡張する手法を提案する。
我々は、よりアルゴリズム的なアプローチにより、微調整をせずに、思考ベースラインの連鎖よりも6.4%改善する。
論文 参考訳(メタデータ) (2023-05-09T11:55:36Z) - Model-Based Reinforcement Learning with Multinomial Logistic Function
Approximation [12.36108042107798]
マルコフ決定過程におけるモデルに基づく強化学習について検討する。
我々は,多項ロジスティックモデルにより状態遷移が与えられるMPPに対して,証明可能な効率のよいRLアルゴリズムを確立する。
本稿では,提案アルゴリズムが既存の手法より一貫して優れていることを示す。
論文 参考訳(メタデータ) (2022-12-27T16:25:09Z) - LAMBADA: Backward Chaining for Automated Reasoning in Natural Language [11.096348678079574]
LAMBADAと呼ばれる逆チェインアルゴリズムは、推論を4つのサブモジュールに分解する。
LAMBADAは最先端のフォワード推論手法よりも精度が向上することを示す。
論文 参考訳(メタデータ) (2022-12-20T18:06:03Z) - On an Edge-Preserving Variational Model for Optical Flow Estimation [0.0]
光流量推定のためのエッジ保存型$L1$正規化手法を提案する。
提案手法は,最先端のHhornとSchunckに基づく変分法と比較して,平均角度誤差と終点誤差を最大化する。
論文 参考訳(メタデータ) (2022-07-21T04:46:16Z) - Constrained Training of Neural Networks via Theorem Proving [0.2578242050187029]
有限トレース上の線形時間論理の深い埋め込み(LTL$_f$)を定式化する。
次に、損失関数 $mathcalL$ を形式化し、その関数 $dmathcalL$ に微分可能であることを正式に証明する。
本研究では,動的運動のための既存のディープラーニングフレームワークのトレーニングに使用する場合,共通の運動仕様パターンに対する予測結果が得られたことを示す。
論文 参考訳(メタデータ) (2022-07-08T13:13:51Z) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。
命題の文字は任意の理論で解釈された一階述語式に置き換えられる。
Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文 参考訳(メタデータ) (2022-04-28T17:57:33Z) - Markov Decision Process modeled with Bandits for Sequential Decision
Making in Linear-flow [73.1896399783641]
会員/加入者の獲得と保持では、複数のページを連続してマーケティングコンテンツを推奨する必要がある。
遷移確率行列をモデル化するためにBandits を用いた MDP としてこの問題を定式化することを提案する。
提案したMDPのBanditsアルゴリズムは,$epsilon$-greedyと$epsilon$-greedy,$epsilon$,IndependentBandits,InteractionBanditsでQ-learningを上回っている。
論文 参考訳(メタデータ) (2021-07-01T03:54:36Z) - A Newton Frank-Wolfe Method for Constrained Self-Concordant Minimization [60.90222082871258]
本稿では,制約集合上の線形最小化オラクル(LMO)を用いて,制約付き自己調和最小化問題のクラスをカラフルに解く方法を示す。
L-smoothの場合、我々の手法のLMO呼び出し数はFrank-Wolfe法とほぼ同じであることを示す。
論文 参考訳(メタデータ) (2020-02-17T15:28:31Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。