論文の概要: Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction

• arxiv url: http://arxiv.org/abs/2010.10296v2
• Date: Fri, 20 May 2022 19:54:42 GMT
• ステータス: 処理完了
• システム内更新日: 2022-10-05 22:59:33.576068
• Title: Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
• Title（参考訳）: 導出による証明のための意味推論を実現する定義量化器
• Authors: Yutaka Nagashima
• Abstract要約: SeLFiEは、Isabelle/HOLにおけるインダクタンス戦術の適用方法に関するユーザの知識を表すクエリ言語である。 評価のために,SeLFiEを用いた自動誘導証明器を開発した。 新しい証明器は,1.0秒タイムアウトのベースライン証明よりも1.4×103%向上し,スピードアップの中央値が4.48倍となった。
• 参考スコア（独自算出の注目度）: 6.85316573653194
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Proof assistants offer tactics to apply proof by induction, but these tactics rely on inputs given by human engineers. To automate this laborious process, we developed SeLFiE, a boolean query language to represent experienced users' knowledge on how to apply the induct tactic in Isabelle/HOL: when we apply an induction heuristic written in SeLFiE to an inductive problem and arguments to the induct tactic, the SeLFiE interpreter judges whether the arguments are plausible for that problem according to the heuristic by examining both the syntactic structure of the problem and definitions of the relevant constants. To examine the intricate interaction between syntactic analysis and analysis of constant definitions, we introduce definitional quantifiers. For evaluation we build an automatic induction prover using SeLFiE. Our evaluation based on 347 inductive problems shows that our new prover achieves 1.4 x 10^3% improvement over the corresponding baseline prover for 1.0 second of timeout and the median value of speedup is 4.48x.
• Abstract（参考訳）: 証明アシスタントは、誘導によって証明を適用する戦術を提供するが、これらの戦術は、人間のエンジニアが与える入力に依存する。 そこで本研究では,Isabelle/HOLにおけるインダクタンス・戦術の適用方法に関する経験者の知識を表現し,インダクタンス・戦術にSeLFiEで記述した帰納的ヒューリスティックを適用し,インダクタンス・戦術に引数を適用した場合,その問題に対して議論が妥当かどうかを,そのヒューリスティックに従って判断し,関連する定数の構文構造と定義の両方を検証した。 構文解析と定数定義の分析の複雑な相互作用を調べるために,定義量化器を導入する。 評価のために,SeLFiEを用いた自動誘導証明器を開発した。 347の帰納的問題に基づく評価の結果,1.0秒のタイムアウトのベースライン証明よりも1.4×10^3%向上し,スピードアップの中央値が4.48倍となった。

関連論文リスト

• Clarify When Necessary: Resolving Ambiguity Through Interaction with LMs [58.620269228776294]
  そこで本稿では,ユーザに対して,あいまいさを解消するためのタスク非依存のフレームワークを提案する。 我々は3つのNLPアプリケーション(質問応答、機械翻訳、自然言語推論)にまたがるシステムを評価する。 インテントシムは堅牢であり、幅広いNLPタスクやLMの改善を実証している。
  論文  参考訳（メタデータ） (2023-11-16T00:18:50Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。 本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。 我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
  論文  参考訳（メタデータ） (2023-10-23T17:58:40Z)
• Phenomenal Yet Puzzling: Testing Inductive Reasoning Capabilities of Language Models with Hypothesis Refinement [92.61557711360652]
  言語モデル(LM)は、しばしば帰納的推論に不足する。 我々は,反復的仮説修正を通じて,LMの帰納的推論能力を体系的に研究する。 本研究は, LMの誘導的推論過程と人間とのいくつかの相違点を明らかにし, 誘導的推論タスクにおけるLMの使用の可能性と限界に光を当てる。
  論文  参考訳（メタデータ） (2023-10-12T17:51:10Z)
• Leveraging Affirmative Interpretations from Negation Improves Natural Language Understanding [10.440501875161003]
  否定は多くの自然言語理解タスクにおいて課題となる。 3つの自然言語理解タスクに対して,このようなメリットモデルを行うことが示される。 我々は,否定文を付与したプラグアンドプレイ型ニューラルジェネレータを構築し,肯定的な解釈を生成する。
  論文  参考訳（メタデータ） (2022-10-26T05:22:27Z)
• Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
  本稿では, 忠実度スルー・カウンタファクトの方法論について紹介する。 これは、説明に表される論理述語に基づいて、反実仮説を生成する。 そして、そのモデルが表現された論理と反ファクトの予測が一致しているかどうかを評価する。
  論文  参考訳（メタデータ） (2022-05-25T03:40:59Z)
• Maieutic Prompting: Logically Consistent Reasoning with Recursive Explanations [71.2950434944196]
  ノイズや一貫性のない言語モデルでさえも問題に対する正しい答えを推測するMaieutic Promptingを開発する。 Maieutic Promptingは最先端のプロンプト法よりも最大20%精度が高い。
  論文  参考訳（メタデータ） (2022-05-24T06:36:42Z)
• Probing as Quantifying the Inductive Bias of Pre-trained Representations [99.93552997506438]
  本稿では,特定のタスクに対する表現の帰納的バイアスを評価することを目的とした,探索のための新しいフレームワークを提案する。 トークン、アーク、文レベルの一連のタスクに我々のフレームワークを適用します。
  論文  参考訳（メタデータ） (2021-10-15T22:01:16Z)
• The Language Model Understood the Prompt was Ambiguous: Probing Syntactic Uncertainty Through Generation [23.711953448400514]
  このような分析に対して,ニューラルネットワークモデル(LM)がどの程度不確実性を示すかを調べる。 LMは複数の解析を同時に追跡できることがわかった。 曖昧な手がかりに対する応答として、LMは正しい解釈を選択することが多いが、時々エラーは改善の潜在的な領域を示す。
  論文  参考訳（メタデータ） (2021-09-16T10:27:05Z)
• Faster Smarter Induction in Isabelle/HOL [6.85316573653194]
  sem_indはインダクトメソッドに渡す引数を推奨する。 定義量化器は、帰納的問題の構文構造だけでなく、ドメインに依存しないスタイルにおける関連する定数の定義も調べることができる。
  論文  参考訳（メタデータ） (2020-09-19T11:51:54Z)

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

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