Girdeji:
- Subutnamanyň ideýasyny we usulyny (göni, gapma-garşylyk, induktiw, garşylykly) tapmak we her logiki ädimiň dogrulygyny öz-özüni barlamak üçin emeli intellekt ulanmak ukyby;
- “Açyk”, “umumylyga zyýan bermezden” ýaly sözleriň aňyrsynda aç-açan boşluklary, aç-açan çaklamalary we esassyz böküşleri kesgitlemek ukyby.
- Talabyň dogrulygyna göz ýetirmezden, subutnama bil baglamazdan ozal garşylykly mysallary gözläp, arassalygy we ygtybarlylygy tapawutlandyrmak ukyby.
Matematiki subutnama, kabul edilen aksiomalardan we öň subut edilen teoremalardan logiki ädimlerde talapyň takyk çykarylmagydyr. Subut etmek matematikanyň iň berk önümidir: ýekeje nädogry logiki geçiş, "boşluk" diýýän ýalňyş ýa-da aç-açan çaklama, ähli subutnamany ret edýär. Emeli intellekt subutnama üçin ynandyryjy görnüşli tekst taýýarlamaga ökde - şonuň üçinem howply. Ynandyryjy ýaly görünýän tekst dogry subutnama däl. Bu bölümde AI-ni subut ediji hyzmatdaş hökmünde nädip ulanmalydygyny we her logiki ädimi nädip barlamalydygyny öwrenersiňiz.
Ilki iki kesgitleme. Subutnama eskiz, subutnamanyň esasy ideýasyny we süňküni berýän, ýöne her jikme-jigi doldurmaýan gysgaça mazmun. Subutnama boşlugy, subutnamanyň "şu ýerden gelýär" diýýän böküşi, ýöne aslynda ony aklamaýar. AI bilen işlän wagtyňyz iň uly töwekgelçilik, ynandyryjy sözlemler bilen baglanyşykly boşluklardyr: tekst suwuk, “şonuň üçin” we “aç-açan” ýaly baglanyşyklardan doly, ýöne arasynda böküşler aslynda subut edilmeýär.
Subutnamada AI-iň güýçleri we gowşak taraplary
AI subut etmek üçin iki zady gowy ýerine ýetirýär: (1) belli teoremany subut etmegiň adaty ideýasyny oýandyrýar, (2) subutnama üçin haýsy usulyň (induksiýa, gapma-garşylyk, göni, gapma-garşylyk) laýyk bolup biljekdigini görkezýär. Onuň gowşak tarapy: asyl ýa-da inçe subutnamanyň her ädiminiň dogrudygyny üpjün etmek. AI dogry ýaly görünýän, ýöne hakykatdanam ýalan “ýalňyş subutnamalary” öndürip biler - mysal üçin, induksiýa ädiminde esasy hadysany geçirip biler ýa-da “umumylygy bozmazdan” aýdyp biler, ýöne umumylygy bozýan çaklamany edip biler.
Şonuň üçin subutnamanyň altyn düzgüni: subutnamanyň ideýasyny tapmak we beýan etmek üçin AI ulanyň; Her logiki ädimiň dogrudygyny özüňiz barlaň. Subutnamany "kabul etmezden" ozal her biriniň "şonuň üçin" dogrudygyna göz ýetiriň.
Stepdimme-ädim: subutnamany barlamak
1. Talaby we çaklamalary aýdyňlaşdyryň. Näme subut edilýär? Haýsy çaklamalara görä? Bular düşnüksiz bolsa, subutnama hem düşnüksiz.
2. Subut etmegiň usulyny biliň. Göni, gapma-garşylyk bilen, induktiw, gapma-garşylyk bilen? Usulyň gurluş talaplaryny biliň (meselem, induksiýada, esasy ýagdaý + induksiýa ädimi möhümdir).
3. Her "şonuň üçin" sorag beriň. Her logiki geçişde "bu hakykatdanam öňki ädimlerden gelýärmi?" sora. Iň mekir boşluklar "aç-açan", "aňsat görünýär", "umumylygy ýitirmän" sözleriň aňyrsynda gizlenýär.
4. Gümürtik çaklamalary gözläň. Subut edilmedik bir çaklama bil baglaýarmy? Mysal üçin, sanyň pozitiwdigini ýa-da bir funksiýanyň üznüksizdigini ýuwaşlyk bilen kabul edip bolar.
5. Mysal üçin synap görüň. Eger talap ýalan bolsa, başga bir mysal ony ýykýar. Subutnamany kabul etmezden ozal ýönekeý aýratyn ýagdaýlarda talapyň dogrudygyny barlaň.
6. Satyn alyş edaralaryna ýüz tutuň. Belli teoremalar üçin adaty subutnamany ygtybarly çeşme bilen deňeşdiriň (okuw kitaby, deňeşdirilen çeşme).
Maslahat: Subutnamadaky "umumylygy ýitirmezden" jümlesi iki ýüzli gylyç. Käwagt hakykatdanam dogry (simmetriýa bar bolsa), käwagt gizlin ýalňyşlyk bolýar. AI bu aňlatmany köp ulanýar. Her gezek "umumylyk hakykatdanam bozulmaýar" diýip özüňizi aklaň; AI sözüni munuň üçin alma.
Subut etmegiň usullary we ýalňyşlyklary
subutnama usuly
Gurluşy
Iň ýaýran AI duzagy
göni
Çaklama → ... → Netije
arasynda bir ädim geçmek
gapma-garşylyk
Munuň tersini kabul ediň → gapma-garşylygy tapyň
Bu gapma-garşylyk hakyky däl
induksiýa
Esasy ýagdaý + ädim
Esasy ýagdaýy ýatdan çykarmak
garşylykly
¬ Netije → assMasama
ýalan ret etmek
Tersine mysal (ret etmek)
ýekeje mysal
Counterexample nädogry
üç sany kiçi halat
1-nji waka - Doly däl iş. Mugallym AI induksiýa arkaly "1 + 2 + ... + n = n (n + 1) / 2" formulasyny subut etdi. AI induksiýa ädimini dogry ýazdy, ýöne hiç haçan esasy hadysany barlamady (n = 1). Mugallym "esasy iş nirede?" Diýip soraýar. diýip sorady. AI goşuldy. Stateer ýagdaýy bolmasa, induksiýa nädogry; 30 sekuntlyk barlag subutnamany ýatda saklady.
2-nji hadysa - nol boýunça gizlin bölüniş. Bir okuwçy “her a, b üçin a = b” ýaly gülkünç “subutnamany” gördi we AI-den “bu ýerde ýalňyşlyk nirede?” Diýip sorady. diýip sorady. YZ subutnamanyň (a - b) bir ädimde bölünýändigini we a = b çaklamasyna görä bu nola bölünýändigini dogry görkezdi. Bu ýerde AI auditor hökmünde üstünlik gazandy; emma okuwçy bu ädimi henizem öz eli bilen barlady.
3-nji waka - falsealan subutnamalary ynandyrmak. In engineeringenerçilik okuwçysy AI deňsizligi subut etdi. Tekst arkaýyn we ynandyryjydy, ýöne bir ädimde inedördül kök alanda, oňyn we otrisatel kökleriň mümkinçiligini äsgermezlik edip, diňe oňyn taraplaryny aldy. Talyp her ädimini soranda bu boşlugy tapdy. Subutnama goşmaça şert (üýtgeýänleriň pozitiwligi) goşulanda güýje girdi.
Göçürip boljak dört şablon
1) Subutnamanyň taslamasyny (ideýa) talap etmek:
Aşakdaky talaplary (göni, gapma-garşylyk, induktiw, garşylykly) subut etmek üçin haýsy usul dogry bolar? Diňe MAIN IDEA we subutnamanyň süňküni beriň, doly subutnamany ýazmaň. Talap: [şu ýerde]
2) stepdimme-ädim, esaslandyrylan subutnama:
Aşakdaky talaby [usul] bilen subut ediň: [talap]. Her ädim üçin haýsy aksioma / teorema / kesgitlemä bil baglaýandygyňyzy ýazyň. "Açyk" ýa-da "aňsat" ýaly aňlatmalary ulanmaň; Her geçişi doly delillendiriň. Induksiýa bolsa, esasy gapagy we induksiýa ädimini aýratyn görkeziň.
3) subutnama aw awlamak:
Aşakdaky subutnamany gözden geçiriň. Diňe logiki boşluklary, aç-açan çaklamalary we esassyz böküşleri gözläň. Her "şonuň üçin" hakykatdanam öňki ädimlerden gelýändigini barlaň. Her ädimiň haýsy ädimdedigini ýazyň. Subut et: [şu ýerde]
4) Mysal üçin gözläň:
Aşakdaky talapyň HAKYKYdygyny ýa-da däldigini barlamak isleýärin: [talap]. Ilki bilen ýönekeý ýagdaýlarda synap görüň; GÖRNÜŞI tapmaga synanyşyň. Munuň tersine mysal tapsaňyz, görkeziň; Eger tapyp bilmeseňiz, synanyşan ýagdaýlaryňyzy sanaň (ýöne bu subutnama däl, diňe subutnama gözläň).
Gowşak haýyş / Güýçli haýyş
Gowşak: "√2 manysyzdygyny subut ediň."
Netije: Adaty subutnama gelýär, ýöne bir ädim (meselem "soň p hatda") hiç hili delilsiz geçip biler we duýmarsyňyz.
Güýçli: "ŞERTLIK BILEN √2 manysyzdygyny subut ediň. Her ädimde haýsy çaklamany ulanandygyňyzy ýazyň;" p² deň bolsa, p hem deňdir "ýaly aralyk talaplary delillendiriň. Netijede, gapma-garşylygyň nirede ýüze çykýandygyny anyk görkeziň."
Netije: Her bir aralyk talap dogry, gapma-garşylygyň çeşmesi aýdyň, boşluklar galmaýar.
Adaty ýalňyşlyklar
- Dogrylygy bilen bulaşyklygy bulaşdyrmak. Ynandyryjy tekst dogry subutnama däl; Her ädim gözegçilik edilmelidir.
- Induksiýada ýeriň ýagdaýyndan geçmek. AI köplenç esasy işi ýatdan çykarýar; Diňe induksiýa ädimi ýeterlik däl.
- Soragsyz "umumylygy ýitirmän" kabul etmek. Bu söz gizlin ýalňyşlyk bolup biler; Her gezek aklaň.
- Gümürtik çaklamalary görmezlik. Oňynlyk, üznüksizlik, nol däl we ş.m. ýaly çaklamalar ýuwaşlyk bilen subutnama girip biler.
- Tersine synanyşmazdan subutnama ynanmak. Eger talap ýalan bolsa, subutnama hem ýalandyr; Ilki bilen ýönekeý ýagdaýlarda talapyň hakykatyny barlaň.
Üns beriň: AI hakykatda ýalan talap üçin hem “subutnama” öndürip biler - tekst öndürýändigi sebäpli logiki ygtybarlylygy kepillendirmeýär. Talabyň dogrudygyny bilmeýän bolsaňyz, ilki bilen garşylyk görkeziň. Falsealan talapyň "subutnamasy" hökmany suratda kemçilikleri öz içine alýar; Siziň işiňiz bu boşlugy tapmak.
Gysgaça
Subut etmek matematikanyň iň berk önümidir we AI ynandyryjy, ýöne nädogry “subutnamalary” öndürip biler. Subutnama ideýasyny we usulyny tapmak üçin AI ulanyň; Her logiki ädimiň dogrudygyny özüňiz barlaň. “Açyk” we “zyýansyz” ýaly söz düzümleriniň esasy ýagdaýlaryny, aç-açan çaklamalary we boşluklary gözläň. Talabyň dogrudygyny bilmeýän bolsaňyz, subutnama ynanmazdan ozal başga bir mysal synap görüň. Erkin gürlemek dogry däl.
Programma meselesi
Adaty teoremany saýlaň (meselem, "iki sany hatda jemi hatda" ýa-da "√2 manysyz"). AI-ni 2-nji şablon bilen ädimme-ädim subut etmegini isläň. Soňra boşlugy awlamak üçin 3-nji şablon bilen birmeňzeş subutnama beriň - öz subutnamasyny barlasyn. Soňra her birini "şonuň üçin" el bilen soraň: esasy waka barmy, aç-açan çaklama barmy, her geçiş dogrymy? Iň bolmanda bir potensial boşlugy ýa-da gowulaşma nokadyny tapyň we belläň.
gözegçilik sanawy
- [] Talaby we çaklamalary düşündirdim.
- [] Subutnama usuly we onuň gurluş talaplary bilen tanyşdym.
- [] Her "şonuň üçin" öňki ädimlerden gelýändigini tassykladym.
- [] Esasy waka / aç-açan çaklama barladym.
- [] Simpleönekeý ýagdaýlarda talaplary barladym we başga mysallary gözledim.
- [] Belli teoremalar üçin adaty subutnamany ygtybarly çeşme bilen deňeşdirdim.