aclanthology.org来源发表:
几何证明不再只靠模型硬推：先找结构相似的旧题，再用符号验证器逐条纠错
核心概要
通用大模型写几何证明时，先检索结构相似、证明已知的旧题作为示例，再由符号验证器逐轮指出错误，完整流程在FormalGeo-7k的50道SAT级欧氏几何题上把证明正确率提到68%–96%，而既不用类比检索也不用验证器反馈的基线为10%–44%。在同样带验证器反馈、同样推理预算下，仅加入类比引导就把GPT-5从88%提到96%、o1从52%提到80%。
正在载入内容…
通用大模型写几何证明时，先检索结构相似、证明已知的旧题作为示例，再由符号验证器逐轮指出错误，完整流程在FormalGeo-7k的50道SAT级欧氏几何题上把证明正确率提到68%–96%，而既不用类比检索也不用验证器反馈的基线为10%–44%。在同样带验证器反馈、同样推理预算下，仅加入类比引导就把GPT-5从88%提到96%、o1从52%提到80%。
通用大模型可以借助结构相似的旧题及其完整证明来写新证明，而不必只靠自身对定理的搜索。 此前的做法是让模型直接生成证明，正确性没有形式化保证；这里把类比检索和符号验证器一起接入生成流程。 在FormalGeo-7k抽样的50道题上，完整流程的正确率为68%–96%，不使用类比检索与验证器反馈的基线为10%–44%。
每道题先被改写成去掉具体名称和数值的抽象形式，再据此找出证明结构相近的旧题。 检索依据是构造、条件与目标三部分的Jaccard相似度，并用一个三层神经网络回归预测两道题的证明相似度。 在预测相似度高于0.95的问题对上，71%的真实证明相似度落在最高的两个区间，而全部问题对中只有1.28%超过该阈值。
验证器只检查证明本身是否成立，不知道标准答案，因此它判断的是答案能否由证明推出。 验证器把证明步骤和几何约束编码成逻辑公式与代数表达式，用SMT求解器Z3检验一致性，并按语法违规、前提缺失、未达目标三档给出反馈。 在o1上，允许验证器反馈重试后，类比方法的正确率从48%升到68%，基线从10%升到38%。
只保留相似题证明中用到的定理，可以显著缩小提示中的定理表。 完整定理表约196条定理、平均约18K token，基线因此提示更长、重试更多。 取k=100时，相似题覆盖了96%目标证明所需的全部定理，平均只用26.66条定理，约为完整表的13.6%；o1的平均提示从18K降到2.5K token。
结论建立在FormalGeo-7k的SAT级欧氏几何题上，主实验为每个难度各10题、共50题的样本，验证器为基于Z3的符号系统；作者计划把方法扩展到几何之外的领域，并探索更强的形式验证与类比检索机制。
作者指出，抽象方案只把实体名和数值替换为占位符，可能漏掉更深的结构关系；Z3不支持反三角函数，需要由三角函数值反推角度的证明无法验证；模型看不到图形，弧相关推理会出错；结果能否推广到几何之外的领域仍需评估。