Kim Michelsen’s Weblog

Et spadestik dybere – afmystificer myterne

Turings stoppeproblem

with 2 comments

I Ingeniøren poppede Turingtesten op igen, men her med understregning af stoppeproblematikken, som Benny Lautrup beskriver i sin artikel i Politiken om Penroses foredrag på Niels Bohr instituttet:

I 1935 opstillede den engelske matematiker Alan Turing en helt generel model for computerberegning, som klargjorde præcist, hvad der menes med et program. I denne model fører Gödels bevis til, at der må findes størrelser, der ikke kan beregnes i en computer. Lidt populært sagt vil computeren løbe løbsk og aldrig stoppe og aflevere et resultat, når den forsøger at beregne sådanne ting. Eksistensbeviset går ligesom før ud på at danne en selvrefererende beregning. Turing antog ganske praktisk, at det var muligt at skrive et superprogram, der på forhånd kunne afgøre, om et vilkårligt program ikke ville stoppe. Superprogrammet skulle altså fodres med et program og først selv stoppe, når det havde fundet ud af, at det program, det var blevet fodret med, ikke stoppede. Men superprogrammet er selv et program. Ved groft sagt at fodre superprogrammet med sig selv, havde Turing konstrueret et program, som, hvis det stoppede, ville have regnet ud, at det ikke stoppede! Han sluttede heraf, at et generelt program, der løser den omtalte opgave, ikke kan skrives. Der findes opgaver, der ikke kan løses af en computer.

Yderligere henvisninger, video om Gödel teoremet og Turing, samt kommentarer til den anden Ing.dk debat, findes i “Kunstig intelligens, bevidsthed eller simuleret intelligens“.

Programmer computere har problemer med

I Penroses bog “The Large, the small, and the Human Mind” nævner han en række problemer som computere enten har svært ved eller overhovedet ikke kan løse, hvor mennesker ikke har nogen problemer. Jeg vil give et par eksempler fra hans bog. De to første er simple skakproblemer men som computere har meget svært ved, specifikt Deep Thought.


I den viste situation er hvids stilling meget svag i forhold til sorts, men hvid har en fordel i at have en barriere mod sort. Deep Thought begik her en kæmpebrøler, som hvid, da den tog det sorte tårn med bonden, hvorved forsvarsværket blev åbnet og sort vandt. Intet menneske ville begå den dumhed.

Samme sted har Penrose vist en endnu mere sofistikeret version.

Problemer der ikke kan løses af computer

En berømt sætning af attenhundredetals matematikeren Lagrange siger at ethvert tal kan udtrykkes som summen af fire kvadrater:

x = a*a + b*b + c*c + d*d

Problemet er nu for computeren at finde et tal der ikke er en sum af fire kvadrater.

Andre eksempler på opgaver der ikke kan beregnes er Polyomino-universer hvor polyominer skal lægges så de dækker en flade.

Spørgsmålet er her om du kan dække planen, uden huller, med de angivne polyominer. Reglerne er simple, faktisk banale, men selvom udviklingen er fuldstændig deterministisk er det ikke beregnbart (følger bevis af Robert Berger). På de efterfølgende sider i hans bog er der flere eksempler med disse Polyominouniverser.

Differentiering og Integration

Det er let at lave et program der kan differentiere kontinuerte funktioner på symbolsk form, der er simple regler hele vejen, men at lave et program der kan gå den modsatte vej, det er ikke let, da der ikke er simple regler for integration på samme måde som for differentiering. Computeren har ikke andet end heuristikker at sætte i stedet for menneskets intuition.

Yderligere

For en bredere og grundigere behandling af Kunstig Intelligens se “Kunstig intelligens, bevidsthed eller simuleret intelligens“, hvor der også er en BBC udsendelse omkring Bevidste computere med udgangspunkt i Gödels teorem.

Written by Kim Michelsen

14 oktober 2008 hos 16:27

Lagt i Bevidsthed, IT

Tagged with ,

2 kommentarer

Subscribe to comments with RSS.

  1. Deep Thought kan til hver en tid slå mig i skak (og selv det skakprogram min Memotech 512 havde i sin tid kunne let slå mig).

    Maple er også langt, langt bedre til at integrere end jeg er.

    Isabelle/HOL kan formodentlig også finde beviser som jeg ikke selv ville kunne finde (har dog ikke prøvet endnu). I hvert fald er en SAT-solver (som fx Chaff) bedre til at verificere logiske kredsløb (og evt. komme med konkrete modbeviser) end jeg er.

    Spin er også bedre til at bevise at protokoller fungerer korrekt end jeg er (og lige som Chaff komme med konkrete modbeviser hvis de ikke fungerer).

    Så øh… datamater kan meget🙂

    (Standardbeviset ang. halting problemet siger ikke noget om hvorvidt der skulle være problemer med nogen som helst anden type programmer end lige netop “superprogrammerne”.)

    Peter Lund

    5 marts 2009 at 19:41

  2. Programmerne er først og fremmest bedre end dig fordi de har en stor database med en masse viden og en cpu med en høj hastighed, der gør at den kan afprøve alle mulige træk eller muligheder som du ikke kan, ikke fordi programmet kan tage bevidste valg.

    I virkeligheden spiller du mod programudvikler(en|ne)s bevidsthed. Det er dem der har forsøgt at forudsige hvad du kan finde på og så programmeret computeren til at behandle dine input.

    Integrationsprogrammerne har fået lagt en mængde symbolske integrationsregler ind, som det kan bruge til at løse de opgaver du kommer med, men hvis du kommer med en opgave den ikke har en regel eller kombination af regler til at løse, har den ingen ‘bevidsthed’ der gør at den kan opfinde en ny regel. Men det kan mennesker og det er mennesker der har lagt alle reglerne ind i programmet.

    Computere er som sagt gode til at gøre alle de ting vi er mindre gode til, dvs. regne og arbejde på store datamængder, til gengæld er de elendige til nytænkning.

    Kim Michelsen

    5 marts 2009 at 21:08


Skriv et svar

Udfyld dine oplysninger nedenfor eller klik på et ikon for at logge ind:

WordPress.com Logo

Du kommenterer med din WordPress.com konto. Log Out / Skift )

Twitter picture

Du kommenterer med din Twitter konto. Log Out / Skift )

Facebook photo

Du kommenterer med din Facebook konto. Log Out / Skift )

Google+ photo

Du kommenterer med din Google+ konto. Log Out / Skift )

Connecting to %s

%d bloggers like this: