研究人员开发了CAPRI，这是一个新颖的工作流程，旨在提高大型语言模型（LLM）为Isabelle定理证明器生成证明的可靠性。CAPRI引入了一个契约感知的修复机制，其中Isabelle验证证明的正确性，而一个独立的检查器强制执行机器可读的编辑契约，以确保LLM仅修改授权的部分。对失败证明的评估表明，CAPRI显著降低了未经授权修改的风险，特别是在关注证明体而不是整个理论时。该系统在各种配置下进行了测试，包括与OpenRouter和OpenAI的比较，在生成有效修复并保持完整性方面显示出有希望的结果。 AI
影响 通过确保模型编辑符合指定的契约来增强对LLM辅助形式化验证的信任。
排序理由 学术论文，详细介绍了LLM在定理证明中生成证明的新方法。[lever_c_demoted from research: ic=1 ai=1.0]
AI 生成摘要 · Google Gemini · 来自 1 个来源。 我们如何撰写摘要 →
