論文の概要: Conjectures, Tests and Proofs: An Overview of Theory Exploration
- arxiv url: http://arxiv.org/abs/2109.03721v1
- Date: Tue, 7 Sep 2021 01:57:07 GMT
- ステータス: 処理完了
- システム内更新日: 2021-09-10 09:00:33.687885
- Title: Conjectures, Tests and Proofs: An Overview of Theory Exploration
- Title（参考訳）: 概念・テスト・証明:理論探索の概観
- Authors: Moa Johansson (Chalmers University of Technology), Nicholas Smallbone
(Chalmers University of Technology)
- Abstract要約: 我々はQuickSpecと呼ばれる理論探査システムの概要を概説する。
QuickSpecは、与えられた関数の集合に関する興味深い予想を自動的に発見することができる。
自動帰納定理証明のための補題の生成に成功している。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: A key component of mathematical reasoning is the ability to formulate
interesting conjectures about a problem domain at hand. In this paper, we give
a brief overview of a theory exploration system called QuickSpec, which is able
to automatically discover interesting conjectures about a given set of
functions. QuickSpec works by interleaving term generation with random testing
to form candidate conjectures. This is made tractable by starting from small
sizes and ensuring that only terms that are irreducible with respect to already
discovered conjectures are considered. QuickSpec has been successfully applied
to generate lemmas for automated inductive theorem proving as well as to
generate specifications of functional programs. We give an overview of typical
use-cases of QuickSpec, as well as demonstrating how to easily connect it to a
theorem prover of the user's choice.
- Abstract（参考訳）: 数学的推論の重要な要素は、問題の領域について興味深い予想を定式化する能力である。
本稿では,与えられた関数集合に関する興味深い予想を自動的に発見できるquickspecと呼ばれる理論探索システムの概要を示す。
QuickSpecは、候補予想を形成するためにランダムテストで項生成をインターリーブすることで機能する。
これは、小さいサイズから始まり、既に発見されている予想について既約である項のみが考慮されることで、扱いやすい。
quickspec は自動帰納的定理証明のための補題の生成や関数型プログラムの仕様の作成に成功している。
我々は、QuickSpecの典型的なユースケースの概要と、ユーザの選択の定理証明者に簡単に接続する方法を示す。
関連論文リスト
- Learning Formal Mathematics From Intrinsic Motivation [34.986025832497255]
ミニモ(Minimo)は、自分自身に問題を起こし、それを解決することを学ぶエージェント(理論実証)である。
制約付き復号法と型指向合成法を組み合わせて、言語モデルから有効な予想をサンプリングする。
我々のエージェントは、ハードだが証明可能な予想を生成することを目標としています。
論文 参考訳（メタデータ） (2024-06-30T13:34:54Z) - ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
人間はより広範に複雑な数学的結果を探求するために新しい定理を開発することができる。
現在の生成言語モデル(LM)は、定理の自動証明において著しく改善されている。
本稿では,エージェントが価値ある(あるいは新しい)定理を自動生成できるかどうかを評価する自動定理生成ベンチマークを提案する。
論文 参考訳（メタデータ） (2024-05-05T02:06:37Z) - Machine learning and information theory concepts towards an AI
Mathematician [77.63761356203105]
人工知能の現在の最先端技術は、特に言語習得の点で印象的だが、数学的推論の点ではあまり重要ではない。
このエッセイは、現在のディープラーニングが主にシステム1の能力で成功するという考えに基づいている。
興味深い数学的ステートメントを構成するものについて質問するために、情報理論的な姿勢を取る。
論文 参考訳（メタデータ） (2024-03-07T15:12:06Z) - Considerations on Approaches and Metrics in Automated Theorem
Generation/Finding in Geometry [0.0]
我々は、幾何定理(と性質)の自動発見のための異なるアプローチを提示し、議論する。
定理証明者が興味深い定理を生成できるかどうかを判断することは、決定論的でない課題である。
論文 参考訳（メタデータ） (2024-01-22T12:51:19Z) - Mathematical conjecture generation using machine intelligence [0.0]
f の型 f の厳密な不等式に焦点をあて、それらをベクトル空間に関連付ける。
我々は、この多様体の線型自己同型を研究することによって、この予想空間の構造的理解を発展させる。
幾何勾配勾配を用いた新しい予想を生成するアルゴリズムパイプラインを提案する。
論文 参考訳（メタデータ） (2023-06-12T17:58:38Z) - TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
GPT-4のこれらの問題を解決する能力は非並列であり、Program-of-Thoughts Promptingの精度は51%である。
TheoremQAは、350の定理をカバーする800の高品質な質問を含むドメインの専門家によってキュレートされる。
論文 参考訳（メタデータ） (2023-05-21T17:51:35Z) - Connes implies Tsirelson: a simple proof [91.3755431537592]
コンヌ埋め込み問題は同期的ツィレルソン予想を意味することを示す。
また、コンネスの代数 $mathcalRomega$ の異なる構成もコンネス埋め込み問題に現れる。
論文 参考訳（メタデータ） (2022-09-16T13:59:42Z) - Who Finds the Short Proof? An Exploration of variants of Boolos' Curious
Inference using Higher-order Automated Theorem Provers [62.997667081978825]
本稿では, 高階自動定理証明器を用いたブーロスの興味ある推論の変種探索について報告する。
驚いたことに、手動で手書き表記する必要があったのは1つの短い手書き表記のみであった。
短い証明を得るために必要な高次の補題はすべて、コンピュータによって自動的に発見される。
論文 参考訳（メタデータ） (2022-08-14T16:31:04Z) - Optimal Measurement Structures for Contextuality Applications [4.407033774951362]
Kochen-Specker (KS) の定理は量子力学の基礎となる基礎的な結果である。
最近、991$-gadgetsと呼ばれる特定の部分構造がKS証明の中に存在することが示されている。
これらのガジェットとそれらの一般化は、コンテキスト性アプリケーションに最適なツールボックスを提供する。
論文 参考訳（メタデータ） (2022-06-27T09:34:36Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。