日志
AI辅助做定理证明的几点心得
热度 11
1. 提前写出非形式的证明。这一点最关键。后面需要反复用这些非形式证明与AI进行交互，给出提示。
2. 相信AI的建模和构造能力，但是不要指望它们的自我纠错能力。如果AI提供的证明代码有问题，不要浪费时间在同一抽象层级反复询问AI。
3. 尽可能细化和分解自己的证明，降低证明的复杂度。
4. 如果已经证明到单句，可以让AI提供对应该单句的可理解的结构化证明。
发表评论 评论 (5 个评论)
- 回复 xiejin77
- 唐老师的非形式证明指的是自己对于证明的思路吧，理论上说借助一些prompt去对于命题做形式化定义，可能会让大模型有更准确的证明能力。
我个人的经验，反复用这些非形式证明与AI进行交互，对基础模型能力是个很大的考验，多跳之后的回答，指令遵从和逻辑关联上很容易出现问题。我在隐私计算领域跟主流大模型讨论一些问题的时候，经常出现前几次的回答准确，后面突然在某一个轮次出现偏离的情况
- 回复 唐家山
- 是的，我说的是在构建形式证明前，需要先有自己的证明思路。如果没有证明思路就贸然用AI辅助进行证明，往往会被AI带到沟里去。
xiejin77: 唐老师的非形式证明指的是自己对于证明的思路吧，理论上说借助一些prompt去对于命题做形式化定义，可能会让大模型有更准确的证明能力。
我个人的经验，反复用这 ...
我现在赞同陶哲轩的看法，AI是一个笨拙而勤快的助手。考虑到陶哲轩的智力超出我许多，这个“笨拙”可能需要打引号。
AI辅助证明要成功，最关键的是层层分解，这样在宏观上证明有一个明确的方向。这样就可以尽量避免AI的幻觉带来的各种偏离。
最后，AI辅助的证明，可以让我从繁重的构建工作解脱出来，转而去关注证明正确性的check工作，这个是AI辅助对我最大的意义。