Fugu-MT 論文翻訳(概要): Truth Set Algebra: A New Way to Prove Undefinability

論文の概要: Truth Set Algebra: A New Way to Prove Undefinability

arxiv url: http://arxiv.org/abs/2208.04422v2
Date: Sat, 1 Jul 2023 20:15:25 GMT
ステータス: 処理完了
システム内更新日: 2023-07-04 15:59:51.277474
Title: Truth Set Algebra: A New Way to Prove Undefinability
Title（参考訳）: 真理集合代数:不定義性を証明する新しい方法
Authors: Sophia Knight, Pavel Naumov, Qi Shi and Vigasan Suntharraj
Abstract要約: 本稿では,論理的連結性の不定義性を相互に証明するための新しい手法を提案する。得られた結果のいくつかは、既存の定理の新たな証明であり、他のものは、この研究の原点である。
参考スコア（独自算出の注目度）: 23.575092210091977
License: http://creativecommons.org/licenses/by/4.0/
Abstract: The article proposes a new technique for proving the undefinability of logical connectives through each other and illustrates the technique with several examples. Some of the obtained results are new proofs of the existing theorems, others are original to this work.
Abstract（参考訳）: 本稿では,論理接続の非定義性を証明する新しい手法を提案し,その手法をいくつかの例で示す。得られた結果のいくつかは既存の定理の新しい証明であり、その他はこの研究の原点である。

関連論文リスト

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)

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