Este artículo introduce una matriz de cobertura de señales para estratificar los errores de tipo y semánticos en la autoformalización de LLM, superando las métricas escalares de corrección de tipo. El marco clasifica las salidas en celdas de éxito verdadero, solo tipo, solo semántico o fallo en ambas categorías cruzando los resultados del elaborador de Lean con juicios de equivalencia semántica.

  • El análisis de ProofNet# y MiniF2F-test con DeepSeek V4-Pro muestra que los métodos de feedback de elaboración recuperan aproximadamente el 64% de los errores del estrato de tipo, aumentando las tasas de éxito verdadero en 34 a 36 puntos porcentuales.
  • La tasa de recuperación de solo tipo a éxito verdadero predice el delta de éxito verdadero en métodos no vistos dentro de 2/186 y hace que el delta de corrección de tipo sea lineal con la tasa de fallo del elaborador vanilla, con un R-cuadrado de 0.96.
  • Los jueces simbólicos discrepan con los jueces semánticos entre 26 y 37 puntos porcentuales en las salidas de feedback de elaboración, con falsos negativos a menudo rastreables a reescrituras forzadas por el elaborador.

Los autores argumentan que los avances en la corrección de tipo deben atribuirse a movimientos específicos en las celdas de error en lugar de solo mejoras escalares, ya que esto revela qué métodos resuelven efectivamente tipos de errores distintos.