Fugu-MT 論文翻訳(概要): Agent-Based Proof Design via Lemma Flow Diagram

論文の概要: 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を,数理教育で普及している「フロー証明」の代替案と考える。いくつか例を挙げる。

関連論文リスト

FLARE: Faithful Logic-Aided Reasoning and Exploration [50.9814063216852]
タスク分解を用いて問題空間をトラバースする新しい手法を提案する。我々はLarge Language Modelsを使ってソリューションを計画し、クエリを事実に軟式化し、論理プログラミングコードを使って述語する。提案手法は,生成したコードに対する推論プロセスの忠実度を計算し,外部の解法に頼らずにマルチホップ探索のステップを解析する。
論文参考訳（メタデータ） (2024-10-14T19:39:11Z)
Towards Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
大規模な言語モデルでリーン推論を実行するためのフレームワークであるLean Copilotを紹介します。証明手順を提案し、中間的な証明目標を完了し、関連する前提を選択するためのツールを構築します。実験により, 提案手法の有効性を実証し, 提案手法の有効性を検証した。
論文参考訳（メタデータ） (2024-04-18T22:54:08Z)
Optimal Flow Matching: Learning Straight Trajectories in Just One Step [89.37027530300617]
我々は,新しいtextbf Optimal Flow Matching (OFM) アプローチを開発し,理論的に正当化する。これは2次輸送のための直列のOT変位をFMの1ステップで回復することを可能にする。提案手法の主な考え方は,凸関数によってパラメータ化されるFMのベクトル場の利用である。
論文参考訳（メタデータ） (2024-03-19T19:44:54Z)
Learning Distributions on Manifolds with Free-Form Flows [7.773439780305304]
本研究では,多様体上のデータ生成モデルであるManifold Free-Form Flows (M-FFF)を提案する。 M-FFF は、既知の射影を持つ任意の多様体に直接適応する。従来のシングルステップメソッドと一貫して一致したり、性能が良くなったりします。
論文参考訳（メタデータ） (2023-12-15T14:58:34Z)
Large Language Model Programs [74.31873455763275]
近年,大規模な事前学習型言語モデル (LLM) は,いくつかの例から指示に従うことや,新しいタスクを実行する能力を示している。本稿では,この推論の行を拡張し,アルゴリズムやプログラムに組み込んでLLMの機能をさらに拡張する手法を提案する。我々は、よりアルゴリズム的なアプローチにより、微調整をせずに、思考ベースラインの連鎖よりも6.4%改善する。
論文参考訳（メタデータ） (2023-05-09T11:55:36Z)
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)
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)

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