FormInv：数学推理基准中语义不变性的测量协议

FormInv提出数学推理基准语义不变性测量协议。审计发现47%自动生成的语义改写存在错误，并定义条件不一致率（CIR）以隔离定理内失败聚类。 该协议在9个模型上评估366至811个经Lean4验证的题目，结果显示Claude Haiku 4.5的CIR（41.9%）远高于DeepSeek V3（4.7%）。