Gêmeo digital ambiental determinístico: onde a IA ajuda e onde o cálculo decide

Quem trabalha com áreas contaminadas, plumas de dispersão ou séries de monitoramento conhece o problema: os dados são poucos, as séries têm ruído e o transporte de um contaminante no solo e na água subterrânea depende de equações que não perdoam atalho. É nesse terreno que muita gente tem experimentado modelos de linguagem.

O risco é conhecido. Um modelo de linguagem pode inventar uma taxa de atenuação, um coeficiente de permeabilidade ou um caminho de fluxo que não existe, e escrever tudo com a mesma fluência com que escreve o que é verdade. O texto convence, e ninguém consegue dizer de onde o número saiu.

O que a verificação formal ensina

Em 26 de outubro de 2026, a OpenAI anunciou que modelos internos produziram uma proposta de refutação da Hipótese do Tempo Exponencial, uma conjectura do fim dos anos 1990 sobre o problema lógico 3-SAT, com a prova formalizada no Lean, um assistente de provas matemáticas. A revisão independente por especialistas ainda está em curso, e o ganho anunciado é teórico, sem efeito prático imediato.

O que interessa aqui é o método, que vale com ou sem a confirmação desse resultado. O Lean não se impressiona com uma frase bem escrita: cada passo da prova é conferido por uma máquina, e o passo que não fecha é recusado. A IA propõe, e a máquina de verificação aceita ou recusa. Mesmo assim, o Lean confirma apenas o enunciado que foi escrito para ele, e ainda cabe a pessoas conferir se esse enunciado diz o que se queria provar.

Um gêmeo digital ambiental precisa da mesma disciplina. Concentração, balanço de massa e comparação com valores de referência não podem ser adivinhados por um texto. Precisam sair de dados identificados e de cálculos que dão sempre o mesmo resultado para a mesma entrada.

Como o ecbyts separa as funções

O ecbyts funciona como um modelo de mundo do empreendimento: um único modelo em que cada elemento, seja um ponto de monitoramento, uma pluma, uma área ou um contrato, tem dado e origem. O 3D é uma das vistas, ao lado de mapa, tabela, gráfico, linha do tempo e relatório.

Os dados entram como observações com parâmetro, unidade, data, campanha e o ponto de monitoramento onde foram medidos. Nenhuma IA participa dessa entrada.

O cálculo é determinístico. Interpolação, comparação com o conjunto de valores de referência escolhido para o modelo, custos e indicadores são funções do próprio app: a mesma entrada produz o mesmo resultado, hoje e daqui a um ano. A IA não faz conta no lugar do motor.

A IA entra como tradutora. Na barra de comandos, você escreve o que quer em linguagem natural, como adicionar um ponto de monitoramento ou mostrar as observações de benzeno, e o assistente escolhe entre as ações que o app já tem. Ele não cria ação nova nem escreve direto no modelo. O padrão é perguntar: só uma lista curta de ações consideradas seguras roda sem confirmação. Nas demais, o cartão de confirmação mostra o que de fato será gravado, com o elemento, o parâmetro e o valor resolvidos no modelo aberto, e avisa quando o texto da IA cita um número que não aparece no que vai ser gravado. Antes de qualquer envio ao provedor de IA, nomes e identificadores dos pontos são trocados por descrições genéricas.

Fica o rastro. Cada alteração feita pela IA é registrada com o modelo usado, a ação e um resumo verificável dos parâmetros, numa trilha de auditoria em que só se acrescenta. Ao exportar a chave .ecbt do modelo, o app emite o Selo ECBYTS, uma autodeclaração de quem responde pelo modelo, com link de verificação. Quem recebe a chave confere que está olhando o mesmo modelo que foi declarado.

O que ainda não fazemos

O ecbyts não prova teoremas sobre o seu modelo. As regras de conformidade são cálculos testados, não provas formais em Lean, e a responsabilidade técnica continua com as pessoas que revisam e assinam. A verificação formal indica uma direção que nos parece certa: quanto mais regras críticas puderem ser escritas de modo que uma máquina as confira, menos espaço sobra para o número sem origem.

O que muda na prática

Para a engenharia ambiental e geotécnica, o caminho sugere sair de planilhas estáticas e relatórios fechados para um modelo que guarda a origem de cada número e mostra quando algo mudou, quem mudou e com qual ferramenta.

Para quem desenvolve software de monitoramento, a regra é simples de dizer e trabalhosa de cumprir: a IA serve para entender o pedido e orquestrar o que já existe, e o núcleo que calcula precisa continuar determinístico, auditável e ligado aos dados medidos.

Para ver a barra de comandos em uso, abra o tour Comandos em Linguagem Natural. Os demais tours de IA estão em Tours de inteligência artificial.