LLM写安全证明效果不佳
matthew_d_green · x · 2026-07-14
Matthew Green 说他最近尝试让 **ChatGPT** 和 **Fable** 帮他写新的 **安全证明**（不是 correctness proofs），目标语言是 **EasyCrypt** 或 **Lean**，但效果“不太理想”。 这条短帖的价值在于它给出了一个非常具体的实测反馈： - LLM 在形式化安全证明这种任务上，至少在作者的使用场景里还不够可靠； - 问题不是“完全不会写”，而是离可用还有明显距离； - 作者也留了一个开放口子：也许是自己的提示方式不对。