Fugu-MT 論文翻訳(概要): Abduction Prover in Isabelle/HOL

論文の概要: Abduction Prover in Isabelle/HOL

arxiv url: http://arxiv.org/abs/2606.04877v1
Date: Wed, 03 Jun 2026 13:41:08 GMT
ステータス: 翻訳完了
システム内更新日: 2026-06-04 20:44:18.784732
Title: Abduction Prover in Isabelle/HOL
Title（参考訳）: Isabelle/HOLにおけるアブダクションプローブ
Authors: Yutaka Nagashima, Daniel Sebastian Goc,
Abstract要約: 本稿では,Isabelle/HOLのAbduction Proverを紹介する。挑戦的な証明目標を与えられたAbduction Proverは、帰納的推論を用いて有用な予想を特定することによって、目標の証明スクリプトを構築する。
参考スコア（独自算出の注目度）: 1.5469452301122173
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Proof assistants based on expressive logics suffer limited automation for proof search, raising the cost of formal verification based on proof assistants. We address this problem by introducing the Abduction Prover for Isabelle/HOL. Given a challenging proof goal, the Abduction Prover constructs a proof script for the goal by identifying useful conjectures using abductive reasoning.
Abstract（参考訳）: 表現論理に基づく証明アシスタントは、証明検索のための限定的な自動化に悩まされ、証明アシスタントに基づく形式的検証のコストが上昇する。我々はIsabelle/HOLのアブダクション・プロバーを導入することでこの問題に対処する。挑戦的な証明目標を与えられたAbduction Proverは、帰納的推論を用いて有用な予想を特定することによって、目標の証明スクリプトを構築する。

関連論文リスト

ExVerus: Verus Proof Repair via Counterexample Reasoning [8.819482630789217]
大規模言語モデル(LLM)のための逆例誘導フレームワークであるEXVERUSを提案する。証明が失敗すると、EXVERUSは反例を自動生成して検証し、LSMを誘導して誘導不変量に一般化し、これらの障害を阻止する。評価の結果,EXVERUSは最先端のプロンプトベースのVerus証明生成器よりも証明精度,堅牢性,トークン効率を著しく向上することがわかった。
論文参考訳（メタデータ） (2026-03-26T18:14:34Z)
Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
現代言語モデル(LM)は、強い推論能力を示すが、標準的な評価は、人間のような推論の重要な側面である効率性を見越しながら、正確性を強調する。本稿では、論理プログラミングのレンズを用いて、LM推論効率を評価するためのフレームワークを提案する。
論文参考訳（メタデータ） (2025-10-29T15:30:31Z)
Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
論文参考訳（メタデータ） (2025-06-05T03:16:08Z)
Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文参考訳（メタデータ） (2024-07-14T01:43:07Z)
A Closer Look at the Self-Verification Abilities of Large Language Models in Logical Reasoning [73.77088902676306]
論理的推論の文脈において,大規模言語モデル(LLM)の自己検証能力について詳しく検討する。本研究の主目的は,既存のLCMが誤った推論手順を正確に識別するのに苦労し,自己検証法の有効性を保証できないことにある。
論文参考訳（メタデータ） (2023-11-14T07:13:10Z)
Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文参考訳（メタデータ） (2022-05-25T02:22:30Z)
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)
Towards United Reasoning for Automatic Induction in Isabelle/HOL [6.85316573653194]
我々は、帰納的定理の証明をさらに自動化するための新しいアプローチである統一推論を提案する。成功の後、統一推論は、帰納的推論(deductive reasoning)、帰納的推論(inductive reasoning)、帰納的推論(inductive reasoning)の3つの流派のうち、最高のものとなる。
論文参考訳（メタデータ） (2020-05-25T08:30:05Z)
Smart Induction for Isabelle/HOL (System Description) [6.85316573653194]
smart_inductは、検索に頼ることなく、インダクション戦術の有望な引数をリストアップする。評価の結果,Smart_inductは問題領域にまたがって貴重なレコメンデーションをもたらすことがわかった。
論文参考訳（メタデータ） (2020-01-27T15:29:34Z)

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