💻 computer science

FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean

Este artigo apresenta o **FormalScience**, um pipeline de agentes com intervenção humana que permite a especialistas em ciência formalizarem raciocínios científicos complexos em código Lean4, introduzindo também o **FormalPhysics**, um novo conjunto de dados de física de nível universitário para avaliar a capacidade de modelos de linguagem em realizar autoformalização sem perda de significado semântico.

Autores originais: Jordan Meadows, Lan Zhang, Andre Freitas

Publicado 2026-04-28

📖 4 min de leitura☕ Leitura rápida

CC BY 4.0

Autores originais: Jordan Meadows, Lan Zhang, Andre Freitas

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

O Tradutor de "Física para Robôs": Entendendo o FormalScience

Imagine que você é um cientista brilhante. Você escreve suas descobertas em um caderno, usando símbolos bonitos, setas, integrais e uma linguagem que parece poesia matemática (o famoso LaTeX). Para um ser humano, isso é claro e elegante.

Agora, imagine que você precisa explicar essa mesma descoberta para um robô extremamente rigoroso, como o Lean (um sistema de "prova formal"). Esse robô não aceita "mais ou menos". Ele não entende "o campo de força aumenta um pouco"; ele exige que você defina exatamente o que é o campo, o que é a força, e prove cada milímetro do caminho usando uma lógica de ferro. Se você esquecer uma vírgula, o robô trava e diz: "Erro! Não entendi!"

O problema é que, até hoje, pedir para uma Inteligência Artificial (como o ChatGPT) traduzir a "poesia" do cientista para a "gramática rígida" do robô tem sido um desastre. A IA muitas vezes inventa coisas ou simplifica tanto o problema que a descoberta perde o sentido.

É aqui que entra o projeto FormalScience.

1. O Método: O "Professor Particular" (Human-in-the-Loop)

Os pesquisadores criaram um sistema chamado FormalScience. Em vez de deixar a IA tentando adivinhar a tradução sozinha, eles criaram uma "ponte".

Imagine que a IA é um tradutor iniciante e o cientista é o professor. O processo funciona assim:

A IA tenta traduzir o problema de física para o código do robô.
O robô tenta ler e, se encontrar um erro, "grita" o erro para a IA.
A IA tenta consertar.
O toque de mestre: O cientista humano entra no meio do processo para dizer: "Ei, IA, você traduziu certo a gramática, mas você mudou o sentido da física! Volte e corrija isso!"

Isso permite que um especialista em física (que não sabe programar para robôs) consiga criar um conjunto de provas perfeitas e verificáveis com um custo muito baixo.

2. O Resultado: O "Dicionário de Física" (FormalPhysics)

Usando esse método, eles criaram o FormalPhysics, um banco de dados com 200 problemas de nível universitário (como Mecânica Quântica e Eletromagnetismo) que já vêm com a tradução perfeita para o robô. É como se eles tivessem criado o primeiro "Dicionário de Tradução de Física para Máquinas" de alta qualidade.

3. O Grande Problema: A "Perda de Sentido" (Semantic Drift)

Aqui está a parte mais fascinante e um pouco assustadora que o artigo revela. Eles descobriram que, quando a IA tenta traduzir física para o código do robô, acontece algo chamado "Deriva Semântica".

Pense nisso como uma "Tradução de Telefone Sem Fio":

O Colapso de Notação: É como se você estivesse tentando descrever um dragão detalhado, mas o tradutor, para facilitar, dissesse apenas "é um lagarto grande". O robô aceita a descrição (o lagarto existe!), mas você perdeu a magia e a complexidade do dragão (a física quântica).
A Elevação da Abstração: É como se você pedisse para alguém calcular a trajetória de um foguete, e o tradutor respondesse: "Bem, se o foguete subir, ele estará mais alto". A lógica está certa, mas a matemática complexa foi substituída por uma obviedade que não serve para nada na prática.

Por que isso é importante?

Se queremos que o futuro da ciência seja feito por IAs que ajudem a descobrir novas leis do universo, precisamos que elas não apenas "falem a língua dos robôs", mas que elas entendam o que os cientistas realmente querem dizer.

O FormalScience é o primeiro passo para garantir que, quando a máquina disser "Provado!", ela não esteja apenas provando uma obviedade, mas sim a verdadeira e complexa realidade da natureza.

Resumo Técnico: FormalScience: Autoformalização de Ciência com Geração de Código Agêntica em Lean

1. O Problema

A autoformalização — o processo de converter raciocínio matemático informal (como LaTeX) em código formalmente verificável (como Lean 4) — é um desafio crítico para Grandes Modelos de Linguagem (LLMs). O problema é intensificado em domínios científicos como a Física, devido a dois fatores principais:

Complexidade de Domínio: A necessidade de lidar com notações específicas (notação de Dirac, cálculo vetorial, operadores não comutativos) que os LLMs atuais não dominam nativamente.
Desvio Semântico (Semantic Drift): Existe um hiato entre o que o código formal consegue compilar e o que o enunciado físico realmente significa. Frequentemente, para que o código compile, o modelo "simplifica" a física, perdendo o rigor científico original (ex: transformar operadores quânticos em escalares comuns).

2. Metodologia

Os autores propõem o FormalScience, um pipeline agêntico human-in-the-loop (com intervenção humana) projetado para ser agnóstico ao domínio, mas aplicado aqui à física. A metodologia divide-se em:

Pipeline FormalScience (Algoritmo 1): Um processo de quatro estágios que utiliza especialistas humanos para validar o alinhamento semântico. O especialista atua como um classificador binário, garantindo que a formalização não apenas compile, mas preserve o significado.
Geração de Código Agêntica (Algoritmo 2): Para reduzir a dependência humana, propõem um sistema de agentes que utiliza:
1. Guarda de Superfície (Surface Guard): Rejeita códigos com tokens proibidos (como $\nabla$ ou $\partial$ , que o Lean não suporta nativamente) ou provas incompletas.
2. Categorização de Erros: Diferencia erros estruturais (sintaxe, módulos ausentes), que exigem regeneração total, de erros semânticos (incompatibilidade de tipos), que são corrigidos por um "agente de patch" usando unified diffs.
Criação do Dataset FormalPhysics: Utilizando o pipeline, os autores construíram um corpus de 200 problemas de nível universitário (Mecânica Quântica e Eletromagnetismo) com suas respectivas representações em LaTeX e Lean 4.

3. Principais Contribuições

FormalScience: Um framework escalável e de baixo custo para gerar conjuntos de dados formais de alta qualidade em qualquer domínio científico.
FormalPhysics: Um benchmark inédito que contém não apenas enunciados e provas informais, mas também provas formais completas (sem o uso excessivo de sorry), superando benchmarks existentes em complexidade e validade.
Taxonomia de Desvio Semântico: Uma caracterização sistemática de como a formalização falha, categorizando o erro em:
- Notational Collapse (Colapso Notacional): Redução de operadores complexos a escalares.
- Abstraction Elevation (Elevação de Abstração): Substituição de cálculos físicos por propriedades algébricas triviais.
- Proof Strategy Substitution (Substituição de Estratégia): Provar o objetivo usando um caminho matemático diferente do original.
- Implicit Premise Selection (Seleção de Premissas Implícitas): Identificação de pressupostos ocultos (o único desvio considerado benéfico).

4. Resultados

Desempenho de Modelos: O pipeline agêntico baseado em GPT-OSS-20B alcançou uma validade formal de 31%, superando significativamente as abordagens de zero-shot e self-refinement de modelos abertos.
Trade-off Alinhamento-Validade: Os resultados mostram que modelos que priorizam a compilação (validade formal) tendem a sacrificar a precisão científica (alinhamento semântico). Modelos como o Kimina-7B conseguem compilar, mas apresentam baixíssimos índices de preservação lógica.
Eficácia do FormalScience: O método com intervenção humana atingiu 100% de validade formal, provando ser uma ferramenta poderosa para a criação de dados de treinamento (fine-tuning) de alta fidelidade.

5. Significância

Este trabalho é fundamental para o avanço da IA para a Ciência. Ele demonstra que a simples compilação de código não é suficiente para garantir a verificação científica. Ao fornecer ferramentas para quantificar o "desvio semântico", o artigo abre caminho para o desenvolvimento de sistemas de IA que não apenas "escrevem código que funciona", mas que preservam o rigor e a profundidade do conhecimento científico durante a transição do informal para o formal.