IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus

• 类型：arxiv
• 标识：2606.18098
• 链接：http://arxiv.org/abs/2606.18098v1
• 主分类：risk
• 形态：method
• 被引：1
• 被引来源：Semantic Scholar
• S2被引：1
• OpenAlex被引：0
• 影响力被引：0
• TLDR：A Retrieval-Augmented Generation framework, Error tracing and counterexample generation for improved context supplied to the Large Language Model, and Compatibility with the latest version of Isabelle and Sledgehammer is implemented for improved efficiency.
• OpenAlex ID：W7165061037
• OpenAlex DOI：10.48550/arxiv.2606.18098
• DOI：10.48550/arxiv.2606.18098
• DOI来源：OpenAlex
• 开放获取：green
• 开放获取链接：https://doi.org/10.48550/arxiv.2606.18098
• OpenAlex更新：2026-07-19
• 待LLM分类：否
• 标题中文：IsabeLLM：将自动定理证明应用于共识协议的形式化验证
• TLDR中文：实现了一个 RAG 框架，包含面向 LLM 的错误追踪与反例生成以提供更优上下文，并兼容最新版 Isabelle 与 Sledgehammer 以提升效率。
• 来源文件：
• /inbox/tom/_candidates/2026-06-17-agent-rag-longcontext-candidates.json
• [S2 enrich]
• [OpenAlex backfill]