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

関連論文リスト

Categorical Schrödinger Bridge Matching [58.760054965084656]
Schr"odinger Bridge (SB)は、未ペアドメイン翻訳のような生成モデリングタスクを解決するための強力なフレームワークである。我々は、最近導入されたイテレーティブマルコフフィッティング(IMF)法を用いて、離散空間におけるSBを解くための理論的かつアルゴリズム的な基礎を提供する。これにより、CSBM(Categorical Schr"odinger Bridge Matching)と呼ばれるSBの実用的な計算アルゴリズムを開発することができる。
論文参考訳（メタデータ） (2025-02-03T14:55:28Z)
Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
本稿では,より優れたサンプル効率を有する定理証明手法であるProofAugを提案する。本手法は,オープンソースのDeepseek-math-7bベースモデルとIsabelle証明アシスタントを用いて,miniF2F-testベンチマークで検証した。
論文参考訳（メタデータ） (2025-01-30T12:37:06Z)
FLARE: Faithful Logic-Aided Reasoning and Exploration [50.9814063216852]
タスク分解を用いて問題空間をトラバースする新しい手法を提案する。我々はLarge Language Modelsを使ってソリューションを計画し、クエリを事実に軟式化し、論理プログラミングコードを使って述語する。提案手法は,生成したコードに対する推論プロセスの忠実度を計算し,外部の解法に頼らずにマルチホップ探索のステップを解析する。
論文参考訳（メタデータ） (2024-10-14T19:39:11Z)
Logicbreaks: A Framework for Understanding Subversion of Rule-based Inference [20.057611113206324]
我々は命題Hhorn論理の推論としてルール追従を定式化する。我々は、小さなトランスフォーマーはそのようなルールを忠実に守ることができるが、悪意のあるプロンプトは、データから学んだ理論的構成とモデルの両方を誤解させる可能性があることを証明している。
論文参考訳（メタデータ） (2024-06-21T19:18:16Z)
Towards Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
大規模な言語モデルでリーン推論を実行するためのフレームワークであるLean Copilotを紹介します。証明手順を提案し、中間的な証明目標を完了し、関連する前提を選択するためのツールを構築します。実験により, 提案手法の有効性を実証し, 提案手法の有効性を検証した。
論文参考訳（メタデータ） (2024-04-18T22:54:08Z)
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)
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)
A Newton Frank-Wolfe Method for Constrained Self-Concordant Minimization [60.90222082871258]
本稿では,制約集合上の線形最小化オラクル(LMO)を用いて,制約付き自己調和最小化問題のクラスをカラフルに解く方法を示す。 L-smoothの場合、我々の手法のLMO呼び出し数はFrank-Wolfe法とほぼ同じであることを示す。
論文参考訳（メタデータ） (2020-02-17T15:28:31Z)

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