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

大语言模型越来越多地用于自动辅导，但其在结构化符号领域的可靠性仍不明确。我们研究命题逻辑证明的逐步反馈，这需要与学习者当前证明状态精确对齐的符号推理。我们引入了一个由516个独特证明状态组成的知识图谱支撑的基准，包含逐步标注和难度指标。与依赖模型自评或二元正确性的先前辅导评估不同，我们的框架支持对反馈质量相对于已验证求解路径的细粒度分析。我们评估了三种角色特化的流水线，具有不同的求解访问权限：导师（部分求解访问）、教师（完整推导访问）和裁判（验证导师反馈）。我们的结果揭示了一个显著的非对称性：当上游反馈易出错（准确率<70%）时验证改善结果，但当反馈已经可靠（准确率>85%）时通过过度规定使性能降低4-6个百分点。关键的是，我们识别出一个共享的复杂度上限；没有任何模型或流水线能可靠地成功处理复杂度超过4-5的证明状态。这些发现挑战了添加验证器或更丰富上下文普遍改善辅导的假设，激励了根据估计复杂度和上游可靠性对问题进行路由的自适应、难度感知的架构。