論文の概要: When Agda met Vampire

• arxiv url: http://arxiv.org/abs/2602.18844v1
• Date: Sat, 21 Feb 2026 14:19:56 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-24 17:42:02.34913
• Title: When Agda met Vampire
• Title（参考訳）: アグダがヴァンパイアに会ったとき
• Authors: Artjoms Šinkarovs, Michael Rawson,
• Abstract要約: 本研究の目的は,証明アシスタントと自動定理証明器(ATP)を簡単な方法で統合することである。 ほとんどのATPは古典的な一階述語論理で作用するが、これらの証明アシスタントは構成的依存型理論に基づいている。 我々は、ATPヴァンパイアに対するAgda証明義務のプロトタイプシステムを作成し、その結果得られた古典的証明をAgdaが型チェックできる構成的証明項に変換する。
• 参考スコア（独自算出の注目度）: 3.373200015661363
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Dependently-typed proof assistants furnish expressive foundations for mechanised mathematics and verified software. However, automation for these systems has been either modest in scope or complex in implementation. We aim to improve the situation by integrating proof assistants with automated theorem provers (ATPs) in a simple way, while preserving the correctness guarantees of the former. A central difficulty arises from the fact that most ATPs operate in classical first-order logic, whereas these proof assistants are grounded in constructive dependent type theory. We identify an expressive fragment of both languages -- essentially equational Horn -- that admits sound, straightforward translations in both directions. The approach produces a prototype system for Agda forwarding proof obligations to the ATP Vampire, then transforming the resulting classical proof into a constructive proof term that Agda can type-check. The prototype automatically derives proofs concerning the properties of a complex field equipped with roots of unity, which took professional Agda developers two full days to complete. The required engineering effort is modest, and we anticipate that the methodology will extend readily to other ATPs and proof assistants.
• Abstract（参考訳）: 依存型証明アシスタントは、機械化された数学と検証されたソフトウェアのための表現力のある基礎を提供する。 しかし、これらのシステムの自動化はスコープが適度か実装が複雑である。 本研究の目的は, 証明アシスタントと自動定理証明器(ATP)を簡単な方法で統合し, 前者の正当性を保証することである。 ほとんどのATPが古典的な一階述語論理で作用するという事実から中心的な困難が生じるが、これらの証明アシスタントは構成的依存型理論に基づいている。 両言語の表現的な断片 - 基本的には方程式のホーン - を識別し、両方向の音で素直な翻訳を許容する。 このアプローチは、ATPヴァンパイアに証明義務を転送するAgdaのプロトタイプシステムを生成し、その結果の古典的証明をAgdaが型チェックできる構成的証明項に変換する。 プロトタイプは、ユニティの根を備えた複素体の性質に関する証明を自動で導き、プロのAgda開発者が完成までに2日を要した。 必要なエンジニアリング努力は控えめであり,他のATPや証明アシスタントにも容易に拡張できると期待している。

関連論文リスト

• Gödel's Poetry [0.0]
  本稿では,Lean4の証明生成に特殊言語モデルを用いるコンピュータ定理証明の新しいアプローチを提案する。 分解せずにMiniF2Fの90.4%のパスレートを達成する。 重要な技術的貢献は、抽象構文木(AST)解析機能を備えたKimina Lean Serverの拡張にあります。
  論文  参考訳（メタデータ） (2025-12-16T10:00:01Z)
• Agentic Program Verification [14.684859166069012]
  本稿では,プログラム検証を行うための最初の大規模言語モデルエージェントであるAutoRocqを提案する。 LLMの広範な訓練を実証例に頼っている過去の研究とは異なり、我々のエージェントはオンザフライで学習し、反復的な改善ループを通じて証明を改善する。 このようにして、我々の証明構成は証明エージェントと定理証明器との間の自律的な協調を含む。
  論文  参考訳（メタデータ） (2025-11-21T15:51:48Z)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。 本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。 また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
  論文  参考訳（メタデータ） (2023-10-16T08:42:39Z)
• Baldur: Whole-Proof Generation and Repair with Large Language Models [8.100054850290507]
  我々は、自然言語のテキストとコードに基づいて訓練され、証明について微調整された大きな言語モデルを使用して、一度に定理のすべての証明を生成する。 我々は、この証明生成モデルと微調整の補修モデルを組み合わせて、生成した証明を修復し、さらに証明力を増強する。 本手法をプロトタイプであるBaldurで評価し、6,336 Isabelle/HOL定理とその証明のベンチマークで評価する。
  論文  参考訳（メタデータ） (2023-03-08T22:00:15Z)
• Neural Unification for Logic Reasoning over Natural Language [0.28675177318965034]
  自動定理証明(Automated Theorem Proving)は、いくつかの予想(クエリ)が一連の公理(事実と規則)の論理的な結果であることを示すことができるコンピュータプログラムの開発を扱う。 近年のアプローチでは、自然言語(英語)で表される公理の予想を導出するトランスフォーマーに基づくアーキテクチャが提案されている。 本研究は, 一般化の項における最先端結果を実現するニューラルユニファイザという, 新たなアーキテクチャを提案する。
  論文  参考訳（メタデータ） (2021-09-17T10:48:39Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)

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

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