Fugu-MT 論文翻訳(概要): What are Your Powers? -- Truth Set Algebras

論文の概要: What are Your Powers? -- Truth Set Algebras

arxiv url: http://arxiv.org/abs/2208.04422v1
Date: Mon, 8 Aug 2022 21:20:03 GMT
ステータス: 処理完了
システム内更新日: 2022-08-10 13:09:27.750185
Title: What are Your Powers? -- Truth Set Algebras
Title（参考訳）: パワーとは何か? --真理集合代数
Authors: Sophia Knight and Pavel Naumov
Abstract要約: 本稿では,不完全な情報設定における4種類の多段階戦略を表現するモダリティ間の相互作用について検討する。これは、未定義性を証明するための新しい「真実集合代数」技術を導入し、これはバイシミュレーションに基づく既存の手法と大きく異なる。
参考スコア（独自算出の注目度）: 29.24017380920295
License: http://creativecommons.org/licenses/by/4.0/
Abstract: The paper studies the interplay between modalities representing four different types of multistep strategies in the imperfect information setting. It introduces a new "truth set algebra'' technique for proving undefinability, which is significantly different from the existing techniques based on bisimulation. The newly proposed technique is used to prove the undefinability of each of the four modalities through a combination of the three others.
Abstract（参考訳）: 本稿では,不完全情報設定における4種類の多段階戦略を表現するモダリティ間の相互作用について検討する。これは、未定義性を証明するための新しい「真実集合代数」技術を導入し、バイシミュレーションに基づく既存の手法とは大きく異なる。新たに提案した手法は、4つのモードのそれぞれが他の3つの組み合わせによって定義不可能であることを証明するために用いられる。

関連論文リスト

How To Discover Short, Shorter, and the Shortest Proofs of Unsatisfiability: A Branch-and-Bound Approach for Resolution Proof Length Minimization [1.4796543791607086]
本稿では,最短解法を見つけるための分岐結合アルゴリズムを提案する。この表現はすべての置換対称性を破り、それによって最先端の対称性の破れを改善する。本実験により, SATコンペティション2002の事例では30～60%, 小型合成式では25～50%の短縮が可能であることが示唆された。
論文参考訳（メタデータ） (2024-11-12T17:31:35Z)
Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文参考訳（メタデータ） (2024-07-14T01:43:07Z)
Proving Theorems Recursively [80.42431358105482]
本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。また,POETRYが検出した最大証明長は10～26。
論文参考訳（メタデータ） (2024-05-23T10:35:08Z)
ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
人間はより広範に複雑な数学的結果を探求するために新しい定理を開発することができる。現在の生成言語モデル(LM)は、定理の自動証明において著しく改善されている。本稿では,エージェントが価値ある(あるいは新しい)定理を自動生成できるかどうかを評価する自動定理生成ベンチマークを提案する。
論文参考訳（メタデータ） (2024-05-05T02:06:37Z)
REFACTOR: Learning to Extract Theorems from Proofs [29.44286369265644]
我々は、REFACTORが、人間が証明を書くのに使用する定理の19.6%を抽出できることを示した。新たに抽出された定理により,既存のMetaMathデータベースが構築可能であることを示す。また、新理論データセットでトレーニングされた証明者が、より多くのテスト定理を証明し、最先端のベースラインを上回ることを実証する。
論文参考訳（メタデータ） (2024-02-26T21:21:30Z)
Verifying Quantum Phase Estimation (QPE) using Prove-It [0.0]
Prove-Itと呼ばれる汎用的な対話型定理証明アシスタントは、量子位相推定(QPE)アルゴリズムを検証するために使用された。 Prove-Itは、量子回路に関するステートメントを含む洗練された数学的ステートメントを表現する能力に特有である。
論文参考訳（メタデータ） (2023-04-05T01:21:00Z)
NaturalProver: Grounded Mathematical Proof Generation with Language Models [84.2064569475095]
自然数理言語における定理証明は、数学の進歩と教育において中心的な役割を果たす。本研究では,背景参照を条件づけて証明を生成する言語モデルであるNaturalProverを開発する。 NaturalProverは、短い(2-6ステップ)証明を必要とするいくつかの定理を証明でき、40%の時間で正しいと評価された次のステップの提案を提供することができる。
論文参考訳（メタデータ） (2022-05-25T17:01:18Z)
Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文参考訳（メタデータ） (2022-05-25T02:22:30Z)
Prove-It: A Proof Assistant for Organizing and Verifying General Mathematical Knowledge [0.0]
Prove-ItはPythonベースの汎用的対話型定理証明アシスタントである。 Prove-ItはフレキシブルなJupyterノートブックベースのユーザーインターフェイスを使って、対話や証明の手順を文書化している。現在の開発と今後の研究には、量子回路操作と量子アルゴリズム検証への有望な応用が含まれている。
論文参考訳（メタデータ） (2020-12-20T18:15:12Z)
Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文参考訳（メタデータ） (2020-02-17T16:06:02Z)

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