IA e os Problemas Difíceis do Mundo · Matemática · arXiv · 2026-10-19
Além da compilação: avaliando a formalização fiel de enunciados em linguagem natural para Lean
Título original: Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization
O Lean verifica que uma declaração gerada está bem tipada, mas não que ela corresponde à intenção do usuário; por isso, os autores medem o quanto a compilação superestima a fidelidade na autoformalização de enunciados. O critério deles exige compilação no Lean e a concordância de dois juízes LLM de famílias de modelos diferentes, e concorda com a maioria humana em 91,5% dos casos em uma auditoria aleatória independente. Em 227 enunciados de nível universitário, em oito sistemas, a diferença entre as saídas que compilam e as aceitas varia de 1,3 a 29,5 pontos percentuais; o agente com ferramentas compila 87,2% dos enunciados, mas apenas 57,7% são aceitos.