# 符号验证

通用大模型写几何证明时，先检索结构相似、证明已知的旧题作为示例，再由符号验证器逐轮指出错误，完整流程在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%。

面向带硬约束的规划任务，一种新的偏好优化目标把二值偏好信号换成由确定性符号验证器算出的连续违反幅度，并按违反严重度缩放，同时用字典序目标把硬约束与软偏好分开。此前直接偏好优化对所有违反给同一训练信号，且当偏好对来自不同模型家族时容易受长度与风格偏置影响。配套的合成流程用程序化约束画像和最小编辑蒸馏生成偏好对，8B模型在TravelPlanner上取得89.2%通过率、NaturalPlan上93.4%调度率，在未见过的PlanBench Blocksworld上比GPT-4o高9.2个百分点。

面向带硬约束的规划任务，一种新的偏好优化目标把二值偏好信号换成由确定性符号验证器算出的连续违反幅度，并按违反严重度缩放，同时用字典序目标把硬约束与软偏好分开。此前直接偏好优化对所有违反给同一训练信号，且当偏好对来自不同模型家族时容易受长度与风格偏置影响。配套的合成流程用程序化约束画像和最小编辑蒸馏生成偏好对，8B模型在TravelPlanner上取得89.2%通过率、NaturalPlan上93.4%调度率，在未见过的PlanBench Blocksworld上比GPT-4o高9.2个百分点。