描述精益 4 自动形式化中由释义引起的失败的特征

近年来，Lean 4 自动形式化变得越来越流行，前沿语言模型和开放权重自动形式化器现在可以生成数学定理的有效形式化。然而，这些评估通常依赖于定理的单一规范措辞，很少探讨输出对于输入的自然变化是否稳健，而先前的工作表明，语义上等效的释义经常会导致不同的形式输出。我们通过将确定性释义规则应用于本科生和奥林匹克级别数学问题的数据集来研究精益 4 中这些分歧的结构。在四个前沿模型和三个开放权重自动形式化器中，我们发现释义敏感性主要由代码生成层的故障主导，并且这些故障的类型因数据集而异。此外，这些模式推广到开放权重模型，表明最先进的自动形式化器仍然难以生成有效的精益代码。我们的结果为自动形式化提供了失败模式分类，并激发针对特定编译失败的训练时间干预。