10:30
官方一手arXiv: OpenAI@Jim Woodcock, Gabriel Leite, Augusto Sampaio, Ran Wei
推荐理由：这论文搞了个 CAPRI 工具，管 LLM 改 Isabelle 证明，能查它有没有动不该动的地方。12 个失败证明跑 180 次，修复率直观看得很清楚，想用 LLM 做形式化证明的可以看看。
CAPRI
共 1 条相关 AI 资讯
8月14日
10:30
CAPRI 是一种面向 Isabelle 证明的契约感知修复工作流，由 Isabelle 检查证明，独立检查器执行机器可读的编辑契约。研究在四个开发项目的十二个失败证明上评估了五种工作流，每任务三份复现，共 180 次运行和 138 次有效修复。其中 144 个被 Isabelle 接受的候选修复有六个修改了受保护文本，均来自可编辑完整理论的迭代工作流。仅限证明体的接口得到 29/36 个有效修复且无契约违规，而对应完整理论工作流为 31/36。