验证何时有害：多智能体反馈在逻辑证明辅导中的非对称效应

大语言模型（LLM）越来越多地用于自动辅导，但其在结构化符号领域的可靠性仍不清楚。我们研究命题逻辑证明的步骤级反馈，这类反馈要求与学习者当前证明状态对齐的精确符号推理。我们引入一个以知识图谱为基础的基准，包含516个独特证明状态以及步骤级标注与难度指标。与依赖模型自评或二元正确性的既有辅导评估不同，我们的框架能够对照经验证的解题路径对反馈质量进行细粒度分析。我们评估了三种具有不同解法访问权限的角色专业化流水线：Tutor（部分解法访问）、Teacher（完整推导访问）和Judge（对Tutor反馈进行验证）。结果揭示出显著的非对称性：当上游反馈错误较多（准确率<70%）时，验证能改善结果；而当反馈已相当可靠（准确率>85%）时，验证会因过度细化使性能下降4-6个百分点。关键的是，我们发现存在共同的复杂度天花板：对复杂度超过4-5的证明状态，没有任何模型或流水线能稳定成功。这些发现挑战了“加入验证器或更丰富上下文必然改善辅导”的假设，推动构建按估计复杂度与上游可靠性路由问题的自适应、难度感知架构。