O que é o raciocínio automatizado?
Raciocínio automatizado é o campo da ciência da computação que tenta fornecer garantias sobre o que um sistema ou programa fará ou nunca fará. Essa garantia se baseia em comprovação matemática. As pessoas resolvem muitos problemas lógicos em matemática, ciências e computação usando estratégias lógicas, como teoremas e deduções. O raciocínio automatizado usa computadores que utilizam as mesmas ferramentas para resolver desafios complexos. As ferramentas de raciocínio automatizado tentam responder a perguntas sobre um programa (ou uma fórmula lógica) usando técnicas conhecidas da matemática. As ferramentas ajudam você a verificar o que é verdade sobre uma afirmação ou expressão.
Quais problemas o raciocínio automatizado pode resolver?
Cientistas e desenvolvedores de software usam o raciocínio automatizado para provar duas coisas. Primeiro, que o projeto ou a implementação de um sistema obedecem às especificações. Segundo, que funciona da maneira pretendida.
O raciocínio automatizado faz isso produzindo provas em lógica formal apoiadas por teoremas matemáticos ou verdades conhecidas. O raciocínio automatizado usa métodos matemáticos de verificação algorítmica baseados em lógica para produzir provas de segurança ou correção para todos os comportamentos possíveis.
O raciocínio automatizado também pode ser usado para provar que os sistemas usados para configurar redes, permitir acesso à rede, conceder permissões ou manter os dados privados e seguros funcionam conforme o esperado.
Ao usar o raciocínio automatizado, você primeiro apresenta ao sistema uma afirmação do problema. Em seguida, o sistema de raciocínio automatizado calcula e valida as suposições com a afirmação do problema. O software faz isso até esgotar todas as opções.
Exemplo de problema para raciocínio automatizado
Para entender melhor o raciocínio automatizado, considere a afirmação do problema Os gatos vivem na terra? e as seguintes afirmações:
- Gatos são mamíferos
- Mamíferos vivem na terra
O sistema de raciocínio automatizado avalia se a afirmação do problema é verdadeira. Especificamente, ele usa dedução lógica. Nesse caso, os gatos são mamíferos, e os mamíferos vivem na terra. Então, verificaria se os gatos vivem na terra.
Limitações do raciocínio automatizado
O raciocínio automatizado não faz previsões ou generalizações. Por exemplo, podemos usá-lo para apresentar um argumento como este:
- Gatos têm pelos
- Mingau é um gato
- Então, Mingau tem pelos
Não podemos usar o raciocínio automatizado para apresentar argumentos como estes:
- Gatos são mamíferos
- Gatos vivem na terra
- Então, todos os mamíferos vivem na terra
Essas aplicações são comuns em um provador de teoremas, que requer orientação humana ao realizar tarefas de raciocínio dedutivo.
Quais são alguns exemplos de uso do raciocínio automatizado?
A capacidade do raciocínio automatizado de fazer inferências lógicas passo a passo é útil em várias áreas. Usando o raciocínio automatizado, é possível comprovar as propriedades de segurança, conformidade, disponibilidade, durabilidade e proteção de arquiteturas de grande escala.
Aqui estão alguns outros exemplos de uso para o raciocínio automatizado.
Modelagem matemática
Cientistas, engenheiros e matemáticos resolvem problemas e verificam provas matemáticas aplicando fórmulas algébricas em atividades científicas. Em tais práticas, esses profissionais usam modelos matemáticos que dependem de diversas variáveis para deduzir as prováveis soluções de um problema.
Verificação de hardware
O raciocínio automatizado ajuda engenheiros de hardware a criar produtos confiáveis. Isso permite a descoberta de possíveis falhas ignoradas pelos métodos de teste convencionais.
Por exemplo, engenheiros de projetos eletrônicos usam análises rigorosas de raciocínio matemático automatizado para obter provas conclusivas de que um determinado projeto de hardware atende às especificações, como os comportamentos ou execuções do sistema.
A verificação mostra que todos os comportamentos possíveis do sistema satisfazem as propriedades temporais que compõem a especificação. Também pode mostrar que cada comportamento possível da implementação do sistema é consistente com algum comportamento de sua especificação geral.
Validação de software
Desenvolvedores de software usam o raciocínio automatizado para ajudar a garantir que os aplicativos sejam robustos contra problemas de segurança indesejados e que o software funcione conforme planejado ou projetado. Assim como a verificação de hardware, o raciocínio automatizado permite que desenvolvedores validem medidas de segurança de software em relação a várias políticas.
Por exemplo, engenheiros da Amazon Web Services (AWS) usam raciocínio automatizado para provar que o código de inicialização é seguro para cada configuração de inicialização. Outro exemplo é a comprovação de que os dados armazenados e processados no Amazon Simple Storage Service (Amazon S3) estão protegidos. Neste exemplo, o raciocínio automatizado é usado para replicação, consistência, ajuste de escala automático, balanceamento de carga e outras tarefas de coordenação.
Modelagem de raciocínio humano
Cientistas da computação usam tecnologias de raciocínio automatizado para configurar o acesso. Para fazer isso, escrevem políticas que descrevem quando permitir e negar solicitações de usuários para acessar um recurso. Isso ajuda a fazer com que apenas os usuários desejados tenham acesso a um recurso, o que é importante para a segurança e a privacidade do recurso.
Por exemplo, cientistas da computação usam fórmulas de teorias de módulos de satisfatibilidade (SMT) e solucionadores de SMT para provar propriedades de segurança.
Quais são algumas ferramentas e técnicas de raciocínio automatizado?
Em seguida, compartilhamos vários métodos de dedução automatizada que permitem aos sistemas de computação realizar a dedução humana.
Lógica clássica
A lógica clássica é uma filosofia matemática que fornece modelos básicos de raciocínio para programas automatizados de raciocínio lógico. Essa lógica é baseada no princípio de que cada proposição tem um valor de verdade de verdadeiro ou falso, mas não ambos.
O principal foco é a lógica de primeira ordem, que permite aos matemáticos representar variáveis desconhecidas como x com quantificadores como existe em uma frase. Por exemplo, cientistas aplicam a lógica clássica na programação lógica para encontrar x nesta frase: O x existe, de tal forma que x vive na terra e x é um mamífero.
Lógica proposicional
A lógica proposicional é um sistema lógico no qual existem proposições que podem ser verdadeiras ou falsas, e a construção de relações entre elas são chamadas de argumentos.
A afirmação clássica de um argumento na lógica proposicional é Se P, então Q. Por exemplo, se for sábado, então é fim de semana.
O raciocínio automatizado usa uma técnica chamada resolução SAT. Ferramentas chamadas de solucionadores SAT são usadas para pesquisar atribuições satisfatórias para argumentos na lógica proposicional. Isso significa variáveis que tornam o argumento verdadeiro.
Qual é a diferença entre raciocínio automatizado e inteligência artificial?
O raciocínio automatizado é uma disciplina específica da inteligência artificial (IA) que aplica dedução lógica aos sistemas de computador.
A IA é uma ciência que ensina computadores a pensar como pessoas ao resolverem problemas. Desdobramentos recentes em IA levaram ao avanço de várias subdisciplinas, incluindo aprendizado profundo, análise de dados e machine learning.
O raciocínio automatizado é diferente de outras tecnologias de IA, como o processamento de linguagem natural (PLN), que se concentra em treinar computadores para entender discursos escritos ou verbais. Em vez disso, o raciocínio automatizado usa modelos lógicos e provas para raciocinar sobre os possíveis comportamentos de um sistema ou programa, incluindo estados que ele pode ou nunca alcançará.
Qual é a diferença entre raciocínio automatizado e aprendizado profundo?
O raciocínio automatizado comprova as propriedades de um programa ou sistema. Ele usa o programa ou o próprio sistema, assim como um modelo ou especificação do sistema em lógica formal.
O aprendizado profundo faz previsões com base na aplicação de modelos estatísticos a grandes conjuntos de dados.
O aprendizado profundo é uma tecnologia avançada de machine learning que simula como o cérebro humano funciona. Diferentes modelos de rede neural são usados, que consistem em várias camadas de neurônios que extraem, comparam e analisam informações relevantes. Cientistas de dados usam o aprendizado profundo para tarefas complexas, como o processamento de dados de câmeras e sensores em carros autônomos.
O raciocínio automatizado é machine learning?
Raciocínio automatizado e machine learning não são a mesma coisa. Resumindo, o machine learning faz previsões e inferências. Já o raciocínio automatizado fornece provas.
O machine learning é uma subárea da IA que treina computadores para tomar decisões com grandes amostras de dados. Por exemplo, cientistas de dados usam machine learning a fim de treinar softwares bancários para identificar atividades fraudulentas. Grandes amostras de dados financeiros são usadas para garantir que o software identifique facilmente os padrões anormais com base nos resultados aprendidos antes.
Em vez de treinar com dados, o raciocínio automatizado faz com que o modelo deduza um resultado segundo verdades e provas matemáticas.
Como a AWS usa o raciocínio automatizado para melhorar as ofertas de serviços?
A AWS usa o raciocínio automatizado para melhorar várias ofertas de serviços. Eis alguns exemplos:
- O Amazon CodeGuru Reviewer usa raciocínio automatizado e machine learning para ajudar desenvolvedores a identificar vulnerabilidades de software.
- O Amazon Inspector Classic tem um recurso de "Acessibilidade de rede" que analisa automaticamente as instâncias do EC2 em busca de possíveis vulnerabilidades de segurança e configurações incorretas.
- O AWS Identity and Access Management (IAM) Access Analyzer gerencia as permissões de contas com raciocínio automatizado.
- O Amazon Virtual Private Cloud (Amazon VPC) Reachability Analyzer aplica raciocínio automatizado para ajudar você a entender e visualizar a rede da AWS.
Visite Segurança comprovada para mais informações sobre raciocínio automatizado em todos os serviços da AWS. Usamos o raciocínio matemático para fornecer garantias de proteção sólidas aos seus workloads de segurança.
Comece a usar a segurança da AWS criando uma conta agora.
Próximas etapas na AWS
Obtenha acesso instantâneo ao nível gratuito da AWS.
