Fugu-MT 論文翻訳(概要): Hammering with Vampire in Lean

論文の概要: Hammering with Vampire in Lean

arxiv url: http://arxiv.org/abs/2610.40310v1
Date: Thu, 29 Oct 2026 15:49:40 GMT
ステータス: 翻訳完了
システム内更新日: 2026-11-01 01:32:10.108605
Title: Hammering with Vampire in Lean
Title（参考訳）: リーンにおける吸血鬼とのハマー
Abstract要約: ヴァンパイア・ハマー(Vampire-Hammer)は、リーンのインタラクティブな定理証明のハンマーである。ヴァンパイアの自動定理証明を使って目標を放ち、Leanカーネルがチェックした証明を再構築する。
参考スコア（独自算出の注目度）: 1.4395184780210915
License: http://creativecommons.org/licenses/by/4.0/
Abstract: We present Vampire-Hammer, a hammer for the Lean interactive theorem prover that discharges goals using the Vampire automated theorem prover and reconstructs proofs checked by the Lean kernel. Vampire-Hammer uses the Lean-auto framework to process goals and premises before dispatching them to Vampire for proof search. Doing so, we rely on standard TPTP problem formats and annotated TSTP proofs that support proof reconstruction. With a 10-second budget on 196,083 eligible Mathlib theorems, Vampire-Hammer solves 21,158 problems not solved by other evaluated tools within the same budget.
Abstract（参考訳）: Vampire-Hammerは、Leanカーネルがチェックした証明を再構築し、Vampire自動定理証明器を使用して目標を出力する対話型定理証明器のハンマーである。 Vampire-HammerはLean-autoフレームワークを使って目標と前提を処理する。そのため、標準的なTPTP問題フォーマットと、証明再構成をサポートする注釈付きTSTP証明に依存している。 196,083個のMathlib定理に対する10秒の予算で、ヴァンパイア・ハマーは、同じ予算内で他の評価ツールによって解決されていない21,158の問題を解決した。

関連論文リスト

LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
信頼性の高い研究レベルのLean AutoformalizationのためのマルチエージェントハーネスであるLeanMarathonを紹介します。 4つのコントラクトスコープエージェントがこの青写真を構築し、監査し、証明し、修復する。我々は4つのErds問題にまたがる最近の2つの研究論文でLeanMarathonを評価した。
論文参考訳（メタデータ） (2026-06-03T20:09:39Z)
LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
論文参考訳（メタデータ） (2026-06-02T08:16:42Z)
Premise Selection for a Lean Hammer [17.976801288981395]
ハマーは、退屈な推論ステップを自動化するために外部の自動定理プローバーとインターフェースするツールである。 LeanHammerは、リーンの最初のエンドツーエンドのドメイン・ジェネラル・ハンマーです。我々の前提セレクタは、LeanHammerが既存の前提セレクタと比較して21%多くの目標を解決できることを示している。
論文参考訳（メタデータ） (2025-06-09T06:50:59Z)
APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
本稿では,自動定理証明のためのモデルに依存しないエージェントフレームワークであるAPOLLO (Automated PrOof repair viaLLM and Lean cOllaboration)を提案する。エージェントのセットは、証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動化されたソルバを利用し、残りの目標に対してLLMを呼び出す。この結果から,LLM出力を目標としたコンパイラ誘導型修復は,効率と正確性の両方において劇的に向上することが示された。
論文参考訳（メタデータ） (2025-05-09T03:38:31Z)
Proof Automation with Large Language Models [6.587933406842906]
大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
論文参考訳（メタデータ） (2024-09-22T00:19:27Z)
Proving Theorems Recursively [80.42431358105482]
本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。また,POETRYが検出した最大証明長は10～26。
論文参考訳（メタデータ） (2024-05-23T10:35:08Z)
Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
リーンでLLM推論を実行するためのフレームワークであるLean Copilotを紹介します。証明のステップを提案し、証明の目標を完了し、関連する前提を選択するツールを構築します。人間を助ける場合、Lean Copilotは平均3.86で手動で入力された証明ステップを2.08ステップしか必要としない。定理証明プロセスを自動化する場合、Lean Copilotの74.2%の証明ステップは平均85%がエソップ(40.1%)より優れている。
論文参考訳（メタデータ） (2024-04-18T22:54:08Z)
Vampire With a Brain Is a Good ITP Hammer [0.0]
我々は,効率のよい神経誘導による飽和手順の強化により,完全なMizarライブラリ上でのハンティングにおけるヴァンパイアの性能を向上させる。節の論理的内容を考慮した従来のニューラルメソッドと比較して、これはニューラルガイダンスの大きなリアルタイム高速化につながる。得られたシステムは、優れた学習能力を示し、Mizarライブラリ上で最先端のパフォーマンスを達成する。
論文参考訳（メタデータ） (2021-02-06T07:24:53Z)

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