CoqPilot：一個基於大型語言模型生成 Coq 證明的外掛程式

Grunnleggende konsepter

CoqPilot 是一個 VS Code 外掛程式，旨在利用大型語言模型和其他方法簡化 Coq 程式碼的生成，並透過整合多種生成方法和自動校驗功能，協助使用者更有效率地編寫 Coq 證明。

Sammendrag

CoqPilot 概述

CoqPilot 是一個為 VS Code 開發的插件，旨在協助自動生成 Coq 證明。它會收集 Coq 檔案中標記為 admit 的部分（即待證明的目標），並結合大型語言模型（LLM）和非機器學習方法來生成候選證明。然後，CoqPilot 會檢查每個候選證明是否解決了給定的子目標，如果成功，則用它替換 admit。

CoqPilot 的主要目標

1. 讓使用者能夠無縫地結合多種 Coq 生成方法。
2. 提供一個零設置的工具使用體驗。
3. 為基於 LLM 的 Coq 證明生成實驗提供一個平台。

CoqPilot 的功能

• 整合多種 Coq 生成方法，包括 OpenAI API、本地運行的 LLM、JetBrains AI 平台和預定義的自動化策略。
• 自動檢查多個生成的證明候選，並向使用者呈現有效的證明。
• 實現前提選擇，以便更好地提示 LLM。
• 創建一個 LLM 引導的機制，嘗試藉助 Coq 的錯誤訊息修復失敗的證明。
• 提供一個基準測試系統，用於評估 Coq 生成方法的效能。

CoqPilot 的優勢

• 與傳統的 Coq 生成工具相比，CoqPilot 更易於設置和使用。
• 它允許使用者組合不同的生成方法，從而提高生成成功的可能性。
• CoqPilot 的自動校驗功能確保只向使用者呈現有效的證明。
• 其模組化架構使其易於適應其他定理證明器。

CoqPilot 的限制

• CoqPilot 依賴於 Coq-LSP，它僅支援從 8.15 版本開始的 Coq 版本。
• 商業 LLM 提供者對其模型的使用率有限制，這可能會影響 CoqPilot 的效能。

CoqPilot 的未來方向

• 開發更先進的技術來增強 LLM 在生成 Coq 程式碼方面的能力。
• 將 CoqPilot 適配到其他定理證明器。
• 探索使用 CoqPilot 來生成更複雜的證明。

Statistikk

在 IMM 專案中，長度不超過 20 個策略的證明佔所有證明的 83%。
使用 CoqPilot 和 GPT-4o 模型，51% 的定理在第一次嘗試時就被成功證明。
將 CoqPilot 與其他 Coq 自動化工具（如 CoqHammer 和 Tactician）結合使用，可以證明 51% 的定理。
在一個包含 50 個定理的實驗中，使用 CoqPilot 的多輪機制成功修復了 2 個額外證明。

Sitater

"我們希望讓使用者能夠無縫地結合多種 Coq 生成方法，並為我們的工具提供零設置的體驗。"
"我們希望為基於 LLM 的 Coq 證明生成實驗提供一個平台。"
"與單獨使用 LLM 相比，CoqPilot 的修改將 GPT-4o 的成功率從 0% 提高到了 34%。"

Viktige innsikter hentet fra

CoqPilot, a plugin for LLM-based generation of proofs

by Andrei Kozyr... klokken arxiv.org 10-28-2024

https://arxiv.org/pdf/2410.19605.pdf

Dypere Spørsmål

除了大型語言模型，還有哪些其他技術可以用於自動生成 Coq 證明？

除了大型語言模型 (LLM) 外，還有其他幾種技術可用於自動生成 Coq 證明：

搜尋式證明搜尋 (Search-based Proof Search)：這種方法將證明搜尋問題轉化為在可能的證明步驟空間中進行搜尋。CoqHammer [4] 就是一個例子，它將 Coq 的邏輯轉換為無類型一階邏輯，並使用先進的搜尋技術來尋找證明。
基於規則的系統 (Rule-based Systems)：這些系統使用預先定義的規則和策略來指導證明過程。它們通常依賴於專家知識和啟發式方法來選擇適當的證明步驟。
基於範例的推理 (Example-based Reasoning)：這種方法從現有的證明中學習，並嘗試將學到的知識應用於新的證明問題。Tactician [3] 中實現的 K-NN 方法就是一個例子，它根據類似情況下使用的策略來預測策略。
歸納邏輯程式設計 (Inductive Logic Programming)：這種方法從正例和反例中學習邏輯程序。在 Coq 證明生成的背景下，這可能涉及從成功的和不成功的證明嘗試中學習。
互動式定理證明 (Interactive Theorem Proving)：雖然不是完全自動化的，但互動式定理證明器（如 Coq 本身）為用戶提供了強大的工具和策略，以幫助他們構建證明。這些工具可以自動化證明過程中的許多步驟，並為用戶提供有關如何進行的指導。
這些技術各有優缺點，並且通常可以組合使用以實現更好的性能。

CoqPilot 如何處理 Coq 證明生成過程中常見的歧義性問題？

Coq 證明生成過程中經常會遇到歧義性問題，例如：

多個可能的證明路徑: 對於一個給定的目標，可能存在多種不同的證明方法。
策略選擇: Coq 提供了大量的策略，選擇正確的策略對於成功的證明至關重要。
隱含資訊: Coq 證明通常依賴於大量的背景知識和定理，這些資訊可能沒有明確地在當前證明狀態中體現出來。
CoqPilot 透過以下方式處理這些歧義性問題：

多模型生成: CoqPilot 可以利用多個 LLM 或其他證明生成服務，並行生成多個候選證明。這種方法可以增加找到正確證明的機率。
前提選擇: CoqPilot 使用「前提選擇」技術，從當前檔案或專案中選擇相關的定理和定義，並將其作為 LLM 的上下文資訊。這有助於 LLM 理解當前的證明目標，並生成更準確的證明。
自動校驗: CoqPilot 使用 Coq 語言伺服器 (Coq-LSP) 來自動校驗生成的證明。這確保只有有效的證明才會被接受。
錯誤修復: 如果生成的證明無效，CoqPilot 可以分析 Coq-LSP 返回的錯誤訊息，並嘗試修復證明。這通常涉及修改證明的某些步驟，或添加缺少的資訊。
透過結合這些方法，CoqPilot 可以有效地處理 Coq 證明生成過程中的歧義性問題，並提高自動生成正確證明的成功率。

如果將 CoqPilot 的自動證明生成能力應用於軟體開發的其他領域，會產生什麼樣的影響？

將 CoqPilot 的自動證明生成能力應用於軟體開發的其他領域，將會產生深遠的影響：

提高軟體品質: 自動證明生成可以幫助開發人員在開發過程中及早發現和修復錯誤，從而提高軟體品質。
降低開發成本: 自動化證明生成可以減少開發人員花費在手動編寫和調試證明上的時間，從而降低開發成本。
促進形式化方法的應用: 自動證明生成可以降低形式化方法的使用門檻，使其更容易被更廣泛的開發人員所接受和使用。
以下是一些具體的應用場景：

智慧合約驗證: 自動證明生成可以用於驗證智慧合約的正確性和安全性，從而減少因程式碼錯誤而造成的財務損失。
安全關鍵系統開發: 在航空航天、醫療設備等安全關鍵系統的開發中，自動證明生成可以用於確保系統的可靠性和安全性。
程式碼自動生成: 自動證明生成可以與程式碼自動生成技術相結合，生成既滿足規範又具有可證明正確性的程式碼。
總體而言，將 CoqPilot 的自動證明生成能力應用於軟體開發的其他領域，將有助於提高軟體品質、降低開發成本，並促進形式化方法的應用，從而推動軟體開發行業的發展。