論文の概要: Who Finds the Short Proof? An Exploration of variants of Boolos' Curious
Inference using Higher-order Automated Theorem Provers
- arxiv url: http://arxiv.org/abs/2208.06879v1
- Date: Sun, 14 Aug 2022 16:31:04 GMT
- ステータス: 処理完了
- システム内更新日: 2022-08-16 14:50:21.827955
- Title: Who Finds the Short Proof? An Exploration of variants of Boolos' Curious
Inference using Higher-order Automated Theorem Provers
- Title（参考訳）: 短い証明は誰か?
高次自動定理証明器を用いたブーロスの奇数推論の変種探索
- Authors: Christoph Benzm\"uller, David Fuenmayor, Alexander Steen, Geoff
Sutcliffe
- Abstract要約: 本稿では, 高階自動定理証明器を用いたブーロスの興味ある推論の変種探索について報告する。
驚いたことに、手動で手書き表記する必要があったのは1つの短い手書き表記のみであった。
短い証明を得るために必要な高次の補題はすべて、コンピュータによって自動的に発見される。
- 参考スコア（独自算出の注目度）: 62.997667081978825
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We report on an exploration of variants of Boolos' curious inference using
higher-order automated theorem provers (ATPs). Surprisingly, only a single
shorthand notation still had to be provided by hand. All higher-order lemmas
required for obtaining short proof are automatically discovered by the
computer. Given the observations and suggestions in this paper, full proof
automation of Boolos' example on the speedup of proof lengths, and related
examples, now seems to be within reach for higher-order ATPs.
- Abstract（参考訳）: 本稿では,高階自動定理証明器(ATPs)を用いたブーロスの興味深い推論の変種探索について報告する。
驚いたことに、手書きの表記は1つしかなかった。
短い証明を得るのに必要な全ての高階の補題はコンピュータによって自動的に発見される。
本論文の観察と提案から,ブーロスの証明長の高速化に関する実例の完全な証明自動化および関連する例は,現在,高次ATPの到達範囲内にあると考えられる。
関連論文リスト
- 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) - miniCodeProps: a Minimal Benchmark for Proving Code Properties [22.548472305010005]
私たちはLeanの証明アシスタントで201のプログラム仕様のベンチマークであるminiCodePropsを紹介します。
その単純さにもかかわらず、MiniCodePropsは現在のLLMベースのプローバーを壊すのに十分である。
論文 参考訳（メタデータ） (2024-06-16T21:11:23Z) - Proving Theorems Recursively [80.42431358105482]
本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。
従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。
また,POETRYが検出した最大証明長は10～26。
論文 参考訳（メタデータ） (2024-05-23T10:35:08Z) - Baldur: Whole-Proof Generation and Repair with Large Language Models [8.100054850290507]
我々は、自然言語のテキストとコードに基づいて訓練され、証明について微調整された大きな言語モデルを使用して、一度に定理のすべての証明を生成する。
我々は、この証明生成モデルと微調整の補修モデルを組み合わせて、生成した証明を修復し、さらに証明力を増強する。
本手法をプロトタイプであるBaldurで評価し、6,336 Isabelle/HOL定理とその証明のベンチマークで評価する。
論文 参考訳（メタデータ） (2023-03-08T22:00:15Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳（メタデータ） (2022-05-25T02:22:30Z) - Conjectures, Tests and Proofs: An Overview of Theory Exploration [0.0]
我々はQuickSpecと呼ばれる理論探査システムの概要を概説する。
QuickSpecは、与えられた関数の集合に関する興味深い予想を自動的に発見することができる。
自動帰納定理証明のための補題の生成に成功している。
論文 参考訳（メタデータ） (2021-09-07T01:57:07Z) - multiPRover: Generating Multiple Proofs for Improved Interpretability in
Rule Reasoning [73.09791959325204]
我々は、自然言語の事実と規則の形で明示的な知識を推論することを目的としている言語形式推論の一種に焦点を当てる。
PRoverという名前の最近の研究は、質問に答え、答えを説明する証明グラフを生成することによって、そのような推論を行う。
本研究では,自然言語規則ベースの推論のために複数の証明グラフを生成するという,新たな課題に対処する。
論文 参考訳（メタデータ） (2021-06-02T17:58:35Z) - Superposition for Lambda-Free Higher-Order Logic [62.997667081978825]
本稿では,意図的および拡張的クラス数$lambda$-free高階論理に対して,難解な完全重ね合わせ計算を導入する。
計算は完全単調でなくてもよい項順でパラメタ化され、$lambda$フリーの高次語彙パスとKnuth-Bendixの順序を使うことができる。
論文 参考訳（メタデータ） (2020-05-05T12:10:21Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳（メタデータ） (2020-02-17T16:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。