論文の概要: Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agent

• arxiv url: http://arxiv.org/abs/2407.14521v1
• Date: Fri, 5 Jul 2024 15:59:16 GMT
• ステータス: 処理完了
• システム内更新日: 2024-07-28 18:39:09.773748
• Title: Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agent
• Title（参考訳）: 自動関数式証明に向けて:ベンチマークデータセットとドメイン特有なインコンテキストエージェント
• Authors: Mahdi Buali, Robert Hoehndorf,
• Abstract要約: ATP(Automated Theorem Proving)はその複雑さと計算上の要求のため、課題に直面している。 近年, 大規模言語モデル (LLM) を用いてATPの作用選択を行っているが, これらの手法は資源集約性が高い。 この研究は、リーン内のCOPRAインコンテキスト学習フレームワークを強化するエージェントであるFEASを紹介します。
• 参考スコア（独自算出の注目度）: 1.006303657343407
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automated Theorem Proving (ATP) faces challenges due to its complexity and computational demands. Recent work has explored using Large Language Models (LLMs) for ATP action selection, but these methods can be resource-intensive. This study introduces FEAS, an agent that enhances the COPRA in-context learning framework within Lean. FEAS refines prompt generation, response parsing, and incorporates domain-specific heuristics for functional equations. It introduces FunEq, a curated dataset of functional equation problems with varying difficulty. FEAS outperforms baselines on FunEq, particularly with the integration of domain-specific heuristics. The results demonstrate FEAS's effectiveness in generating and formalizing high-level proof strategies into Lean proofs, showcasing the potential of tailored approaches for specific ATP challenges.
• Abstract（参考訳）: ATP(Automated Theorem Proving)はその複雑さと計算上の要求のため、課題に直面している。 近年, 大規模言語モデル (LLM) を用いてATPの作用選択を行っているが, これらの手法は資源集約性が高い。 この研究は、リーン内のCOPRAインコンテキスト学習フレームワークを強化するエージェントであるFEASを紹介します。 FEASはプロンプト生成、応答解析を洗練し、機能方程式にドメイン固有のヒューリスティックを組み込む。 FunEqは、様々な困難を伴う関数方程式問題のキュレートされたデータセットである。 FEASはFunEqのベースライン、特にドメイン固有のヒューリスティックを統合することでパフォーマンスを向上する。 その結果、FEASがハイレベルな証明戦略をリーンの証明に組み込んで、特定のATP課題に対する調整されたアプローチの可能性を示した。

関連論文リスト

• Entropy-Regularized Token-Level Policy Optimization for Language Agent Reinforcement [67.1393112206885]
  大規模言語モデル(LLM)は、対話的な意思決定タスクにおいてインテリジェントなエージェントとして期待されている。 本稿では,トークンレベルでのLLMの最適化に適したエントロピー拡張RL法である,エントロピー正規化トークンレベル最適化(ETPO)を導入する。 我々は,データサイエンスコード生成を多段階対話型タスクのシリーズとしてモデル化したシミュレーション環境におけるETPOの有効性を評価する。
  論文  参考訳（メタデータ） (2024-02-09T07:45:26Z)
• Functional Linear Non-Gaussian Acyclic Model for Causal Discovery [7.303542369216906]
  我々は、fMRIとEEGデータセットを含む脳効果接続タスクにおける因果関係を識別するフレームワークを開発する。 非ガウス確率ベクトルと無限次元ヒルベルト空間のランダム関数の間の因果関係の同定可能性の理論的保証を確立する。 実データでは、fMRIデータから得られる脳の接続パターンを分析することに重点を置いている。
  論文  参考訳（メタデータ） (2024-01-17T23:27:48Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
  論文  参考訳（メタデータ） (2023-10-16T08:42:39Z)
• Transport Equation based Physics Informed Neural Network to predict the Yield Strength of Architected Materials [0.0]
  PINNモデルは、提供されたデータセットの過度な適合を避ける能力を示す、例外的な一般化能力を示す。 この研究は、特定の実世界のアプリケーションに対してアクティベーション関数を選択しながら、性能と計算効率のバランスを打つことの重要性を強調している。
  論文  参考訳（メタデータ） (2023-07-29T12:42:03Z)
• On the Integration of Physics-Based Machine Learning with Hierarchical Bayesian Modeling Techniques [0.0]
  本稿では,ガウス過程(GP)モデルの平均関数にメカニクスに基づくモデルを組み込み,カーネルマシンによる潜在的な不一致を特徴付けることを提案する。 カーネル関数の定常性は、階層的ベイズ手法によって解決された長いデータセットの逐次処理において難しいハードルである。 数値および実験例を用いて, 構造力学逆問題に対する提案手法の可能性を示した。
  論文  参考訳（メタデータ） (2023-03-01T02:29:41Z)
• Offline Reinforcement Learning with Differentiable Function Approximation is Provably Efficient [65.08966446962845]
  歴史的データを用いて意思決定戦略を最適化することを目的としたオフライン強化学習は、現実の応用に広く適用されている。 微分関数クラス近似(DFA)を用いたオフライン強化学習の検討から一歩踏み出した。 最も重要なことは、悲観的な適合Q-ラーニングアルゴリズムを解析することにより、オフライン微分関数近似が有効であることを示すことである。
  論文  参考訳（メタデータ） (2022-10-03T07:59:42Z)
• Data-Driven Reachability analysis and Support set Estimation with Christoffel Functions [8.183446952097528]
  動的システムの前方到達可能な集合を推定するためのアルゴリズムを提案する。 生成された推定は、経験的逆クリストッフェル函数と呼ばれる関数の部分レベル集合である。 到達可能性解析に加えて、確率変数の支持を推定する一般的な問題にも同様のアプローチを適用することができる。
  論文  参考訳（メタデータ） (2021-12-18T20:25:34Z)
• Scalable Gaussian Processes for Data-Driven Design using Big Data with Categorical Factors [14.337297795182181]
  ガウス過程(GP)は、大きなデータセット、カテゴリ入力、および複数の応答を調節するのに困難である。 本稿では,変分推論によって得られた潜伏変数と関数を用いて,上記の課題を同時に解決するGPモデルを提案する。 本手法は三元系酸化物材料の機械学習と多スケール対応機構のトポロジー最適化に有用である。
  論文  参考訳（メタデータ） (2021-06-26T02:17:23Z)
• Tesseract: Tensorised Actors for Multi-Agent Reinforcement Learning [92.05556163518999]
  MARLは、コミュニケーションと可観測性に様々な制約を課すことによって、問題を悪化させる。 値ベースの手法では、最適な値関数を正確に表現することが課題となる。 政策勾配法では、批判者の訓練を困難にし、遅れる批判者の問題を悪化させる。 学習理論の観点からは、関連するアクション値関数を正確に表現することで、両方の問題に対処できることが示される。
  論文  参考訳（メタデータ） (2021-05-31T23:08:05Z)
• Removing Bias in Multi-modal Classifiers: Regularization by Maximizing Functional Entropies [88.0813215220342]
  いくつかのモダリティは、他のものよりも分類結果に容易に寄与することができる。 機能的エントロピーと機能的フィッシャー情報とを結合した対数ソボレフの不等式に基づく手法を開発した。 VQA-CPv2 と SocialIQ の2つの挑戦的マルチモーダルデータセットに対して,より均一にモダリティを活用しながら,最先端の結果を得る。
  論文  参考訳（メタデータ） (2020-10-21T07:40:33Z)
• Feature Quantization Improves GAN Training [126.02828112121874]
  識別器の特徴量子化(FQ)は、真と偽のデータの両方を共有離散空間に埋め込む。 本手法は,既存のGANモデルに容易に接続でき,訓練における計算オーバーヘッドがほとんどない。
  論文  参考訳（メタデータ） (2020-04-05T04:06:50Z)

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

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