LeanBET: Formally-verified surface area calculations in Lean

Este artigo apresenta o LeanBET, um pipeline de análise de área superficial Brunauer–Emmett–Teller (BET) totalmente executável e formalmente verificado, implementado em Lean 4, que garante a correção matemática ao mesmo tempo que alcança um acordo numérico quase perfeito com a implementação de referência BETSI estabelecida.

O essencial

Imagine que você está tentando medir a área superficial de uma esponja, mas a esponja é feita de buracos invisíveis e microscópicos. Cientistas usam um método chamado BET (nomeado em homenagem a três cientistas) para estimar essa área observando como um gás adere à esponja. É uma ferramenta padrão na química, mas é um pouco como tentar resolver um quebra-cabeça onde a imagem na caixa está borrada.

Aqui está o problema: Para obter a resposta, os cientistas precisam escolher uma faixa específica de pontos de dados de seu experimento e traçar uma linha reta através deles. O problema é que pessoas diferentes (ou programas de computador diferentes) podem escolher faixas ligeiramente distintas. Uma pessoa pode dizer: "Vamos usar os 10 pontos do meio", enquanto outra diz: "Não, use os 12 pontos do meio". Isso leva a respostas diferentes para a mesma esponja, causando confusão e falta de confiança nos resultados.

Para corrigir isso, uma equipe criou um programa de computador chamado BETSI que verifica automaticamente todas as faixas possíveis de dados para encontrar a "melhor". É como ter um robô que tenta todas as combinações possíveis de peças de quebra-cabeça para encontrar aquela que se encaixa perfeitamente. No entanto, mesmo robôs podem ter bugs, ou pressupostos ocultos que os tornam errados de maneiras sutis.

Aparece o "LeanBET": O Robô Comprovação-Matemática

Os autores deste artigo construíram uma nova versão desse robô usando uma ferramenta especial de computador chamada Lean 4. Pense no Lean 4 não apenas como uma linguagem de programação, mas como um professor de matemática super rigoroso que nunca permite que você cometa um erro sem prova.

Veja como eles fizeram isso, usando algumas analogias simples:

1. O Sistema de "Dois Cérebros" (Polimorfismo)

Normalmente, quando você escreve um programa de computador, usa "números de ponto flutuante" (como os números em uma calculadora). Estes são rápidos, mas ligeiramente bagunçados porque os computadores não podem manter precisão infinita. Quando você faz provas matemáticas, usa "números reais" (perfeitos, precisão infinita), mas não pode executá-los em um computador.

Os autores resolveram isso construindo um robô que muda de forma.

• Cérebro A (A Prova): Quando precisam provar que a matemática está correta, o robô veste um traje de "Número Real". Ele faz matemática perfeita e teórica para provar que a lógica é impecável.
• Cérebro B (A Execução): Quando precisam executar o programa em dados reais, o robô troca para um traje de "Ponto Flutuante". Ele roda rápido em computadores reais.
• A Magia: Como o robô é construído da mesma maneira em ambos os trajes, se o "Cérebro da Prova" diz que a lógica é perfeita, o "Cérebro de Execução" é garantido de seguir as mesmas regras. É como provar que o projeto de uma ponte é seguro com matemática perfeita e, em seguida, construir a ponte real com aço verdadeiro, sabendo que o projeto se sustenta.

2. A "Receita vs. O Cozimento" (Derivação como Especificação)

Na ciência normal, você escreve uma receita (a teoria matemática) no papel, e depois um chef (o programador) tenta cozinhar na cozinha (o software). Às vezes, o chef adiciona uma pitada de sal aqui ou ali, ou entende mal uma etapa, e o prato fica com um sabor diferente da receita.

No LeanBET, a receita e o cozimento acontecem na mesma sala. A "derivação matemática" (a receita) é escrita diretamente no código. O computador verifica que o código é a receita. Se o código diz "adicione sal", a prova matemática verifica que "adicionar sal" é exatamente o que a teoria exige. Não há lacuna entre a teoria e a prática.

3. O "Inspetor Rigoroso" (Verificação Formal)

O artigo afirma que seu programa não apenas adivinha a resposta; ele carrega consigo um certificado de correção.

• Software Padrão: Você executa o programa, ele lhe dá um número, e você espera que esteja certo.
• LeanBET: Você executa o programa, ele lhe dá um número, e também entrega um documento matematicamente provado dizendo: "Verifiquei cada etapa, segui todas as regras, e este número é a única resposta correta com base nos dados que você me forneceu".

O Que Eles Encontraram?

Eles testaram seu novo "Robô Comprovação-Matemática" contra o antigo "Robô Padrão" (BETSI) usando 19 conjuntos diferentes de dados (como 19 esponjas diferentes).

• O Resultado: Para 18 das 19 esponjas, os dois robôs deram a resposta exata até o menor ponto decimal.
• O Único Glitch: Para uma esponja (chamada UiO-66), houve uma diferença minúscula (0,03%). Os autores admitem que ainda não sabem o motivo, mas é um erro muito pequeno comparado ao ruído usual nos experimentos.

A Conclusão

Este artigo não trata de inventar uma nova maneira de medir esponjas. Trata-se de construir uma versão confiável da maneira existente. Eles pegaram uma ferramenta científica padrão, reconstruíram-na dentro de um ambiente de "prova matemática" e mostraram que funciona tão bem quanto as ferramentas antigas, mas com a garantia de que não cometeu nenhum erro lógico.

É como fazer um upgrade de um mapa comum para um GPS que não apenas lhe diz a rota, mas também prova, passo a passo, que a rota é a mais curta e segura possível, sem desvios ocultos.

Resumo técnico

Resumo Técnico de "LeanBET: Cálculos de área superficial formalmente verificados em Lean"

Declaração do Problema
O método Brunauer–Emmett–Teller (BET) é o quadro padrão para estimar a área superficial específica a partir de isotermas de adsorção de gases. No entanto, a implementação prática envolve subjetividade significativa, particularmente na seleção da faixa de pressão relativa para regressão linear. Embora existam critérios de consistência (critérios de Rouquerol) para filtrar regiões válidas, múltiplos intervalos de pressão frequentemente satisfazem essas regras, levando a variabilidade nas áreas superficiais relatadas entre diferentes laboratórios e implementações de software. Esforços anteriores para padronizar esse processo, como o algoritmo de Identificação de Superfície BET (BETSI), dependem de software numérico de propósito geral (Python). Embora o BETSI reduza a subjetividade através da enumeração exaustiva, permanece um algoritmo numérico no qual suposições ocultas de implementação ou erros sutis não podem ser formalmente descartados, deixando as garantias científicas da saída não verificadas.

Metodologia
Os autores apresentam LeanBET, um pipeline de análise BET totalmente executável e formalmente verificado implementado no prova de teoremas Lean 4. A abordagem integra código executável com provas matemáticas em um único ambiente, utilizando um design numérico polimórfico para fechar a lacuna entre computação e verificação:

• Polimorfismo: O algoritmo é escrito usando um tipo genérico α restringido por uma classe de tipos BETLike. Isso permite que a mesma estrutura de código seja instanciada sobre números de ponto flutuante (Float) para execução eficiente em dados experimentais reais e sobre números reais (Real) para provas matemáticas não computáveis.
• Derivação como Especificação: A derivação algébrica da equação BET linearizada não é meramente uma motivação, mas serve como especificação formal. O código é construído para espelhar essa derivação, garantindo que a transformação executável corresponda ao modelo teórico.
• Fluxo de Trabalho: O pipeline executa as seguintes etapas, cada uma acompanhada de uma prova formal:
  1. Enumeração de Janelas: Gera sistematicamente todas as sublistas contíguas da isoterma contendo pelo menos dois pontos de dados.
  2. Linearização: Transforma pontos de dados $(p, n)$ na forma BET linearizada $p/[n(1-p)]$.
  3. Regressão Linear: Realiza regressão de mínimos quadrados em cada janela para extrair inclinação, intercepto e $R^2$.
  4. Verificações de Admissibilidade: Filtra candidatos com base nos critérios de Rouquerol (monotonicidade de $n(1-p)$, positividade dos parâmetros $C$ e $n_m$, e consistência da pressão de monocamada).
  5. Seleção de Joelho: Resolve empates entre janelas válidas selecionando aquela com o maior índice final, quebrando empates adicionais com o menor erro percentual.

Principais Contribuições

1. Verificação Formal do Pipeline BETSI: O artigo fornece a primeira implementação verificada por máquina do fluxo de trabalho completo do BETSI. Prova que o código executável satisfaz as definições matemáticas da teoria BET e os critérios de seleção específicos.
2. Provas de Corretude e Completude: Os autores provam formalmente:
   • Teorema A.1 & A.2: A equação da isoterma BET é derivada das suposições do modelo de camadas, e a etapa de linearização é algebricamente correta.
   • Teorema A.3: A enumeração de janelas é correta (apenas janelas válidas são geradas) e completa (nenhuma janela contígua válida é perdida).
   • Teorema A.4 & A.5: A etapa de regressão retorna um verdadeiro minimizador de mínimos quadrados, e os parâmetros físicos extraídos ($n_m$, $C$) concordam com suas definições teóricas.
   • Teorema A.6 & A.7: As verificações de admissibilidade e a estratégia de seleção baseada em joelho satisfazem estritamente suas especificações formais.
3. Implementação Polimórfica: O trabalho demonstra um padrão prático para computação científica em Lean, onde a corretude é provada sobre números reais idealizados enquanto a execução ocorre sobre aritmética de ponto flutuante, evitando a necessidade de linguagens de verificação separadas.

Resultados
A implementação LeanBET foi avaliada contra a implementação de referência baseada em Python do BETSI usando um conjunto de benchmark de 19 isotermas de adsorção.

• Acordo Numérico: O LeanBET concorda com a referência BETSI com precisão de máquina para 18 das 19 isotermas.
• Discrepância: Para o conjunto de dados UiO-66, foi observada uma desvio de aproximadamente 0,03% (0,36 m²/g). Os autores observam que a causa desse desvio específico permanece indeterminada, mas enfatizam que é significativamente menor que as incertezas experimentais típicas.
• Status de Verificação: Todas as provas foram compiladas com sucesso, fornecendo garantias verificadas por máquina de que a saída do algoritmo adere às restrições matemáticas especificadas.

Significado
O artigo afirma que o LeanBET demonstra que um fluxo de trabalho prático de computação científica pode ser construído em um prova de teoremas sem sacrificar o acordo numérico com implementações de referência estabelecidas. A contribuição principal não é um novo algoritmo, mas uma garantia formalmente verificada de corretude. Ao vincular o pipeline executável a declarações matemáticas verificadas por máquina, o trabalho aborda a crise de reprodutibilidade na análise BET, eliminando ambiguidades quanto à aderência da implementação à teoria subjacente e aos critérios de seleção. Os autores posicionam isso como um passo para fechar a lacuna entre derivações teóricas e implementações de software na ciência dos materiais.