Çerçeve sorunu - Frame problem - Wikipedia

İçinde yapay zeka, çerçeve sorunu kullanımla ilgili bir sorunu açıklar birinci dereceden mantık (FOL) dünyadaki bir robot hakkında gerçekleri ifade etmek için. Bir robotun durumunu geleneksel FOL ile temsil etmek, basitçe çevredeki şeylerin keyfi olarak değişmediğini ima eden birçok aksiyomun kullanılmasını gerektirir. Örneğin, Hayes bir "blok dünya "blokları birlikte istiflemeyle ilgili kurallarla. Bir FOL sisteminde, ek olarak aksiyomlar çevre hakkında çıkarımlar yapmak için gereklidir (örneğin, bir bloğun fiziksel olarak hareket ettirilmediği sürece konumunu değiştiremeyeceği). Çerçeve problemi, bir robot ortamının uygulanabilir bir tanımı için yeterli aksiyom koleksiyonunu bulma problemidir.[1]

John McCarthy ve Patrick J. Hayes bu sorunu 1969 tarihli makalesinde tanımlamış, Yapay Zeka Açısından Bazı Felsefi Sorunlar. Bu makalede ve daha sonra gelen pek çok makalede, biçimsel matematik problemi, yapay zeka için bilgi temsilinin zorluğunun daha genel tartışmaları için bir başlangıç ​​noktasıydı. Rasyonel varsayılan varsayımların nasıl sağlanacağı ve insanların sanal ortamda sağduyu olarak düşündükleri gibi konular.[2] Daha sonra terim daha geniş bir anlam kazandı. Felsefe, eylemlere yanıt olarak güncellenmesi gereken inançları sınırlama sorunu olarak formüle edilir. Mantıksal bağlamda, eylemler tipik olarak, diğer her şeyin (çerçeve) değişmeden kaldığı örtük varsayımıyla, değiştirdikleriyle belirlenir.

Açıklama

Çerçeve sorunu çok basit alanlarda bile ortaya çıkar. Açık veya kapalı olabilen bir kapısı ve açık veya kapalı olabilen bir ışığı olan bir senaryo, statik olarak iki ile temsil edilir. önermeler ve . Bu koşullar değişebilirse, iki ile daha iyi temsil edilirler yüklemler ve zamana bağlı olan; bu tür yüklemler denir akıcı. 0 zamanında kapının kapalı olduğu ve ışığın kapalı olduğu ve 1. zamanda kapının açıldığı bir alan doğrudan mantıkla temsil edilebilir.[açıklama gerekli ] aşağıdaki formüllerle:

İlk iki formül ilk durumu temsil eder; üçüncü formül, kapıyı açma eylemini 1. anda gerçekleştirmenin etkisini temsil eder. Böyle bir eylem, kapının kilidinin açılması gibi ön koşullara sahip olsaydı, şu şekilde temsil edilirdi: . Pratikte, birinin bir yüklemi olurdu bir eylemin ne zaman yürütüleceğini ve bir kuralı belirlemek için eylemlerin etkilerini belirlemek için. İle ilgili makale durum hesabı daha fazla ayrıntı verir.

Yukarıdaki üç formül, bilinenlerin mantığında doğrudan bir ifade olsa da, sonuçları doğru bir şekilde çizmek için yeterli değildir. Aşağıdaki koşullar (beklenen durumu temsil eden) yukarıdaki üç formülle tutarlı olsa da, bunlar yalnızca bunlar değildir.

   

Aslında, yukarıdaki üç formülle tutarlı olan başka bir koşul kümesi şudur:

   

Çerçeve sorunu, yalnızca eylemler tarafından hangi koşulların değiştirildiğini belirlemenin diğer tüm koşulların değiştirilmemesini gerektirmemesidir. Bu sorun, eylemlerden etkilenmeyen tüm koşulların bu eylem gerçekleştirilirken değiştirilmeyeceğini açıkça belirten "çerçeve aksiyomları" eklenerek çözülebilir. Örneğin, 0 zamanında gerçekleştirilen eylem kapıyı açma eylemi olduğundan, bir çerçeve aksiyomu, ışığın durumunun 0'dan 1'e kadar değişmediğini belirtecektir:

Çerçeve problemi, böyle bir çerçeve aksiyomunun, eylemin koşulu etkilemeyeceği şekilde her eylem ve koşul çifti için gerekli olmasıdır.[açıklama gerekli ] Diğer bir deyişle, sorun, çerçeve aksiyomlarını açıkça belirtmeden dinamik bir alanı resmileştirmektir.

McCarthy tarafından bu sorunu çözmek için önerilen çözüm, minimum miktarda koşul değişikliğinin meydana geldiğini varsaymayı içerir; bu çözüm şu çerçeve kullanılarak resmileştirilmiştir sınırlama. Yale atış sorunu Ancak, bu çözümün her zaman doğru olmadığını gösterir. Daha sonra, tahmini tamamlama, akıcı kapanma, halef devlet aksiyomları, vb.; aşağıda açıklanmıştır. 1980'lerin sonunda, McCarthy ve Hayes tarafından tanımlanan çerçeve sorunu çözüldü.[açıklama gerekli ]. Bundan sonra bile, "çerçeve problemi" terimi, kısmen aynı probleme, ancak farklı ortamlarda (örneğin, eşzamanlı eylemler) ve kısmen de dinamik bir şekilde temsil ve muhakeme genel problemine atıfta bulunmak için kullanıldı. alanlar.

Çözümler

Aşağıdaki çözümler çerçeve probleminin çeşitli şekillerde nasıl çözüldüğünü göstermektedir. Biçimcilikler tam olarak sunulmamaktadır: sunulanlar, tam çözümü açıklamak için yeterli olan basitleştirilmiş versiyonlardır.

Akıcı oklüzyon çözümü

Bu çözüm, Erik Sandewall, ayrıca bir resmi dil dinamik alanların spesifikasyonu için; bu nedenle, böyle bir alan önce bu dilde ifade edilebilir ve ardından otomatik olarak mantığa çevrilebilir. Bu makalede, yalnızca mantıktaki ifade ve eylem adı olmayan basitleştirilmiş dilde gösterilmektedir.

Bu çözümün mantığı, yalnızca koşulların zaman içindeki değerini değil, aynı zamanda son yürütülen eylemden etkilenip etkilenemeyeceklerini de temsil etmektir. İkincisi, tıkanma adı verilen başka bir durumla temsil edilir. Bir koşul olduğu söyleniyor tıkalı belirli bir zaman noktasında, koşulu bir etki olarak doğru veya yanlış yapan bir eylem gerçekleştirilmişse. Tıkanma, “değiştirme izni” olarak görülebilir: Bir koşul tıkanırsa, eylemsizlik kısıtlamasına uymaktan kurtulur.

Kapı ve ışığın basitleştirilmiş örneğinde, tıkanma iki koşulla resmileştirilebilir ve . Mantık, bir koşulun ancak karşılık gelen tıkanma koşulu bir sonraki zaman noktasında doğruysa değeri değiştirebileceğidir. Buna karşılık, kapatma koşulu yalnızca koşulu etkileyen bir eylem yürütüldüğünde doğrudur.

Genel olarak, bir koşulu doğru veya yanlış yapan her eylem, karşılık gelen tıkanma koşulunu da doğru kılar. Bu durumda, doğrudur, yukarıdaki dördüncü formülün öncülünü yanlış yapmak ; bu nedenle, kısıtlama için geçerli değil . Bu nedenle, değeri değiştirebilir, bu da üçüncü formül tarafından zorunlu kılınan şeydir.

Bu koşulun işe yaraması için, oklüzyon tahminlerinin yalnızca bir eylemin sonucu olarak doğru kılındığında doğru olması gerekir. Bu şu şekilde de sağlanabilir: sınırlama veya yüklem tamamlama ile. Tıkanmanın mutlaka bir değişiklik anlamına gelmediğine dikkat etmek önemlidir: örneğin, zaten açıkken (yukarıdaki resmileştirmede) kapıyı açma eylemini yürütmek, yüklemi yapar doğru ve yapar doğru; ancak, zaten doğru olduğu için değeri değiştirmedi.

Tahmin tamamlama çözümü

Bu kodlama, akıcı kapatma çözümüne benzer, ancak ek yüklemler, değişim iznini değil, değişimi ifade eder. Örneğin, yüklemin zamandan değişecek -e . Sonuç olarak, bir yüklem, ancak ve ancak karşılık gelen değişiklik koşulu doğruysa değişir. Bir eylem, ancak ve ancak önceden yanlış olan veya tam tersi bir koşulu doğru yaparsa, değişikliğe neden olur.

Üçüncü formül, kapının açılmasının kapının açılmasına neden olduğunu söylemenin farklı bir yoludur. Kesin olarak, kapının açılmasının, daha önce kapatılmışsa kapının durumunu değiştirdiğini belirtir. Son iki koşul, bir koşulun zaman içinde değer değiştirdiğini belirtir ancak ve ancak ilgili değişiklik koşulu zamanında doğruysa . Çözümü tamamlamak için, değişiklik tahminlerinin doğru olduğu zaman noktalarının olabildiğince az olması gerekir ve bu, eylemlerin etkilerini belirleyen kurallara yüklem tamamlama uygulayarak yapılabilir.

Halef devlet aksiyomları çözümü

Bir eylemin yürütülmesinden sonra bir koşulun değeri, yalnızca ve ancak aşağıdaki durumlarda koşulun doğru olması gerçeğiyle belirlenebilir:

  1. eylem koşulu doğru kılar; veya
  2. koşul önceden doğruydu ve eylem onu ​​yanlış yapmaz.

Bir halef devlet aksiyomu bu iki gerçeğin mantığında bir biçimlendirmedir. Örneğin, eğer ve eylemin o anda yürütüldüğünü belirtmek için kullanılan iki koşuldur sırasıyla kapıyı açmak veya kapatmak için, çalışan örnek aşağıdaki gibi kodlanmıştır.

Bu çözüm, eylemlerin etkilerinden ziyade koşulların değeri etrafında merkezlenmiştir. Başka bir deyişle, her eylem için bir formül yerine her koşul için bir aksiyom vardır. Eylemlerin ön koşulları (bu örnekte mevcut olmayanlar) diğer formüllerle resmileştirilmiştir. Halef durum aksiyomları, varyantta kullanılır. durum hesabı önerenRay Reiter.

Akıcı analiz çözümü

akıcı hesap durum hesabının bir çeşididir. Birinci dereceden mantığı kullanarak çerçeve problemini çözerşartlar, durumları temsil etmek için yüklemlerden çok. Öngörüleri birinci dereceden mantıkta terimlere dönüştürmek denir şeyleşme; akış analizi, koşulların durumunu temsil eden yüklemlerin şeyleştirildiği bir mantık olarak görülebilir.

Birinci dereceden mantıkta bir yüklem ve bir terim arasındaki fark, bir terimin bir nesnenin (muhtemelen diğer nesnelerden oluşan karmaşık bir nesne) bir temsili olması, bir yüklemin ise bir koşul üzerinden değerlendirildiğinde doğru veya yanlış olabilen bir koşulu temsil etmesidir. verilen şartlar.

Akıcı analizde, her olası durum, her biri durumda doğru olan koşulları temsil eden diğer terimlerin bileşimi ile elde edilen bir terimle temsil edilir. Örneğin, kapının açık ve ışığın açık olduğu durum terimle temsil edilir. . Bir koşul değil, nesne olduğu için bir terimin kendi başına doğru veya yanlış olmadığını fark etmek önemlidir. Başka bir deyişle, terim olası bir durumu temsil eder ve tek başına bunun mevcut durum olduğu anlamına gelmez. Bunun belirli bir zamandaki durum olduğunu belirtmek için ayrı bir koşul belirtilebilir, ör. bu zamanın durumu olduğu anlamına gelir .

Akıcı hesapta verilen çerçeve probleminin çözümü, eylem yürütüldüğünde durumu temsil eden bir terimin nasıl değiştiğini belirterek eylemlerin etkilerini belirlemektir. Örneğin, 0 zamanında kapıyı açma eylemi aşağıdaki formülle temsil edilir:

Bir koşulu doğru yerine yanlış yapan kapıyı kapatma eylemi biraz farklı bir şekilde temsil edilir:

Bu formül, uygun aksiyomlar verildiği sürece çalışır. ve örneğin, aynı koşulu iki kez içeren bir terim geçerli bir durum değildir (örneğin, her zaman her biri için yanlıştır ve ).

Olay hesabı çözümü

olay hesabı akıcı analiz gibi akıcıları temsil etmek için terimler kullanır, ancak aynı zamanda halef durum aksiyomları gibi akıcıların değerini sınırlayan aksiyomlara da sahiptir. Olay analizinde, atalet, belirli bir zaman noktasında bir akıcılığın doğru olduğunu ve bu arada onu yanlışa çeviren hiçbir işlem yapılmadığını belirten formüllerle uygulanır. Tahmin tamamlanması, bir akıcılığın yalnızca onu doğru kılan bir eylem gerçekleştirilmişse gerçekleştirildiğini elde etmek için, aynı zamanda yalnızca açıkça belirtilmişse bir eylemin gerçekleştirilmiş olduğunu elde etmek için olay hesaplamasında hala gereklidir.

Varsayılan mantık çözümü

Çerçeve problemi, varsayılan olarak "her şeyin bulunduğu durumda kaldığı varsayılır" ilkesini resmileştirme problemi olarak düşünülebilir (Leibniz, "Gizli Ansiklopediye Giriş", c. 1679). Bu varsayılan, bazen sağduyu eylemsizlik kanunu, tarafından ifade edildi Raymond Reiter içinde varsayılan mantık:

(Eğer durumda doğrudur ve varsayılabilir[3] o eylemi gerçekleştirdikten sonra doğru kalır o zaman şu sonuca varabiliriz doğru kalır).

Steve Hanks ve Drew McDermott onların temelinde savundu Yale atış Örneğin, çerçeve sorununa yönelik bu çözümün tatmin edici olmadığı. Hudson Turner, bununla birlikte, uygun ek postülatların varlığında doğru çalıştığını gösterdi.

Yanıt seti programlama çözümü

Varsayılan mantık çözümünün dilindeki karşılığı cevap seti programlama ile bir kuraldır güçlü olumsuzluk:

(Eğer zamanında doğru ve varsayılabilir ki zaman zaman doğru kalır o zaman şu sonuca varabiliriz doğru kalır).

Ayırma mantığı çözümü

Ayırma mantığı formun ön / son özelliklerini kullanarak bilgisayar programları hakkında akıl yürütmeye yönelik bir biçimciliktir . Ayırma mantığı, Hoare mantığı bilgisayar belleğindeki ve diğer dinamik kaynaklardaki değişken veri yapıları hakkında akıl yürütmeye yöneliktir ve ayrık bellek bölgeleri hakkında bağımsız akıl yürütmeyi desteklemek için "ve ayrı olarak" telaffuz edilen özel bir bağlayıcı * vardır.[4][5]

Ayırma mantığı bir sıkı kodun şunları yapabileceğini söyleyen ön / son özelliklerin yorumlanması sadece ön koşul tarafından var olduğu garanti edilen bellek konumlarına erişin.[6] Bu, mantığın en önemli çıkarım kuralının sağlamlığına yol açar, çerçeve kuralı

Çerçeve kuralı, kodun kapsama alanı (erişilen belleğe) dışındaki keyfi belleğin tanımlarının bir belirtime eklenmesine izin verir: bu, ilk belirtimin yalnızca etki alanına odaklanmasını sağlar. Örneğin, çıkarım

bir listeyi sıralayan kodu yakalar x ayrı bir listeyi ayırmaz y, ve bunu bahsetmeden yapar y çizginin üstündeki ilk spesifikasyonda.

Çerçeve kuralının otomasyonu, kod için otomatik muhakeme tekniklerinin ölçeklenebilirliğinde önemli artışlara yol açtı,[7] sonunda endüstriyel olarak 10 milyonlarca hattan oluşan kod tabanlarına konuşlandırıldı.[8]

Çerçeve problemine ayırma mantığı çözümü ile yukarıda bahsedilen akıcı analiz arasında bazı benzerlikler var gibi görünüyor.

Eylem açıklama dilleri

Eylem açıklama dilleri Çerçeve problemini çözmek yerine atlatın. Eylem tanımlama dili, durumları ve eylemleri açıklamak için özel olan bir sözdizimine sahip resmi bir dildir. Örneğin, eylem kilitli değilse kapıyı açar:

nedenleri Eğer

Bir eylem tanımlama dilinin anlam bilgisi, dilin neyi ifade edebileceğine (eşzamanlı eylemler, gecikmeli etkiler, vb.) Bağlıdır ve genellikle geçiş sistemleri.

Etki alanları doğrudan mantık yerine bu dillerde ifade edildiğinden, çerçeve sorunu yalnızca bir eylem tanımlama mantığında verilen bir belirtimin mantığa çevrilmesi gerektiğinde ortaya çıkar. Bununla birlikte, tipik olarak, bu dillerden bir çeviri verilir. cevap seti programlama birinci dereceden mantık yerine.

Ayrıca bakınız

Notlar

  1. ^ Hayes, Patrick. "Yapay Zekada Çerçeve Sorunu ve İlgili Sorunlar" (PDF). Edinburgh Üniversitesi.
  2. ^ McCarthy, J; P.J. Hayes (1969). "Yapay zeka açısından bazı felsefi sorunlar". Makine Zekası. 4: 463–502. CiteSeerX  10.1.1.85.5082.
  3. ^ yani çelişen bilgi bilinmiyor
  4. ^ Reynolds, J.C. (2002). "Ayırma mantığı: paylaşılan değişken veri yapıları için bir mantık". Bilgisayar Bilimlerinde Mantık Üzerine 17. Yıllık IEEE Sempozyumu Bildiriler Kitabı. Kopenhag, Danimarka: IEEE Comput. Soc: 55–74. CiteSeerX  10.1.1.110.7749. doi:10.1109 / LICS.2002.1029817. ISBN  978-0-7695-1483-3. S2CID  6271346.
  5. ^ O'Hearn, Peter (2019-01-28). "Ayırma mantığı". ACM'nin iletişimi. 62 (2): 86–95. doi:10.1145/3211968. ISSN  0001-0782.
  6. ^ O’Hearn, Peter; Reynolds, John; Yang, Hongseok (2001). Fribourg, Laurent (ed.). "Veri Yapılarını Değiştiren Programlar Hakkında Yerel Akıl Yürütme". Bilgisayar Bilimi Mantığı. Bilgisayar Bilimlerinde Ders Notları. Berlin, Heidelberg: Springer. 2142: 1–19. doi:10.1007/3-540-44802-0_1. ISBN  978-3-540-44802-0.
  7. ^ Calcagno Cristiano; Dino Distefano; Peter O'Hearn; Hongseok Yang (2011-12-01). "Çift Kaçırma Yoluyla Bileşimsel Şekil Analizi". ACM Dergisi. 58 (6): 1–66. doi:10.1145/2049697.2049700. S2CID  52808268.
  8. ^ Distefano, Dino; Fähndrich, Manuel; Logozzo, Francesco; O'Hearn, Peter (2019-07-24). "Statik analizleri Facebook'ta ölçeklendirme". ACM'nin iletişimi. 62 (8): 62–70. doi:10.1145/3338112.

Referanslar

Dış bağlantılar