🤖 AI

PriorProof: A Point-in-Time Measure of Technique Novelty for Formal Proofs

O artigo apresenta o PriorProof, um método automatizado e livre de ontologia para quantificar a novidade de técnicas de prova formal em Lean ao medir o surprisal de suas pegadas de dependência contra um prior ancorado no tempo, demonstrando uma concordância moderada com especialistas humanos e servindo como um sinal decomponível e interpretável, em vez de um substituto para o julgamento de especialistas.

Autores originais: Neel Somani

Publicado 2026-07-21

📖 8 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Neel Somani

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ê está caminhando por uma biblioteca massiva e em constante expansão de ideias matemáticas. Nesta biblioteca, cada novo livro (uma prova) deve citar os livros mais antigos que utilizou para construir seus argumentos. Geralmente, quando um matemático escreve uma nova prova, ele tenta usar as ferramentas mais comuns e consagradas disponíveis naquele momento. Mas, às vezes, eles tomam um caminho selvagem e inesperado, usando uma combinação estranha de ferramentas antigas que ninguém pensou em misturar antes. A grande questão é: como sabemos, apenas olhando para a lista de livros que eles usaram, se o caminho deles foi verdadeiramente surpreendente ou apenas um desvio rotineiro? Este é o enigma da "novidade" na matemática formal. Enquanto os humanos podem discutir se uma prova é "elegante" ou "original", os computadores lutam com esses sentimentos vagos. Eles precisam de uma forma mecânica e rígida de medir se uma prova seguiu uma rota que era improvável de acontecer dado o que se sabia na época. É aqui que entra a ideia de "surpresa" — pense nisso como uma medida de quanto uma prova faz a biblioteca dizer: "Espere, eu não esperava que você usasse essa ferramenta específica para este trabalho!"

Entra o PriorProof, uma nova ferramenta projetada para agir como um bibliotecário que viaja no tempo. Em vez de perguntar a um humano: "Esta prova foi inteligente?", o PriorProof faz uma pergunta fria e direta: "Se congelássemos a biblioteca no exato momento em que esta prova foi escrita, quão surpreendente seria a lista de ferramentas utilizadas?" Os pesquisadores construíram um sistema que analisa uma prova formal (escrita em uma linguagem chamada Lean), remove a formatação rebuscada e cria uma "impressão digital" da maquinaria matemática específica utilizada. Então, ele volta no tempo para um instantâneo da biblioteca de antes da existência dessa prova. Ele pergunta: "Com base em outras provas com objetivos semelhantes daquele período anterior, quão provável era que alguém usasse estas ferramentas específicas?" Se a resposta for "muito improvável", a prova recebe uma alta "pontuação de novidade". O estudo descobriu que este escore mecânico frequentemente concorda com especialistas humanos sobre quais provas seguiram o caminho mais incomum, especialmente quando a diferença entre as pontuações é grande. No entanto, os autores são cuidadosos ao dizer que isso não é uma varinha mágica que resolve tudo; é um sinal útil que funciona melhor quando a diferença entre dois processos é óbvia, e não mede a "beleza" ou a "importância" da matemática, apenas o quão inesperada foi a rota.

O Bibliotecário Viajante no Tempo

Imagine que você é um detetive tentando descobrir se um ladrão usou um método secreto e nunca antes visto para abrir um cofre. Você não pode perguntar ao ladrão o que ele estava pensando, mas pode olhar para as ferramentas que ele deixou para trás. O PriorProof é esse detetive, mas para provas matemáticas. Ele não se importa com o motivo do ladrão ou o quão legal o assalto pareceu; ele só se importa com as ferramentas (as constantes e lemas matemáticos) usadas para resolver o problema e se essas ferramentas foram uma escolha estranha para aquele período de tempo.

Aqui está como o truque de mágica funciona, passo a passo:

A Impressão Digital: Quando um matemático escreve uma prova em Lean (uma linguagem de computador para matemática), o computador a transforma em uma lista longa e detalhada de cada ferramenta que ela utilizou. O PriorProof pega essa lista e a limpa, agrupando ferramentas semelhantes em "famílias" (como agrupar todos os martelos juntos, ou todas as chaves de fenda). Esta é a "impressão digital".
A Máquina do Tempo: O sistema então viaja no tempo. Ele captura um instantâneo de toda a biblioteca matemática de antes da prova ter sido escrita. Ele olha para todas as outras provas escritas naquela época que tentavam resolver problemas semelhantes.
A Previsão: Usando um modelo de computador inteligente (um modelo de linguagem), ele prevê: "Se eu estivesse escrevendo uma prova para este problema naquela época, quais ferramentas eu provavelmente usaria?" Ele constrói uma expectativa "a priori", como uma previsão do tempo para ferramentas matemáticas.
A Pontuação de Surpresa: Finalmente, ele compara as ferramentas reais usadas na nova prova contra a previsão. Se a prova usou ferramentas que a previsão disse serem muito improváveis (baixa probabilidade), o sistema atribui a ela uma alta pontuação de "surpresa". Uma pontuação alta significa: "Uau, esse foi um caminho estranho de se tomar!"

O Que o Detetive Descobriu

Os pesquisadores testaram este sistema em uma seção específica da biblioteca matemática chamada Topologia (que lida com formas e espaços). Eles não apenas adivinharam; eles configuraram um teste cego. Eles pegaram 100 pares de provas e as mostraram a três especialistas em matemática. Os especialistas tiveram que escolher qual prova em cada par seguiu o caminho "menos padrão" (mais surpreendente). Eles não viram as pontuações; apenas usaram seus cérebros.

Então, eles compararam as escolhas dos especialistas humanos com o que o PriorProof previu. Aqui está o resultado:

De 76 pares únicos de provas (alguns foram mostrados múltiplas vezes para verificar a consistência), o PriorProof concordou com a maioria dos especialistas humanos em 53 deles. Isso é cerca de 69,7%.
Para os 12 pares que foram especificamente escolhidos por serem exemplos "clássicos" de provas surpreendentes versus padrões, o PriorProof acertou 11 vezes (cerca de 91,7%).
Para os outros 64 pares, que eram um pouco mais complicados, ele acertou 42 (cerca de 65,6%).

Os autores também observaram a "lacuna de pontuação" — a diferença entre a pontuação de surpresa das duas provas em um par. Eles encontraram um padrão nítido: quando a lacuna era enorme (significando que uma prova era muito mais surpreendente que a outra), o sistema era muito confiável, concordando com os humanos 84,2% das vezes. Mas quando a lacuna era pequena (as duas provas eram de forma semelhante surpreendentes), o sistema era menos seguro, concordando apenas 63,2% das vezes. Isso sugere que a ferramenta é ótima para detectar as "grandes surpresas", mas torna-se imprecisa quando as diferenças são sutis.

O Que Ele NÃO É (e o que ele descarta)

É crucial entender o que o PriorProof não está alegando ser. Os autores são muito claros sobre isso:

Não é uma medida de "Originalidade" ou "Gênio": Uma pontuação alta não significa que o matemático era um gênio. Significa apenas que ele usou uma combinação estranha de ferramentas. Às vezes, um caminho estranho é apenas um desvio desajeitado, não um insight brilhante.
Não é uma medida de "Importância": Uma prova pode ser incrivelmente importante para o mundo da matemática, mas usar ferramentas muito padrão e entediantes. O PriorProof daria a ela uma pontuação baixa, mesmo que ela mudasse a história.
Não é um "Detector de Plágio": O sistema não se importa se alguém copiou uma prova. Ele só se importa com a probabilidade estatística das ferramentas usadas.
Não é um Juiz "Perfeito": Os autores afirmam explicitamente que seu método não é um "problema resolvido". De fato, quando compararam o PriorProof com um modelo de linguagem de IA poderoso (GPT-5-mini), a IA concordou com os especialistas humanos com mais frequência (cerca de 78,9% contra 69,7%). No entanto, a diferença não foi estatisticamente significativa o suficiente para dizer que um era definitivamente melhor que o outro. O real valor do PriorProof não é vencer a IA, mas sim ser transparente. Você pode olhar para a pontuação e ver exatamente qual ferramenta causou a surpresa, enquanto a IA é uma "caixa preta" que apenas fornece uma resposta.

A Conclusão

O PriorProof é uma nova forma mecânica de medir o quão "não padrão" é uma prova matemática, observando o quão surpreendentes foram suas escolhas de ferramentas na época em que foi escrita. Ele funciona bem o suficiente para concordar com especialistas humanos cerca de dois terços do tempo, e torna-se ainda melhor quando a diferença entre duas provas é óbvia. Ele não nos diz se uma prova é bela, importante ou brilhante, mas nos dá um sinal confiável e datado que diz: "Ei, este caminho foi inesperado". É uma ferramenta para pesquisadores encontrarem casos interessantes para estudar, não um juiz final da grandeza matemática. Os autores sugerem que, no futuro, poderemos usar isso para ajudar a identificar provas geradas por máquinas interessantes ou para estudar como as bibliotecas matemáticas evoluem, mas, por enquanto, é apenas uma maneira muito inteligente e muito específica de medir a surpresa.

Resumo Técnico: PriorProof

Declaração do Problema

Bibliotecas de provas formais, como a Mathlib do Lean, oferecem um registro único do desenvolvimento matemático: o termo de prova elaborado lista explicitamente as constantes utilizadas, e o controle de versão identifica exatamente quais declarações existiam no momento da escrita. Isso permite uma investigação mecânica sobre a não-padronização da rota de prova relativa ao tempo: determinar o quão "surpreendente" ou não padronizada foi a rota de uma prova em relação às técnicas disponíveis quando ela foi escrita.

Enquanto as avaliações existentes de provadores de teoremas aprendidos focam em se um teorema foi provado, o custo de busca ou a transferibilidade, elas não medem diretamente se uma prova bem-sucedida segue uma rota que a biblioteca anterior teria tornado provável. Filósofos e matemáticos há muito analisam virtudes da prova como explicação, pureza e elegância, mas estas são difíceis de operacionalizar mecanicamente. O PriorProof aborda um constructo mais estreito: novidade de rota, definida como o desvio da pegada de dependência de uma prova em relação à distribuição esperada de dependências para enunciados similares no estado anterior da biblioteca.

Metodologia

O PriorProof é uma medida trimestral, baseada em pontos no tempo, para provas de Lean 4/Mathlib. O pipeline opera sobre uma declaração de teorema $D$ escrita no tempo $t$ através de três estágios primários:

1. Extração da Pegada de Dependência

O sistema extrai uma "pegada de família de dependências" ponderada do termo de prova elaborado $p_D$ :

Extração: Utiliza o getUsedConstants do Lean para identificar constantes de fato referenciadas pelo termo da prova, excluindo meros imports de arquivos.
Filtragem: Um filtro determinístico remove recursores gerados, coerções, burocracia de typeclass plumbing e boilerplate de táticas.
Travessia de Fronteira: As dependências são recursivamente substituídas por dependências mais antigas nas quais elas se baseiam até que a travessia atinja declarações estabelecidas na captura da biblioteca antes de $t$ . O estabelecimento é definido por um limiar de contagem de reuso pré-bin para evitar que declarações introduzidas conjuntamente apareçam como estabelecidas.
Recuo de Família (Family Backoff): Cada constante sobrevivente mapeia para a "família de dependência" mais fina (namespace, módulo ou área da biblioteca) com pelo menos cinco ocorrências pré-bin. Isso reduz a novidade acidental de nomes raros sem exigir uma ontologia construída à mão.
Resultado: Um conjunto ponderado $\Phi_t(D) = \{(f_i, w_i)\}$ representando as famílias de dependência observadas.

2. Construção de Prior Condicionada ao Enunciado

Para determinar o que era "esperado", o sistema recupera enunciados de teoremas similares de uma captura da biblioteca estritamente anterior ao trimestre do alvo ( $L_{<b(t)}$ ):

Recuperação: Um codificador de sentence-transformer (ajustado via contraste de pares pré-bin) recupera os $k=32$ vizinhos mais próximos baseados em similaridade de cosseno.
Suavização: Um prior suavizado hierarquicamente $q_t(f|D)$ $q_{t} (f ∣ D)$ é construído como uma mistura das distribuições empíricas de famílias de:
- Vizinhos recuperados ( $q_{r,t}$ )
- Namespace do alvo ( $q_{n,t}$ )
- Módulo do alvo ( $q_{m,t}$ )
- A biblioteca pré-bin completa ( $q_{g,t}$ )
Otimização: Os pesos da mistura e os parâmetros de suavização são selecionados maximizando a log-verossimilhança cronológica das famílias observadas em provas anteriores, garantindo que o prior seja preditivo em vez de ajustado ao estudo humano.

3. Pontuação

O score PriorProof $S_t(D)$ é a surprisal ponderada da pegada observada sob o prior construído:
$S_t(D) = \sum_{i=1}^{m_D} w_i [-\log q_t(f_i | D)]$
Um score alto indica que a prova utiliza famílias de dependência que eram improváveis para teoremas anteriores com enunciados similares. Para comparações pareadas, a métrica seleciona a prova com o score mais alto, usando a diferença absoluta de score $\Delta(A, B)$ como um sinal de confiança interna.

Contribuições Principais

Definição Mecânica: Uma definição de não-padronização da rota de prova relativa ao tempo como surprisal da pegada de dependência, que não requer uma ontologia de técnica construída à mão ou rótulos humanos.
Disciplina Temporal: Uma disciplina rigorosa de vazamento (leakage) onde a recuperação, o suporte de família, a contagem de reuso e o ajuste fino do codificador são estritamente restritos aos dados pré-bin.
Estudo Empírico: Um estudo cego sobre a topologia da Mathlib envolvendo validação mecânica, uma comparação de três avaliadores e um baseline de modelo de linguagem.
Evidência de Calibração de Extremidade: Evidência empírica de que a diferença absoluta de score serve como um candidato indicador de confiabilidade, onde lacunas maiores correlacionam-se com maior concordância com avaliadores humanos, embora a relação não seja uma escada monotônica resolvida.

Resultados

O estudo avaliou 100 apresentações cegas (colapsando para 76 pares de provas subjacentes distintos) contra três avaliadores de domínio retidos e baselines de modelos de linguagem (gpt-5/gpt-5-mini).

Concordância com Avaliadores: O PriorProof concordou com a maioria de três avaliadores em 53/76 pares (69,7%).
- Pares Canônicos: 11/12 (91,7%) em 12 contrastes canônicos selecionados à mão.
- Pares Estratificados: 42/64 (65,6%) no conjunto mais amplo.
Baseline de Modelo de Linguagem: A melhor condição de modelo de linguagem concordou em 60/76 pares (78,9%). Um teste de McNemar comparando o PriorProof e o modelo resultou em $p=0,210$ , indicando que a diferença não está estatisticamente estabelecida com este tamanho de amostra.
Calibração de Gap de Score:
- No menor bin de gap de score, a concordância foi de 12/19 (63,2%), estatisticamente compatível com o acaso.
- No maior bin de gap de score, a concordância foi de 16/19 (84,2%).
- Os bins intermediários foram não-monótonos e os intervalos de confiança eram amplos. O artigo conclui que isso apoia uma tendência de calibração de extremidade (gaps altos são mais confiáveis) em vez de uma curva de calibração universal resolvida.
Validação Mecânica: As pegadas observadas receberam probabilidade cronológica significativamente maior do que alternativas aleatórias. Estudos de ablação confirmaram que os componentes de recuperação e suavização contribuem significativamente para o score, enquanto verificações de redundância não encontraram "hits" vivos no corpus curado (embora o caminho aninhado estivesse inativo devido a limitações de backend).

Significância e Alegações

O artigo apresenta o PriorProof não como um substituto para o julgamento de especialistas ou modelos, nem como uma teoria completa da novidade matemática. Em vez disso, ele é posicionado como um sinal decomponível e ancorado no tempo.

Escopo: A métrica visa especificamente se uma rota de prova utiliza maquinaria prévia inesperadamente distribuída. Ela é cega à novidade definicional, valor explicativo, elegância ou crédito de autoria.
Indicador de Confiabilidade: A principal utilidade identificada é o gap de score. Os resultados sugerem que quando o gap de score entre duas provas é grande, a preferência da métrica tem maior probabilidade de alinhar-se com o julgamento humano. Quando o gap é pequeno, a métrica é menos confiável.
Limitações: Os autores observam explicitamente que a métrica pode ser manipulada pela adição de maquinaria rara irrelevante, e que a implementação atual carece de normalização consciente de subtermos (detecção de redundância aninhada está inativa). O escopo estatístico é limitado a um domínio matemático (topologia) e um tamanho de amostra específico.
Utilidade Futura: A métrica destina-se a ser um instrumento de pesquisa para analisar provas formais verificadas, priorizando casos para revisão por especialistas e estudando provas geradas por máquinas para ver se elas reproduzem padrões esperados ou descobrem rotas que merecem atenção humana. É um gerador de hipóteses, não um árbitro de originalidade.