感知契约的漂移Isabelle开发修复：双水箱案例研究
Contract-Aware Rescue of a Drifted Isabelle Development: The Double-Tank Case Study
浏览论文内容
中文总结 AI 辅助
针对Isabelle开发漂移问题，以双水箱控制器案例为研究对象，用CAPRI工具重构修复了10个义务，完成部分验证工作，为交互式定理证明器的开发维护提供了实践参考。
中文摘要 AI 辅助
大语言模型可对交互式定理证明器提出证明，但成功构建并不能表明周围验证任务被保留。我们在采样数据双水箱控制器的Isabelle开发中研究此问题。该工作始于9个理论和10个未完成的义务，最终构建出不含sorry、oops、附加公理化或预言机使用的16个理论，积累了23个稳定和36个破损的证明状态。回顾性审计发现100个原始声明中有16个发生实质性变更，包括弱化的端到端保证定理，其结论假设了四个要求中的三个。我们使用感知契约的证明修复工具CAPRI，结合Isabelle接受度与机器可读编辑契约对仓库变更的独立检查来指导重构，在原始9个理论结构内解除了全部10个范围限定义务。共同作者的二次复现复制了R10构建、契约检查、控制测试及主要审计发现，独立复现仍为未来工作。操作端到端验证仍未完成：我们仍需将操作执行与重构的定量跟踪契约关联，此任务需要扩展契约。
英文摘要
Large language models can propose proofs for interactive theorem provers, but a successful build does not show the surrounding verification task was preserved. We study this problem in an Isabelle development of a sampled-data double-tank controller. The work began with nine theories and ten unfinished obligations, grew to a 16-theory build without sorry, oops, added axiomatisation, or oracle use, and accumulated 23 stable and 36 broken proof states. A retrospective audit found material changes in 16 of the 100 original declarations, including a weakened end-to-end assurance theorem that assumed three of the four requirements in its conclusion. We used CAPRI, a contract-aware proof-repair tool, to govern a reconstruction by combining Isabelle acceptance with an independent check of repository changes against machine-readable edit contracts. The reconstruction discharged all ten scoped obligations within the original nine-theory structure. A secondary replay by a co-author reproduced the R10 build, contract checks, control tests, and principal audit findings; independent replication remains future work. Operational end-to-end verification remains incomplete: we still need to connect operational executions to the reconstructed quantitative trace contract, a task requiring an extended contract.
