Fugu-MT 論文翻訳(概要): Smart Induction for Isabelle/HOL (System Description)

論文の概要: Smart Induction for Isabelle/HOL (System Description)

arxiv url: http://arxiv.org/abs/2001.10834v1
Date: Mon, 27 Jan 2020 15:29:34 GMT
ステータス: 処理完了
システム内更新日: 2023-01-06 08:34:28.503033
Title: Smart Induction for Isabelle/HOL (System Description)
Title（参考訳）: Isabelle/HOLのためのスマート誘導(システム記述)
Authors: Yutaka Nagashima
Abstract要約: smart_inductは、検索に頼ることなく、インダクション戦術の有望な引数をリストアップする。評価の結果,Smart_inductは問題領域にまたがって貴重なレコメンデーションをもたらすことがわかった。
参考スコア（独自算出の注目度）: 6.85316573653194
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Proof assistants offer tactics to facilitate inductive proofs. However, it still requires human ingenuity to decide what arguments to pass to those induction tactics. To automate this process, we present smart_induct for Isabelle/HOL. Given an inductive problem in any problem domain, smart_induct lists promising arguments for the induct tactic without relying on a search. Our evaluation demonstrated smart_induct produces valuable recommendations across problem domains.
Abstract（参考訳）: 証明アシスタントは帰納的証明を促進する戦術を提供する。しかし、誘導戦術にどの引数を渡すかを決めるには、まだ人間の創造性が必要である。このプロセスを自動化するために,Isabelle/HOL の Smart_induct を提案する。あらゆる問題領域における帰納的問題として、smart_inductは検索に頼らずに帰納的戦術の有望な引数をリストアップする。評価の結果,Smart_inductは問題領域間で有用なレコメンデーションを提供することがわかった。

関連論文リスト

Inductive or Deductive? Rethinking the Fundamental Reasoning Abilities of LLMs [99.76347807139615]
推論には2つの典型型がある: 帰納的推論(deductive reasoning)と帰納的推論(inductive reasoning)。大規模言語モデル(LLM)の推論能力に関する広範な研究にもかかわらず、ほとんどの研究は帰納的推論と帰納的推論を厳密に区別することができなかった。 LLM推論では、帰納的または帰納的推論という、より大きな課題を引き起こします。
論文参考訳（メタデータ） (2024-07-31T18:47:11Z)
Phenomenal Yet Puzzling: Testing Inductive Reasoning Capabilities of Language Models with Hypothesis Refinement [92.61557711360652]
言語モデル(LM)は、しばしば帰納的推論に不足する。我々は,反復的仮説修正を通じて,LMの帰納的推論能力を体系的に研究する。本研究は, LMの誘導的推論過程と人間とのいくつかの相違点を明らかにし, 誘導的推論タスクにおけるLMの使用の可能性と限界に光を当てる。
論文参考訳（メタデータ） (2023-10-12T17:51:10Z)
Self-Polish: Enhance Reasoning in Large Language Models via Problem Refinement [50.62461749446111]
Self-Polish(SP)は、与えられた問題を徐々に洗練し、より理解しやすく解けるように誘導することによって、モデルの推論を促進する新しい方法である。 SPは、CoTのような答え/推論サイドの他のすべてのプロンプトメソッドであり、最先端の技術とのシームレスな統合を可能にし、さらなる改善を可能にします。
論文参考訳（メタデータ） (2023-05-23T19:58:30Z)
Enhancing Large Language Models Against Inductive Instructions with Dual-critique Prompting [55.15697111170836]
本稿では,大規模言語モデル(LLM)のテクスト誘導的指示に対する行動を明らかにするとともに,その真しさと有用性を高める。広範囲な人的・自動的な評価の結果,帰納的命令処理において LLM に共通する脆弱性が発見された。異なる帰納的スタイルがモデルに同じエラーを識別する能力に影響を及ぼし、基礎となる仮定の複雑さがモデルの性能にも影響を及ぼす。
論文参考訳（メタデータ） (2023-05-23T06:38:20Z)
User Guided Abductive Proof Generation for Answer Set Programming Queries (Extended Version) [0.0]
本稿では,与えられた Answer Set Programming (ASP) ルールセットに対して,クエリの可能な証明を生成する方法を提案する。ユーザが提供する事実のセット(おそらく空である)が与えられた場合、我々のメソッドはクエリーのentailmentに必要な追加の事実を推測する。また,クエリの正当性グラフに対応する有向エッジの集合を生成する手法を提案する。
論文参考訳（メタデータ） (2022-09-16T14:06:12Z)
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)
Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文参考訳（メタデータ） (2022-05-25T02:22:30Z)
Impossibility Results in AI: A Survey [3.198144010381572]
不合理性定理(英: impossibility theorem)は、特定の問題や問題の集合が主張に記述されているように解決できないことを示す定理である。我々はAIの領域に適用可能な不合理性定理を、推論、識別不能、誘導、トレードオフ、難解性の5つのカテゴリに分類した。我々は,ゆるやかな不合理性は,安全に対する100%の保証を否定する,と結論づける。
論文参考訳（メタデータ） (2021-09-01T16:52:13Z)
Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction [6.85316573653194]
SeLFiEは、Isabelle/HOLにおけるインダクタンス戦術の適用方法に関するユーザの知識を表すクエリ言語である。評価のために,SeLFiEを用いた自動誘導証明器を開発した。新しい証明器は,1.0秒タイムアウトのベースライン証明よりも1.4×103%向上し,スピードアップの中央値が4.48倍となった。
論文参考訳（メタデータ） (2020-10-19T09:05:09Z)
Faster Smarter Induction in Isabelle/HOL [6.85316573653194]
sem_indはインダクトメソッドに渡す引数を推奨する。定義量化器は、帰納的問題の構文構造だけでなく、ドメインに依存しないスタイルにおける関連する定数の定義も調べることができる。
論文参考訳（メタデータ） (2020-09-19T11:51:54Z)
Towards United Reasoning for Automatic Induction in Isabelle/HOL [6.85316573653194]
我々は、帰納的定理の証明をさらに自動化するための新しいアプローチである統一推論を提案する。成功の後、統一推論は、帰納的推論(deductive reasoning)、帰納的推論(inductive reasoning)、帰納的推論(inductive reasoning)の3つの流派のうち、最高のものとなる。
論文参考訳（メタデータ） (2020-05-25T08:30:05Z)

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