Ir para o conteúdo

Raciocínio automatizado

Origem: Wikipédia, a enciclopédia livre.

Em ciência da computação, particularmente em representação do conhecimento e raciocínio e metalógica, a área de raciocínio automatizado dedica-se a compreender diferentes aspectos do raciocínio. O estudo do raciocínio automatizado ajuda a produzir programas de computador que permitem que computadores raciocinem completa, ou quase completamente, de forma automática. Embora o raciocínio automatizado seja considerado um subcampo da inteligência artificial, também possui conexões com a ciência da computação teórica e a filosofia.

As subáreas mais desenvolvidas do raciocínio automatizado são a demonstração automatizada de teoremas (e o subcampo menos automatizado, porém mais pragmático, da demonstração interativa de teoremas) e a verificação automatizada de provas (vista como raciocínio garantidamente correto sob premissas fixas). Trabalho extensivo também foi realizado em raciocínio por analogia usando indução e abdução.[1]

Outros tópicos importantes incluem o raciocínio sob incerteza e o raciocínio não monotônico. Uma parte importante do campo da incerteza é a argumentação, onde restrições adicionais de minimalidade e consistência são aplicadas sobre a dedução automática mais padrão. O sistema OSCAR de John Pollock é um exemplo de sistema de argumentação automatizado que é mais específico do que ser apenas um provador automatizado de teoremas.

Ferramentas e técnicas de raciocínio automatizado incluem as lógicas e cálculos clássicos, lógica fuzzy, inferência bayesiana, raciocínio com entropia máxima e muitas técnicas ad hoc menos formais.

Na década de 2020, para melhorar a capacidade dos modelos de linguagem de grande escala de resolver problemas complexos, pesquisadores de IA criaram modelos de linguagem de raciocínio que podem gastar mais tempo no problema antes de gerar uma resposta[2] e arquiteturas neuro-simbólicas que usam sistemas de raciocínio simbólicos para prevenir alucinações.[3][4][5]

Primeiros anos

[editar | editar código]

O desenvolvimento da lógica formal desempenhou um grande papel no campo do raciocínio automatizado, que por sua vez levou ao desenvolvimento da inteligência artificial. Uma prova formal é uma prova na qual cada inferência lógica foi verificada até os axiomas fundamentais da matemática. Todas as etapas lógicas intermediárias são fornecidas, sem exceção. Nenhum apelo é feito à intuição, mesmo que a tradução da intuição para a lógica seja rotineira. Assim, uma prova formal é menos intuitiva e menos suscetível a erros lógicos.[6]

Alguns consideram o encontro de verão de Cornell em 1957, que reuniu muitos lógicos e cientistas da computação, como a origem do raciocínio automatizado, ou da dedução automatizada.[7] Outros dizem que começou antes disso com o programa Logic Theorist de 1955 de Newell, Shaw e Simon, ou com a implementação de 1954 por Martin Davis do procedimento de decisão de Presburger (que provou que a soma de dois números pares é par).[8]

O raciocínio automatizado, embora uma área de pesquisa significativa e popular, passou por um "inverno da IA" nos anos oitenta e início dos anos noventa. O campo subsequentemente se recuperou, no entanto. Por exemplo, em 2005, a Microsoft começou a usar tecnologia de verificação em muitos de seus projetos internos e planeja incluir uma linguagem de especificação e verificação lógica em sua versão de 2012 do Visual C.[7]

Contribuições significativas

[editar | editar código]

Principia Mathematica foi um trabalho marcante na lógica formal escrito por Alfred North Whitehead e Bertrand Russell. Seu propósito era derivar todas ou algumas das expressões matemáticas, em termos de lógica simbólica. Principia Mathematica foi inicialmente publicada em três volumes em 1910, 1912 e 1913.[9] Sucedeu The Principles of Mathematics, um livro de 1903 de Bertrand Russell, no qual Russell apresentou seu famoso paradoxo e argumentou sua tese de que matemática e lógica são idênticas.

Logic Theorist (LT) foi o primeiro programa desenvolvido em 1956 por Allen Newell, Cliff Shaw e Herbert A. Simon para "imitar o raciocínio humano" na demonstração de teoremas e foi demonstrado em cinquenta e dois teoremas do capítulo dois do Principia Mathematica, provando trinta e oito deles.[10] Além de provar os teoremas, o programa encontrou uma prova para um dos teoremas que era mais elegante do que a fornecida por Whitehead e Russell. Após uma tentativa frustrada de publicar seus resultados, Newell, Shaw e Herbert relataram em sua publicação de 1958, The Next Advance in Operation Research:

"Existem agora no mundo máquinas que pensam, que aprendem e que criam. Além disso, sua capacidade de fazer essas coisas aumentará rapidamente até que (num futuro visível) a gama de problemas que elas podem resolver seja tão extensa quanto aquela à qual a mente humana tem sido aplicada."[11]

Exemplos de Provas Formais

AnoTeoremaSistema de ProvaFormalizadorProva Tradicional
1986Primeira IncompletudeBoyer–MooreShankar[12]Gödel
1990Reciprocidade QuadráticaBoyer–MooreRussinoff[13]Eisenstein
1996Fundamental do CálculoHOL LightHarrisonHenstock
2000Fundamental da ÁlgebraMizarMilewskiBrynski
2000Fundamental da ÁlgebraRocq (então: Coq)Geuvers et al.Kneser
2004Quatro CoresRocq (então: Coq)GonthierRobertson et al.
2004Números PrimosIsabelleAvigad et al.Selberg-Erdős
2005Curva de JordanHOL LightHalesThomassen
2005Ponto Fixo de BrouwerHOL LightHarrisonKuhn
2006Flyspeck 1IsabelleBauer–NipkowHales
2007Resíduo de CauchyHOL LightHarrisonClássica
2008Números PrimosHOL LightHarrisonProva analítica
2012Feit–ThompsonRocq (então: Coq)Gonthier et al.[14]Bender, Glauberman and Peterfalvi
2016Problema dos triplos pitagóricos booleanosFormalizado como SATHeule et al.[15]Nenhuma

Sistemas de prova

[editar | editar código]
Provador de Teoremas Boyer-Moore (NQTHM)
O design do NQTHM foi influenciado por John McCarthy e Woody Bledsoe. Iniciado em 1971 em Edimburgo, Escócia, este foi um provador de teoremas totalmente automático construído usando Lisp puro. Os principais aspectos do NQTHM foram:
  1. o uso de Lisp como uma lógica de trabalho.
  2. a dependência de um princípio de definição para funções recursivas totais.
  3. o uso extensivo de reescrita e "avaliação simbólica".
  4. uma heurística de indução baseada na falha da avaliação simbólica.[16][17]
HOL Light
Escrito em OCaml, o HOL Light é projetado para ter uma base lógica simples e limpa e uma implementação desobstruída. É essencialmente outro assistente de prova para lógica clássica de ordem superior.[18]
Rocq
Desenvolvido na França, o Rocq é outro assistente de prova automatizado, que pode extrair automaticamente programas executáveis a partir de especificações, como código-fonte Objective CAML ou Haskell. Propriedades, programas e provas são formalizados na mesma linguagem chamada Cálculo das Construções Indutivas (CIC).[19]

Aplicações

[editar | editar código]

O raciocínio automatizado tem sido mais comumente usado para construir provadores automatizados de teoremas. Frequentemente, no entanto, os provadores de teoremas exigem alguma orientação humana para serem eficazes e, portanto, se qualificam mais geralmente como assistentes de prova. Em alguns casos, tais provadores criaram novas abordagens para provar um teorema. O Logic Theorist é um bom exemplo disso. O programa criou uma prova para um dos teoremas do Principia Mathematica que era mais eficiente (exigindo menos etapas) do que a prova fornecida por Whitehead e Russell. Programas de raciocínio automatizado estão sendo aplicados para resolver um número crescente de problemas em lógica formal, matemática e ciência da computação, programação lógica, verificação de software e hardware, projeto de circuitos e muitos outros. O TPTP (Sutcliffe e Suttner 1998) é uma biblioteca de tais problemas que é atualizada regularmente. Há também uma competição entre provadores automatizados de teoremas realizada regularmente na conferência CADE (Pelletier, Sutcliffe and Suttner 2002); os problemas para a competição são selecionados da biblioteca TPTP.[20]

Ver também

[editar | editar código]

Conferências e workshops

[editar | editar código]

Periódicos

[editar | editar código]

Comunidades

[editar | editar código]

Referências

[editar | editar código]
  1. ↑ Defourneaux, Gilles, and Nicolas Peltier. "Analogy and abduction in automated deduction." IJCAI (1). 1997.
  2. ↑ Kemper, Jonathan (11 de maio de 2025). «Deepseek-R1 triggers boom in reasoning-enabled language models». the decoder (em inglês). Consultado em 16 de maio de 2025
  3. ↑ Garcez, Artur (30 de Maio de 2025). «Neurosymbolic AI is the answer to large language models' inability to stop hallucinating». The Conversation. doi:10.64628/AB.5gpku36ct
  4. ↑ Jones, Nicola (2025). «How good old-fashioned AI could spark the field's next revolution». Nature (News feature). 647: 842-844. doi:10.1038/d41586-025-03856-1
  5. ↑ Rosenbush, Steven (12 de agosto de 2025). «Meet Neurosymbolic AI, Amazon's Method for Enhancing Neural Networks». Wall Street Journal (em inglês). ISSN 0099-9660. Consultado em 16 de agosto de 2025. Cópia arquivada em 17 de fevereiro de 2026
  6. ↑ C. Hales, Thomas "Formal Proof", University of Pittsburgh. Retrieved on 2010-10-19
  7. 1 2 "Automated Deduction (AD)", [The Nature of PRL Project]. Retrieved on 2010-10-19
  8. ↑ Martin Davis (1983). «The Prehistory and Early History of Automated Deduction». In: Jörg Siekmann; G. Wrightson. Automation of Reasoning (1) — Classical Papers on Computational Logic 1957–1966. Heidelberg: Springer. pp. 1–28. ISBN 978-3-642-81954-4 Here: p.15
  9. ↑ "Principia Mathematica", at Stanford University. Retrieved 2010-10-19
  10. ↑ "The Logic Theorist and its Children" [ligação inativa]. Retrieved 2010-10-18
  11. ↑ Shankar, Natarajan Little Engines of Proof, Computer Science Laboratory, SRI International. Retrieved 2010-10-19
  12. ↑ Shankar, N. (1994), Metamathematics, Machines, and Gödel's Proof, ISBN 9780521585330, Cambridge, UK: Cambridge University Press
  13. ↑ Russinoff, David M. (1992), «A Mechanical Proof of Quadratic Reciprocity», J. Autom. Reason., 8 (1): 3–21, doi:10.1007/BF00263446
  14. ↑ Gonthier, G.; et al. (2013), «A Machine-Checked Proof of the Odd Order Theorem» (PDF), in: Blazy, S.; Paulin-Mohring, C.; Pichardie, D., Interactive Theorem Proving, ISBN 978-3-642-39633-5, Lecture Notes in Computer Science, 7998, pp. 163–179, CiteSeerX 10.1.1.651.7964Acessível livremente, doi:10.1007/978-3-642-39634-2_14
  15. ↑ Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W. (2016). «Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer». Theory and Applications of Satisfiability Testing – SAT 2016. Col: Lecture Notes in Computer Science. 9710. [S.l.: s.n.] pp. 228–245. ISBN 978-3-319-40969-6. arXiv:1605.00723Acessível livremente. doi:10.1007/978-3-319-40970-2_15
  16. ↑ The Boyer-Moore Theorem Prover Retrieved on 2010-10-23
  17. ↑ Boyer, Robert S. and Moore, J Strother and Passmore, Grant Olney The PLTP Archive. Retrieved on 2023-07-27
  18. ↑ Harrison, John HOL Light: an overview. Retrieved 2010-10-23
  19. ↑ Introduction to Coq. Retrieved 2010-10-23
  20. ↑ «Automated Reasoning». Stanford Encyclopedia of Philosophy. 2025

Ligações externas

[editar | editar código]
Obtida de "https://pt.wikipedia.org/w/index.php?title=Raciocínio_automatizado&oldid=73103467"