- Terence Tao encontrou um erro pequeno, mas não trivial, em um artigo durante seu projeto de formalização em Lean4
- O erro apareceu em um argumento na página 6 do artigo arXiv
2310.05328, onde1/2 log((n - 1)/(n - k - 1))diverge emn = 3, k = 2 - O problema se limita a valores pequenos de
n; paran >= 8, o argumento original funciona, e os casos pequenos denpodem ser tratados diretamente com um método mais grosseiro - O Lean exigiu uma prova de
0 < n - 3, mas a única hipótese eran > 2, então a táticalinarithnão conseguiu obter a contradição necessária - Tao pretende corrigir o argumento ajustando algumas constantes numéricas e incluir uma nota de rodapé na nova versão dizendo que a imprecisão do argumento anterior foi descoberta durante a tentativa de formalização em Lean
Erro revelado pela formalização em Lean4
- Terence Tao descobriu um bug pequeno, mas não trivial, em um artigo durante seu projeto de formalização em Lean4
- O alvo da formalização era um argumento na página 6 do artigo arXiv
2310.05328 - A expressão problemática tinha a seguinte forma
1/2 log((n - 1)/(n - k - 1))
- Essa expressão diverge no caso
n = 3, k = 2
Escopo do erro e forma de correção
- Esse problema ocorre apenas para valores pequenos de
n- Para
n >= 8, o argumento em questão continua funcionando - Os casos pequenos de
npodem ser tratados diretamente com um método mais grosseiro, embora as constantes piorem
- Para
- Tao considera que pode corrigir o argumento trocando algumas constantes numéricas dessa página
- Na nova versão do artigo, ele pretende acrescentar uma nota de rodapé dizendo que o argumento anterior era ligeiramente impreciso e que isso foi descoberto ao tentar formalizá-lo em Lean
Ponto específico em que o Lean travou
- No ponto em que a formalização falhou, o Lean exigiu provar
0 < n - 3- A única hipótese disponível era
n > 2 - A tática
linarithnão conseguiu derivar uma contradição a partir da negação de0 < n - 3
- A única hipótese disponível era
1 comentários
Comentários do Hacker News
Ele começou a aprender Lean4 com a ajuda do GPT-4 no começo deste mês: https://mathstodon.xyz/@tao/111208692505811257
Muitos dos posts dele no Mastodon neste mês foram sobre o progresso do aprendizado, e é um caso interessante de como grandes modelos de linguagem podem acelerar até o trabalho de pessoas no mais alto nível
Curiosamente, se só pessoas muito qualificadas conseguirem usar bem essas ferramentas, isso pode aumentar ainda mais a desigualdade
Se você quiser conhecer Lean4 com mais facilidade, o Natural Number Game é ótimo: https://adam.math.hhu.de/#/g/hhu-adam/NNG4
Se preferir só ler, sem o jogo, veja aqui: https://lean-lang.org/theorem_proving_in_lean4/introduction.html
No começo eu tinha escrito Alloy como Allow
Alguns anos atrás, enquanto eu procurava uma forma de reduzir erros nos programas que escrevo, conheci o TLA+ do Lamport e aprendi a escrever especificações formais pensando no comportamento do programa como uma máquina de estados
O TLA+ me ajudou a entender claramente a abstração, e depois também descobri a série Software Foundations, que usa o assistente de provas Coq para criar software formalmente correto. Os exercícios são apresentados meio como um pequeno jogo, então foi bem divertido resolvê-los: https://softwarefoundations.cis.upenn.edu/
Especificações formais, que são uma abstração de alto nível, focam em uma linguagem dedicada para descrever o código, enquanto contratos de código, uma abstração de nível mais baixo, são mais próximos de substituir a lógica de validação por um modelo melhor. O C# já teve o Code Contracts[1], uma abordagem simples mas poderosa que verificava contratos em tempo de compilação com o solver SMT Z3[2], mas ele foi descontinuado alguns anos depois[3] e praticamente morreu ao ser removido do .NET Runtime. Hoje, a coisa mais próxima disso em C# provavelmente é o Dafny[4], e o lado do desenvolvimento em C# ainda continua pensando em como colocar isso diretamente na linguagem[5]
[1] https://www.microsoft.com/en-us/research/project/code-contracts/
[2] https://github.com/Z3Prover/z3
[3] https://github.com/microsoft/CodeContracts
[4] https://github.com/dafny-lang/dafny
[5] https://github.com/dotnet/csharplang/issues/105
O Idris2 parece oferecer um sistema de tipos mais avançado para prova de teoremas, ao mesmo tempo em que busca ser uma linguagem de uso geral: https://github.com/idris-lang/Idris2
Existe também um livro meio derivado que usa Agda em vez de Coq: https://plfa.github.io/
Ainda não consegui ler, mas já coloquei na lista, e acho que Agda ou Idris têm mais chance de parecer linguagens de programação do que Coq
Estou realmente animado com tipos dependentes. Só acho que isso ainda deve demorar para chegar
O Dependent Haskell está em andamento, mas dizem que é difícil encaixar isso depois em uma linguagem já existente, e o criador do Idris também disse que espera que o Idris sirva de modelo para outras linguagens, não que tenha adoção mainstream. Coq, Agda e F* também não foram projetadas como linguagens de uso geral. A implementação do compilador é complexa e a sintaxe pode ficar verbosa, mas o que eu quero é simplicidade. Quero codificar tudo o que sei sobre entradas e saídas. Hoje, em linguagens mainstream, muitas vezes sabemos mais sobre os argumentos ou sobre a saída do que o sistema de tipos consegue expressar
Seria ótimo ter uma abordagem gradual, como no TypeScript, em que não fosse preciso provar tudo em todos os lugares, mas ainda fosse possível adicionar restrições de valores no nível de tipos em pontos arbitrários
Por exemplo, se você sabe ao mesmo tempo uma lista de números e o seu comprimento, pode criar com tipos dependentes um tipo de lista que inclua explicitamente esse comprimento, e garantir em tempo de compilação que as operações preservem esse tamanho. Se você definir uma função que só aceita uma lista de comprimento 3 e passar uma de comprimento 4, isso não compila, então dá para capturar o erro antes da execução. É como uma camada extra de verificações de segurança que torna os tipos mais expressivos e permite codificar até relações complexas entre variáveis
Se uma das mentes mais brilhantes da nossa geração consegue ampliar o escopo do próprio trabalho com a combinação de modelos de linguagem de grande porte e prova automática, então o futuro dessa combinação de tecnologias parece muito promissor.
Começa com correção de bugs, depois ajuda na verificação e, no fim, provavelmente vai impulsionar novas descobertas e ampliar os limites. Precisamos de um termo para descrever o fenômeno em que dinâmicas como a Lei de Moore “infectam” áreas que originalmente não tinham esse tipo de característica cumulativa. Como contexto adicional, Terence Tao está usando o Copilot para aprender Lean: https://mathstodon.xyz/@tao/111271244206606941
Ele provavelmente conseguiria sem o Copilot, mas talvez nem tivesse começado por causa do atrito de adotar uma ferramenta nova. Modelos de linguagem de grande porte têm grande potencial nesse tipo de situação de “bicicleta para a mente”
Alguns anos atrás, também encontrei um bug em um post do blog de matemática de Terence Tao. Avisei, ele corrigiu e ainda me agradeceu.
Claro, isso não me levou à primeira página do Hacker News
Fiquei preocupado achando que Lean4 fosse outro modelo de linguagem de grande porte, mas na verdade era uma ferramenta bastante sólida e confiável
Fico imaginando se seria possível combinar verificadores formais de prova como o Lean proof checker com modelos de linguagem que geram pares sintéticos de conjectura e prova em uma linguagem formal como Lean
O Lean proof checker poderia verificar automaticamente se as provas sintéticas escritas pelo modelo de linguagem estão corretas, e essa informação poderia ser usada como sinal de recompensa de aprendizado por reforço a ser aplicado ao modelo original, levando-o a escrever provas melhores. Ou então provas sintéticas corretas de rodadas anteriores poderiam ser usadas como dados de treino para treinar um novo modelo. Também daria para tornar isso mais adversarial. Separar em um modelo de geração de conjecturas e um modelo de prova/refutação, e adicionar um modelo que preveja se a prova sintética será verificada pelo Lean proof checker. Quanto menor a probabilidade prevista de estar correta, maior a recompensa para o modelo gerador de provas quando ele de fato produzir uma prova correta. Por fim, se adicionar um modelo que preveja a recompensa que o modelo gerador de provas receberá para uma conjectura sintética específica, o modelo gerador de conjecturas será recompensado por criar conjecturas com alta recompensa esperada que não sejam difíceis nem fáceis demais para o modelo gerador de provas. O sistema inteiro poderia produzir provas sintéticas cada vez mais difíceis, e isso poderia levar a um autoaprendizado melhor do modelo gerador de provas. Em princípio, isso poderia escalar até capacidades sobre-humanas em geração de provas, sendo algo parecido com GANs ou com autojogo do AlphaGo Zero. A parte difícil é o bootstrapping inicial: o primeiro treinamento do modelo gerador exige dados de provas em Lean fornecidos por humanos. Mas, quando as provas sintéticas ficarem boas o bastante, o sistema poderá continuar seu autoaprendizado automaticamente
No fim, poderíamos ter um modelo que conhece todos os teoremas e todas as provas corretas da literatura matemática
Para as etapas iniciais de aprendizado supervisionado a partir de provas existentes e busca de novas provas, há TacticToe (https://arxiv.org/abs/1804.00596), Tactician (https://arxiv.org/pdf/2008.00120.pdf), CoqGym/ASTactic (https://arxiv.org/abs/1905.09381), Proverbot9001 (https://arxiv.org/abs/1907.07794), Diva (https://dl.acm.org/doi/10.1145/3510003.3510138#sec-terms). A maioria tem algum tipo de modelo de linguagem internamente, mas, se você estiver procurando grandes modelos de linguagem que receberam atenção recente, há GPT-f (https://arxiv.org/abs/2009.03393), Baldur (https://arxiv.org/abs/2303.04910) e COPRA (https://arxiv.org/abs/2310.04353). Ainda assim, por enquanto, esses modelos não parecem ser tão eficazes quanto ferramentas especializadas que não são LLMs. No lado de aprender por reforço para ir além de provas escritas por humanos, há TacticZero (https://openreview.net/forum?id=edmYVRkYZv), o artigo da OpenAI (https://arxiv.org/pdf/2202.01344.pdf), rlCoP (https://arxiv.org/abs/1805.07563), trabalhos da linha HOList (https://arxiv.org/pdf/1905.10006.pdf), HyperTree Proof Search (https://arxiv.org/abs/2205.11491), além de trabalhos em andamento da equipe da University of Massachusetts e meus
O contexto anterior sobre como Tao usou ferramentas de grandes modelos de linguagem, incluindo o GPT-4, nessa jornada está aqui: https://mathstodon.xyz/@tao/111233986893287137
Também é possível acompanhar o progresso dele no GitHub: https://github.com/teorth/symmetric_project/