💬 NLP

MioFFAn: an Annotation Software for Formula Formalization with LLM Automation Capabilities

Este artigo apresenta o MioFFAn, um framework de anotação de código aberto e customizável que estende a arquitetura MioGatto para facilitar a criação de conjuntos de dados de alta qualidade para formalização de fórmulas, combinando a anotação humana com a automação modular de Grandes Modelos de Linguagem.

Autores originais: Nicolas Sibuet, Horacio Saggion, Riccardo Rossi

Publicado 2026-07-28

📖 7 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Nicolas Sibuet, Horacio Saggion, Riccardo Rossi

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você é um detetive tentando resolver um mistério, mas as pistas estão escritas em um código secreto que apenas um computador consegue ler, enquanto a história está escrita em uma linguagem que apenas humanos entendem. Esta é a luta diária de cientistas que escrevem artigos repletos de matemática complexa. Eles usam fórmulas belas e elegantes para descrever como o mundo funciona, mas essas fórmulas são frequentemente apenas "imagens" de matemática — como o desenho de uma ponte. Para realmente construir a ponte, um computador precisa das plantas: as instruções específicas, variáveis e a lógica que dizem a uma máquina exatamente como calcular a tensão no aço. Esse processo de transformar uma "imagem" de matemática em "plantas" para um computador é chamado de Formalização de Fórmulas.

O problema é que os computadores, mesmo os superinteligentes movidos por Inteligência Artificial (IA), são péssimos em ler essas plantas por conta própria. Eles precisam de uma biblioteca massiva de exemplos — milhares de pares de "imagem matemática" e "planta de computador" — para aprender como traduzir. Mas aqui está o detalhe: ninguém construiu essa biblioteca ainda porque é incrivelmente difícil e entediante de criar. Humanos têm que se sentar e reescrever manualmente cada símbolo matemático de um artigo em código, uma tarefa tão tediosa que retarda o progresso científico. É como tentar ensinar um robô a cozinhar escrevendo à mão cada receita do zero, ingrediente por ingrediente, para cada prato do mundo.

É aqui que uma nova ferramenta chamada MioFFAn entra em cena. Pense nela como um caderno interativo de alta tecnologia projetado para tornar o trabalho entediante de traduzir matemática em código muito mais rápido e menos doloroso. Os pesquisadores por trás dela não construíram apenas uma ferramenta estática; eles construíram um sistema de "humano no circuito" (human-in-the-loop). Isso significa que o software atua como um assistente inteligente que adivinha a tradução usando IA, mas depois pede a um especialista humano para conferir e corrigir os erros. É como ter um robô que pode redigir uma carta para você, mas você ainda precisa assiná-la e garantir que os fatos estejam corretos antes de enviá-la. Ao usar essa abordagem de equipe, os autores mostram que podemos começar a construir essa biblioteca crucial de exemplos de matemática para código muito mais rápido do que antes, abrindo as portas para que os computadores finalmente entendam e executem a matemática complexa que impulsiona a ciência moderna.

A História do Artigo: Construindo uma Ponte Entre a Matemática e o Código

O artigo apresenta o MioFFAn, um software de código aberto projetado para ajudar pesquisadores a anotar documentos científicos. Seu principal objetivo é facilitar a Formalização de Fórmulas, que é o ato de pegar uma expressão matemática de um artigo e transformá-la em um código simbólico executável (como o código que você escreveria em um sistema de álgebra computacional). Os autores argumentam que, embora tenhamos ótimas ferramentas para escanear documentos e ler o texto (OCR), carecemos da "profundidade semântica" para transformar essas fórmulas escaneadas em código que um computador possa realmente executar.

Para resolver isso, os autores construíram o MioFFAn sobre uma ferramenta mais antiga chamada MioGatto. Eles perceberam que a ferramenta antiga era ótima para identificar símbolos matemáticos individuais (como a letra $x$ ), mas péssima para lidar com grupos complexos de símbolos (como uma função inteira $f(x)$ ou um tensor $\delta u_i$ ) e não permitia o tipo de anotação hierárquica e flexível necessária para a ciência do mundo real. O MioFFAn corrige isso introduzindo várias atualizações importantes:

Agrupamento e Hierarquia: Em vez de apenas marcar letras individuais, o MioFFAn permite que os usuários selecionem blocos inteiros de uma fórmula como uma única unidade. Ele trata uma expressão complexa como um "grupo" que ainda pode ser decomposto em suas partes, se necessário.
Regras Customizáveis: O software é um camaleão. Ele permite que os usuários definam suas próprias "taxonomias" (regras e categorias) para diferentes campos científicos. Por exemplo, um físico pode precisar marcar uma variável como um "vetor", enquanto um biólogo pode precisar marcá-la como uma "concentração". A ferramenta se adapta a essas necessidades.
Fundamentação Contextual: Ele ajuda a vincular os símbolos matemáticos de volta ao texto no documento onde eles são explicados. Se um artigo diz "seja $v$ a velocidade", a ferramenta ajuda você a destacar essa frase e conectar ao símbolo $v$ na fórmula.
Automação "Humano no Circuito": Esta é a parte mais emocionante. O software inclui um recurso onde uma IA (especificamente, um Modelo de Linguagem Grande, ou LLM) tenta fazer a anotação primeiro. Ela sugere quais partes da fórmula são o quê, o que as variáveis significam e onde elas são definidas no texto. No entanto, o usuário humano não é substituído; ele atua como um supervisor. Eles revisam as sugestões da IA, corrigem quaisquer erros e confirmam o resultado final.

Os autores testaram este sistema usando um campo científico específico chamado Métodos de Elementos Finitos (FEM), que é usado para simular coisas como o impacto de um carro ou a curvatura de uma ponte. Eles configuraram o software para entender as regras matemáticas específicas de FEM e então realizaram um experimento de "prova de conceito". Eles alimentaram o software com alguns artigos científicos e deixaram a IA tentar anotar, depois compararam o trabalho da IA contra um "padrão ouro" criado por especialistas humanos.

Os resultados foram uma mistura de promessa e realidade. A IA foi surpreendentemente boa em algumas coisas, mas teve dificuldades em outras. Por exemplo, quando a IA tinha permissão para ver os símbolos matemáticos originais (como a letra grega $\lambda$ ), ela teve um desempenho muito melhor na identificação das partes da fórmula (cerca de 57,7% de cobertura) do que quando os símbolos eram substituídos por nomes de texto longos (o que caiu para 36,2%). No entanto, a IA ainda não é perfeita; ela frequentemente teve dificuldade em localizar precisamente a definição de texto no documento, às vezes destacando parágrafos inteiros em vez de apenas a frase específica.

O artigo descarta explicitamente a ideia de que a IA possa realizar este trabalho perfeitamente sozinha atualmente. Os autores afirmam que os resultados automatizados estão "longe de serem ideais" e devem ser usados apenas como um "baseline" que um especialista humano refina rapidamente. Eles argumentam que tentar usar a IA para uma tradução totalmente automática de ponta a ponta, sem verificações humanas, provavelmente levaria a erros difíceis de detectar.

Em sua avaliação, os autores descobriram que a abordagem de "Caracteres Originais" (manter os símbolos matemáticos como estão) funcionou melhor para a IA entender a estrutura da matemática. Eles também compararam três modelos de IA diferentes (Nemotron da NVIDIA, Gemma do Google e Qwen da Alibaba) e descobriram que o modelo Qwen3-4B-Instruct-2507 teve um desempenho significativamente melhor que os outros, alcançando uma taxa de cobertura de 57,7% na identificação de símbolos, comparado a aproximadamente 33,9% do segundo melhor modelo.

Em última análise, o artigo sugere que o MioFFAn é um "playground" poderoso para desenvolver melhores estratégias de automação. Ele não afirma ter resolvido o problema de traduzir matemática para código para sempre. Em vez disso, oferece uma estrutura flexível onde pesquisadores podem testar diferentes estratégias de IA, ver o que funciona e melhorar o sistema gradualmente. Os autores concluem que, embora a automação atual seja apenas um passo "provisório", essa parceria entre humano e IA é a maneira mais eficaz de construir os conjuntos de dados de alta qualidade necessários para treinar sistemas futuros e mais inteligentes. Eles vislumbram um futuro onde esta ferramenta ajude a construir uma biblioteca massiva e compartilhada de traduções de matemática para código, tornando mais fácil para os computadores ajudarem os cientistas a resolver seus problemas mais complexos.

Resumo Técnico: MioFFAn

Definição do Problema

A tradução automática de expressões matemáticas encontradas na literatura científica em código simbólico executável — definida neste trabalho como Formalização de Fórmulas — é atualmente dificultada por uma severa escassez de conjuntos de dados de alta qualidade e de verdade fundamental (ground-truth) especializados para domínios científicos técnicos. Embora os sistemas de Reconhecimento Óptico de Caracteres (OCR) possam extrair formatos de apresentação como LaTeX ou MathML, eles carecem da profundidade semântica e computacional necessária para implementar essas fórmulas em código. Embora os Grandes Modelos de Linguagem (LLMs) ofereçam um mecanismo promissor para orquestrar essa transformação, seu desenvolvimento está estagnado pela falta de corpora de referência que capturem informações contextuais específicas, tais como definições de variáveis, propriedades de operadores e restrições específicas do domínio. Ferramentas de anotação existentes focam frequentemente na identificação de símbolos individuais ou resolução de correferência, em vez da geração do código simbólico que orquestra esses elementos.

Metodologia

Os autores apresentam o MioFFAn (Math identifier-oriented Formula Formalization Annotator), um framework de código aberto, centrado no documento e customizável, projetado para facilitar a anotação rápida para a Formalização de Fórmulas. O sistema é construído sobre a arquitetura MioGatto, mas introduz extensões estruturais e funcionais significativas para abordar as limitações da ferramenta original.

Arquitetura do Framework e Melhorias

O MioFFAn opera como uma aplicação cliente-servidor (TypeScript/Python) usando HTML e MathML para permitir a interação dinâmica baseada na web. As principais melhorias arquiteturais em relação ao MioGatto incluem:

Gestão Hierárquica e Composta de Identificadores: O sistema estende a definição de Identificadores Matemáticos (MIs) além de tags <mi> únicas para suportar estruturas compostas (ex: subscritos, sobrescritos) e Grupos definidos pelo usuário. Isso permite que notações complexas (ex: $\delta u_i$ ou $f(x)$ ) sejam tratadas como entidades únicas, preservando a capacidade de anotar os símbolos constituintes.
Esquema de Propriedades Desacoplado: O framework separa Propriedades Semânticas Invariantes (atribuídas a um Conceito, ex: "vetor velocidade") de Propriedades Variantes (atribuídas a uma Ocorrência, ex: "transposto"). Isso permite que conceitos sejam reutilizados em diferentes notações e modalidades de implementação.
Fundamentação Flexível: As Fontes de Fundamentação (SoG) agora suportam o destaque de intervalos (inter-span highlighting) entre múltiplos nós HTML e são associadas a Conceitos em vez de Ocorrências individuais, permitendo a seleção de fórmulas inteiras exibidas ou segmentos de texto entre nós.
Fluxo de Trabalho Centrado no Documento: Os usuários podem navegar entre múltiplas amostras de documentos dentro de uma única sessão sem reinicializações do servidor, e o sistema suporta o preenchimento dinâmico de esquemas de anotação via configuração JSON.

Recursos de Formalização de Fórmulas

Para visar especificamente a Formalização de Fórmulas, o MioFFAn introduz três recursos principais:

Equações de Interesse (EoI): Os usuários designam expressões específicas para formalização, o que inicializa uma entrada dedicada no esquema de anotação.
Nomes de Variáveis Canônicos: Cada Conceito é mapeado para um Nome de Variável único para garantir uma representação inequívoca no código simbólico gerado.
Construção Integrada de Código Simbólico: Um ambiente interativo fornece uma paleta de Nomes de Variáveis definidos e operadores específicos do domínio (ex: grad(), div()) para auxiliar os usuários na síntese do código simbólico final, minimizando erros de sintaxe manuais.

Pipeline de Automação

O MioFFN incorpora um pipeline de automação modular com participação humana (human-in-the-loop) via LLMs. A automação é desacoplada da aplicação principal, permitindo que pesquisadores troquem estratégias. O pipeline consiste em três sub-tarefas:

Segmentação de Símbolos: O LLM identifica elementos MathML ou estruturas compostas para serem agrupados como Ocorrências únicas.
Atribuição de Conceitos: O LLM sugere Conceitos (com Nomes de Variáveis e descrições) e os mapeia para os símbolos segmentados.
Identificação de SoG: O LLM identifica intervalos de texto ou fórmulas que servem como evidência para os Conceitos.

O sistema impõe formatos de saída rigorosos (listas de Grupos, Conceitos, etc.) para permitir a avaliação agnóstica de metodologia usando métricas padrão de NLP.

Caso de Uso e Avaliação

O framework foi configurado para Métodos de Elementos Finitos (FEM), um domínio que exige a caracterização precisa de tensores de alta dimensão e formulações variacionais. Uma taxonomia customizada e uma biblioteca de operadores (visando um compilador baseado em Sympy para KratosMultiphysics) foram definidas.

Uma avaliação preliminar de prova de conceito foi conduzida em um conjunto curado de 6 amostras de FEM usando um modelo local Qwen3-4B-Instruct. A avaliação comparou duas variantes de automação:

Caracteres Originais: Os LLMs processaram HTML com caracteres Unicode não padronizados.
Nomes Explícitos: Os LLMs processaram HTML onde os caracteres Unicode foram substituídos por nomes explícitos (ex: "GREEK SMALL LETTER LAMBDA").

Resultados:

A variante de Caracteres Originais superou significativamente a variante de Nomes Explícitos em Segmentação de Símbolos (57,7% de cobertura vs. 36,2%; 36,8% CoNLL vs. 26,9%).
A variante de Nomes Explícitos mostrou melhorias marginais em Atribuição de Conceitos e Identificação de SoG.
A análise qualitativa revelou que, embora o modelo frequentemente identificasse o contexto semântico correto, ele teve dificuldades com a especificação precisa de IDs de tags na tarefa de Identificação de SoG, destacando frequentemente parágrafos inteiros em vez de sentenças específicas.

Principais Contribuições

Framework MioFFAn: Uma ferramenta de anotação especializada e de código aberto que preenche a lacuna entre a notação matemática e o código simbólico executável, abordando a escassez de dados de verdade fundamental para a Formalização de Fórmulas.
Extensões Arquiteturais: Melhorias significativas sobre a linha de base MioGatto, incluindo suporte para identificadores compostos, esquemas de propriedades desacoplados e mecanismos de fundamentação flexíveis.
Automação Modular: Um design de pipeline que permite o refinamento iterativo de estratégias de LLM através de sub-tarefas modulares, facilitando a avaliação de abordagens de automação concorrentes.
Adaptabilidade de Domínio: Demonstração da configurabilidade do framework através de uma aplicação específica aos Métodos de Elementos Finitos, incluindo uma taxonomia e um conjunto de operadores customizados.

Significância e Alegações

O artigo posiciona o MioFFAn não como uma solução totalmente automatizada, mas como um campo de experimentação de participação humana (human-in-the-loop). Os autores alegam que o valor primário do framework reside em sua capacidade de:

Facilitar a criação de conjuntos de dados de alta qualidade e específicos de domínio necessários para treinar e testar LLMs para a Formalização de Fórmulas.
Permitir que pesquisadores refinem iterativamente as capacidades de automação ao isolar sub-tarefas específicas (segmentação, atribuição, fundamentação) e avaliá-las com métricas padrão.
Fornecer uma linha de base para automação que pode ser rapidamente refinada por especialistas humanos, reconhecendo que as capacidades atuais dos LLMs são insuficientes para a formalização totalmente autônoma em domínios científicos complexos.

Os autores concluem que, embora a automação atual não seja ideal, o design modular do MioFFAn suporta efetivamente o desenvolvimento de fluxos de trabalho automatizados mais sofisticados no futuro, abordando, em última análise, o gargalo da escassez de dados na geração de código científico.