論文の概要: A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants

• arxiv url: http://arxiv.org/abs/2508.18587v1
• Date: Tue, 26 Aug 2025 01:39:50 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-08-27 17:42:38.634193
• Title: A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
• Title（参考訳）: 証明支援による検証におけるLLMの有効性に関する事例研究
• Authors: Barış Bayazıt, Yao Li, Xujie Si,
• Abstract要約: 我々は、hs-to-coqツールとVerdiの2つの成熟したRocqプロジェクトに基づくケーススタディを実行する。 定量分析と定性解析の両方を用いて, LLM の有効性を評価した。
• 参考スコア（独自算出の注目度）: 9.022905966514717
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models (LLMs) can potentially help with verification using proof assistants by automating proofs. However, it is unclear how effective LLMs are in this task. In this paper, we perform a case study based on two mature Rocq projects: the hs-to-coq tool and Verdi. We evaluate the effectiveness of LLMs in generating proofs by both quantitative and qualitative analysis. Our study finds that: (1) external dependencies and context in the same source file can significantly help proof generation; (2) LLMs perform great on small proofs but can also generate large proofs; (3) LLMs perform differently on different verification projects; and (4) LLMs can generate concise and smart proofs, apply classical techniques to new definitions, but can also make odd mistakes.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、証明の自動化によって証明アシスタントを用いた検証に役立つ可能性がある。 しかし,この作業においてLLMがどの程度有効であるかは明らかでない。 本稿では、Hs-to-coqツールとVerdiの2つの成熟したRocqプロジェクトに基づくケーススタディを実行する。 定量分析と定性解析の両方を用いて, LLM の有効性を評価した。 本研究は,(1)同一ソースファイル内の外部依存関係とコンテキストが証明生成に有効であること,(2) LLMは小さな証明において優れた性能を示すが,大きな証明も生成可能であること,(3) LLMは異なる検証プロジェクトにおいて異なる性能を示すこと,(4) LLMは簡潔でスマートな証明を生成し,古典的手法を新しい定義に適用できること,そして奇異な誤りを犯す可能性があること,などを明らかにする。

関連論文リスト

• LLM4VV: Evaluating Cutting-Edge LLMs for Generation and Evaluation of Directive-Based Parallel Programming Model Compiler Tests [7.6818904666624395]
  本稿では,コンパイラテストの生成にLLMを用いたデュアルLLMシステムと実験について述べる。 LLMは、品質の高いコンパイラテストを生成し、それらを自動的に検証する有望な可能性を持っていることは明らかである。
  論文  参考訳（メタデータ） (2025-07-29T02:34:28Z)
• Towards Reliable Proof Generation with LLMs: A Neuro-Symbolic Approach [14.213719696233934]
  大型言語モデル(LLM)は厳密な論理的推論と記号的推論を必要とする形式的ドメインと競合する。 本稿では,LLMの生成強度と構造成分を組み合わせ,この課題を克服するニューロシンボリックアプローチを提案する。
  論文  参考訳（メタデータ） (2025-05-20T15:13:32Z)
• "I know myself better, but not really greatly": How Well Can LLMs Detect and Explain LLM-Generated Texts? [10.454446545249096]
  本稿では,2進(人間対LLM生成)と3進分類(未決定クラスを含む)の2つの設定において,現在のLLMの検出と説明能力について検討する。 異なる大きさの6つのオープンソースLCMを評価し、自己検出(LLM)が相互検出(他のLCMからの出力の同定)を一貫して上回っていることを発見した。 本研究は, 自己検出・自己説明における現在のLCMの限界を浮き彫りにして, 過度に適合し, 一般化性を高めるためのさらなる研究の必要性を浮き彫りにした。
  論文  参考訳（メタデータ） (2025-02-18T11:00:28Z)
• Proof Automation with Large Language Models [6.587933406842906]
  大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。 本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。 その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
  論文  参考訳（メタデータ） (2024-09-22T00:19:27Z)
• 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)
• LLatrieval: LLM-Verified Retrieval for Verifiable Generation [67.93134176912477]
  検証可能な生成は、大きな言語モデル(LLM)がドキュメントをサポートするテキストを生成することを目的としている。 本稿では,LLatrieval (Large Language Model Verified Retrieval)を提案する。 実験により、LLatrievalは幅広いベースラインを著しく上回り、最先端の結果が得られることが示された。
  論文  参考訳（メタデータ） (2023-11-14T01:38:02Z)
• Rephrase and Respond: Let Large Language Models Ask Better Questions for Themselves [57.974103113675795]
  本稿では,Rephrase and Respond'(RaR)という手法を提案する。 RaRは、パフォーマンスを改善するためのシンプルだが効果的なプロンプト方法として機能する。 また,RaRは理論的にも経験的にも,一般的なChain-of-Thought(CoT)法と相補的であることを示す。
  論文  参考訳（メタデータ） (2023-11-07T18:43:34Z)
• Assessing the Reliability of Large Language Model Knowledge [78.38870272050106]
  大規模言語モデル(LLM)は、知識探索タスクにおける高い性能のため、知識ベースとして扱われてきた。 LLMが実際に正しい答えを連続的に生成する能力をどのように評価するか。 LLMの信頼性を直接測定するための新しい指標であるMOdel kNowledge relIabiliTy score (MONITOR)を提案する。
  論文  参考訳（メタデータ） (2023-10-15T12:40:30Z)

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

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