Otomatik Akıl Yürütme Nedir?
Otomatik akıl yürütme, bir sistemin veya programın ne yapacağı veya asla yapmayacağı konusunda güvence sağlamaya çalışan bilgisayar bilimi alanıdır. Bu güvence matematiksel kanıta dayanmaktadır. İnsanlar matematik, bilim ve hesaplamada teoremler ve çıkarımlar gibi mantıksal stratejiler kullanarak birçok mantıksal problemi çözer. Otomatik akıl yürütme, karmaşık zorlukları çözmek için aynı araçları kullanan bilgisayarları kullanır. Otomatik akıl yürütme araçları, matematikten bilinen teknikleri kullanarak bir program (veya bir mantık formülü) hakkındaki soruları yanıtlamaya çalışır. Araçlar, bir ifade veya anlatım hakkında neyin doğru olduğunu kontrol etmenize yardımcı olur.
Otomatik akıl yürütme hangi sorunları çözebilir?
Bilim adamları ve yazılım geliştiricileri, iki şeyi kanıtlamak için otomatik akıl yürütmeyi kullanıyor. İlk olarak, bir sistem tasarımının veya uygulamasının spesifikasyonuna uyduğunu kanıtlarlar. İkincisi, amaçlandığı gibi çalıştığını kanıtlarlar.
Otomatik akıl yürütme bunu matematiksel teoremlerle veya bilinen gerçeklerle desteklenen biçimsel mantıkta kanıtlar üreterek yapar. Otomatik akıl yürütme olası tüm davranışlar için güvenlik veya doğruluk kanıtları üretmek için matematiksel, mantık tabanlı algoritmik doğrulama yöntemleri kullanır.
Otomatik akıl yürütme, ağları yapılandırmak, ağ erişimine izin vermek veya izinler sağlamak veya verileri amaçlandığı gibi gizli ve güvenli bir şekilde tutmak için kullanılan sistemleri kanıtlamak için de kullanılabilir.
Otomatik akıl yürütmeyi kullandığınızda, önce sisteme bir sorun ifadesi sunarsınız. Daha sonra otomatik akıl yürütme sistemi, varsayımları sorun ifadesiyle hesaplar ve doğrular. Yazılım, tüm seçenekleri tüketene kadar bunu yapar.
Otomatik akıl yürütme için örnek sorun
Otomatik akıl yürütmeyi daha iyi anlamak için, Kediler karada mı yaşar? sorun ifadesini ve aşağıdaki savları düşünün:
- Kediler memelidir
- Memeliler karada yaşar
Otomatik akıl yürütme sistemi, sorun ifadesinin doğru olup olmadığını değerlendirir. Özellikle, mantıksal çıkarım kullanır. Bu durumda, kediler memelidir ve memeliler karada yaşarlar. Öyleyse, kedilerin karada yaşadığını doğrular.
Otomatik akıl yürütmenin sınırlamaları
Otomatik akıl yürütme, tahminler veya genellemeler yapmaz. Örneğin, böyle bir argüman yapmak için otomatik akıl yürütmeyi kullanabiliriz:
- Kedilerin kılları var
- Fluffy bir kedidir
- Öyleyse, Fluffy"nin kılları var
Bunun gibi argümanlar yapmak için otomatik akıl yürütmeyi kullanamayız:
- Kediler memelidir
- Kediler karada yaşar
- Öyleyse, tüm memeliler karada yaşar
Bu tür uygulamalar, tümdengelimli akıl yürütme görevlerini yerine getirirken insan rehberliği gerektiren bir teorem ispatlayıcı’da yaygındır.
Bazı otomatik muhakeme kullanım durumları nelerdir?
Otomatik akıl yürütmenin mantık çıkarımlarını adım adım yapma yeteneği çeşitli alanlarda faydalıdır. Otomatik akıl yürütmeyi kullanarak büyük ölçekli mimarilerin güvenlik, uyumluluk, kullanılabilirlik, dayanıklılık ve emniyet özelliklerini kanıtlayabilirsiniz.
İşte otomatik akıl yürütme için diğer bazı kullanım durumları.
Matematiksel model
Bilim adamları, mühendisler, ve matematikçiler bilimsel uygulamalarda cebirsel formüller uygulayarak problemleri çözer ve matematiksel kanıtları doğrular. Bu tür uygulamalarda, bir soruna olası çözümleri çıkarmak için çeşitli değişkenlere dayanan matematiksel modeller kullanırlar.
Donanım doğrulaması
Otomatik akıl yürütme, donanım mühendislerinin güvenilir ürünler üretmesine yardımcı olur. Geleneksel test yöntemleriyle gözden kaçan potansiyel kusurları keşfetmelerini sağlar.
Örneğin, elektronik tasarım mühendisleri, belirli bir donanım tasarımının, sistem davranışları veya uygulamaları gibi spesifikasyonunu karşıladığına dair kesin kanıt elde etmek için titiz matematiksel otomatik akıl yürütme analizleri kullanır.
Doğrulama, sistemin tüm olası davranışlarının spesifikasyonu oluşturan zamansal özellikleri karşıladığını gösterir. Ayrıca, sistemin uygulanmasının her olası davranışının, üst düzey spesifikasyonunun bazı davranışlarıyla tutarlı olduğunu da gösterebilir.
Yazılım doğrulama
Yazılım geliştiricileri, uygulamaların istenmeyen güvenlik sorunlarına karşı sağlam olmasını ve yazılımın amaçlandığı veya tasarlandığı gibi çalışmasını sağlamak için otomatik akıl yürütmeyi kullanır. Donanım doğrulaması gibi, otomatik akıl yürütme de geliştiricilerin yazılım güvenlik önlemlerini çeşitli politikalara göre doğrulamasına olanak tanır.
Örneğin, Amazon Web Services (AWS) mühendisleri, ön yükleme kodunun, otomatik akıl yürütme ile her ön yükleme yapılandırması için güvenli olduğunu kanıtlar. Diğer bir örnek, Amazon Basit Depolama Hizmeti (Amazon S3) üzerinde depolanan ve işlenen verilerin korunduğunu kanıtlamasıdır. Bu örnekte, çoğaltma, tutarlılık, otomatik ölçeklendirme, yük dengeleme ve diğer koordinasyon görevleri için otomatik mantığa dayanırlar.
İnsan muhakemesi modelleme
Bilgisayar bilimcileri, erişimi yapılandırmak için otomatik akıl yürütme teknolojilerini kullanır. Bunu yapmak için, bir kaynağa erişmek için kullanıcı isteklerine ne zaman izin verileceğini veya reddedileceğini açıklayan ilkeler yazarlar. Bu, kaynağın güvenliği ve gizliliği için önemli olan kaynağa yalnızca amaçlanan kullanıcıların erişebildiğini doğrular.
Örneğin, bilgisayar bilimcileri güvenlik özelliklerini kanıtlamak için tatmin edilebilirlik modulo teorileri (SMT) formülleri ve SMT çözücüleri kullanırlar.
Bazı otomatik akıl yürütme araçları ve teknikleri nelerdir?
Ardından, bilgi işlem sistemlerinin insan çıkarımları gerçekleştirmesini sağlayan birkaç otomatik çıkarım yöntemini paylaşıyoruz.
Klasik mantık
Klasik mantık, otomatik mantıksal akıl yürütme programları için temel akıl yürütme modelleri sağlayan matematiksel bir felsefedir. Bu mantık, her önermenin doğru veya yanlış bir gerçek değerine sahip olduğu, ancak her ikisinin de olmadığı ilkesine dayanmaktadır.
Öncelikle birinci dereceden mantığa odaklanır, matematikçilerin x gibi bilinmeyen değişkenleri bir cümlede varmış gibi niceleyicilerle temsil etmelerine olanak tanır. Örneğin, bilim adamları bu cümlede x"i bulmak için mantık programlamada klasik mantığı uygular: X var ve x karada yaşıyor ve x bir memeli.
Önerme mantığı
Önerme mantığı, doğru veya yanlış olabilecek önermelerin olduğu ve aralarında argümanlar denilen ilişkilerin kurulduğu bir mantık sistemidir.
Önerme mantığındaki bir argümanın klasik ifadesi P ise, Q’dur şeklindedir. Örneğin, bugün Cumartesi ise, o zaman hafta sonudur.
Otomatik akıl yürütme, SAT çözme adı verilen bir teknik kullanır. Önerme mantığındaki argümanlara tatmin edici tahsisler aramak için SAT çözücüler adı verilen araçları kullanır. Bu, argümanı doğru yapan değişkenler anlamına gelir.
Otomatik akıl yürütme ve yapay zeka arasındaki fark nedir?
Otomatik akıl yürütme, bilgisayar sistemlerine mantıksal kesinti uygulayan belirli bir yapay zeka (AI) disiplinidir.
AI, bilgisayarlar sorunları çözdüğünde bilgisayarlara insanlar gibi düşünmeyi öğreten bir bilimdir. Yapay zekadaki son gelişmeler derin öğrenme, veri analizi ve makine öğrenimi dahil, çeşitli alt disiplinlerin ilerlemesine yol açtı, i.
Otomatik akıl yürütme, yazılı veya sözlü konuşmaları anlamak için bilgisayarları eğitmeye odaklanan doğal dil işleme (NLP) gibi diğer yapay zeka teknolojilerinden farklıdır. Yerine, otomatik akıl yürütme, ulaşamayacağı veya asla ulaşamayacağı durumlar dahil, bir sistemin veya programın olası davranışları hakkında akıl yürütmek için mantıksal modeller ve kanıtlar kullanır.
Otomatik akıl yürütme ve derin öğrenme arasındaki fark nedir?
Otomatik akıl yürütme, bir programın veya sistemin özelliklerini kanıtlar. Programın veya sistemin kendisinin yanı sıra, sistemin bir modelini veya özelliklerini biçimsel mantıkta kullanır.
Derin öğrenme, istatistiksel modellerin büyük veri kümelerine uygulanmasına dayalı tahminlerde bulunur.
Derin öğrenme, insan beyninin nasıl çalıştığını simüle eden gelişmiş bir makine öğrenimi teknolojisidir. İlgili bilgileri çıkaran, karşılaştıran ve analiz eden birden fazla nöron katmanından oluşan farklı sinir ağı modelleri kullanır. Veri bilimcileri, kendi kendine giden araçlarda kamera ve sensör verilerinin işlenmesi gibi karmaşık uygulamalar için derin öğrenmeyi kullanır.
Otomatik akıl yürütme makine öğrenimi mi?
Otomatik akıl yürütme ve makine öğrenimi aynı şey değildir. Kısacası, makine öğrenimi tahminler ve çıkarımlar yapar. Otomatik akıl yürütme kanıt sağlar.
Makine öğrenimi, bilgisayarları büyük veri örnekleriyle karar vermeleri için eğiten bir yapay zeka alt kümesidir. Örneğin, veri bilimcileri, dolandırıcılık faaliyetlerini belirlemek üzere bankacılık yazılımını eğitmek için makine öğrenimini kullanır. Yazılımın önceden öğrenilen sonuçlara dayanarak anormal kalıpları kolayca tanımlamasını sağlamak için büyük finansal veri örnekleri kullanırlar..
Modeli verilerle eğitmek yerine, otomatik akıl yürütme, modelin matematiksel gerçeğe ve kanıta dayalı bir sonuç çıkarmasını sağlar.
AWS, hizmet tekliflerini iyileştirmek için otomatik akıl yürütmeyi nasıl kullanır?
AWS, çeşitli hizmet tekliflerini iyileştirmek için otomatik akıl yürütmeyi kullanır. Aşağıda bazı örnekler veriyoruz:
- Amazon CodeGuru İzleyici, geliştiricilerin yazılım güvenlik açıklarını belirlemelerine yardımcı olmak için otomatik akıl yürütme ve makine öğrenimi kullanır.
- Amazon Inspector Classic, olası güvenlik açıkları ve yanlış yapılandırmalar için EC2 bulut sunucularınızı otomatik olarak analiz eden bir Ağ Ulaşılabilirlik özelliğine sahiptir.
- AWS Kimlik ve Erişim Yönetimi (IAM) Erişim Analiz Aracı, otomatik akıl yürütme ile hesap izinlerini yönetir.
- Amazon Sanal Özel Bulut (Amazon VPC) Erişilebilirlik Analizörü, AWS ağınızı anlamanıza ve görselleştirmenize yardımcı olmak için otomatik akıl yürütme uygular.
AWS hizmetlerinde otomatik muhakeme hakkında daha fazla bilgi için Provable Security sayfasını ziyaret edin. Güvenlik iş yükleriniz için güçlü güvenlik güvenceleri sağlamak için matematiksel akıl yürütmeyi kullanıyoruz.
Hemen bir hesap oluşturarak AWS'de API'leri kullanmaya başlayın.
AWS'de Sonraki Adımlar
