KI vs. Halteproblem
-
Das Halteproblem besagt doch, dass es nicht möglich ist mit einem Program zu berechnen, ob ein Programm für eine bestimmte Eingabe terminiert.
Wenn man jetzt eine KI hätte, die Programmcode verstehen kann, dann müsste diese doch auch sagen können, ob das Programm terminiert oder nicht oder ob ein Widerspruch im Programm vorliegt.
Bedeutet das jetzt, dass es keine solche KI geben kann oder das das Halteproblem doch gelöst werden kann?
Oder hab ich nen Denkfehler drin?
-
---
-
ja, du kannst keine KI schreiben, die sowas versteht.
aber vielleicht solltest du dir pclint anschauen.
-
Ich will sowas nicht schreiben. Ist ne rein theoretische frage.
-
Wie Du richtig bemerkt hast würde so ein Programm das Halteproblem lösen. Dieses ist aber nicht lösbar, also kann es das Programm nicht geben.
Es stimmt übrigens auch nicht, dass das ne KI direkt entscheiden kann, ob ein Programm hält, wenn sie den Code verstanden hat.
Nimm folgendes einfache Programm:
Eingabe: eine natürliche Zahl n(>=1).
solange n!=1
wenn n gerade dann n/=2
sonst n = 3n+1Gib aus "Fertig"
Das ist ein sehr einfaches Programm, den Code davon kann man verhältnismäßig leicht verstehen. Trotzdem ist die Analyse davon offen. Es ist nicht bekannt, ob das Programm für jedes n als Eingabe terminiert.
-
Das Problem ist also, dass das verstehen des Codes nicht dazu führt, dass man sagen kann ob ein Programm terminiert. Also brauchten wir eine KI die ein unlösbares Problem löst. Das wird schwierig.
PS:
Wieso klaut der Server mir immer das m im Namen? Ich versuch es mal mit 2.
-
GedankenAusStaub&Stro schrieb:
Das Halteproblem besagt doch, dass es nicht möglich ist mit einem Program zu berechnen, ob ein Programm für eine bestimmte Eingabe terminiert.
...Die Annahme gilt nur für symbolische Verarbeitung (Turing Maschine). In der konnektivistischen Verarbeitung lässt sich das nicht so einfach sagen.
-
Dann bräuchtest Du aber auch irgendne andere Art von Rechner, die sich offensichtlich nicht mit nem normalen Rechner emulieren lässt.
-
naja, für so einen realen rechner existiert ja auch nicht wirklich ein halteproblem. so ein pc hat nunmal nur endlich viele zustände und lässt sich somit auch als riesigen endlichen automaten darstellen in welchem eine ki dann auch das halteproblem lösen kann.
-
*plonk*
Hab ich schonmal angemerkt, dass ich Argumente dieser Art für unglaublich dämlich halte?
-
Jester schrieb:
*plonk*
Hab ich schonmal angemerkt, dass ich Argumente dieser Art für unglaublich dämlich halte?
meinst du jetzt mich? warum? das Collatz-Problem auf einem realen rechner landet entweder in einem zyklus (der erkannt werden kann) oder es stößt an die grenzen des datentyps in dem dein n gespeichert wird (im zweifeilsfall duruch die größe des speichers beschränkt) oder es terminiert.
-
Ja genau. Und alle unsere Probleme sind in konstanter Zeit lösbar. Schließlich gibt's nur ne konstante Anzahl an möglichen Zuständen.
-
GedankenAusStaub&Stro schrieb:
Das Halteproblem besagt doch, dass es nicht möglich ist mit einem Program zu berechnen, ob ein Programm für eine bestimmte Eingabe terminiert.
Wenn man jetzt eine KI hätte, die Programmcode verstehen kann, dann müsste diese doch auch sagen können, ob das Programm terminiert oder nicht oder ob ein Widerspruch im Programm vorliegt.
Bedeutet das jetzt, dass es keine solche KI geben kann oder das das Halteproblem doch gelöst werden kann?
Oder hab ich nen Denkfehler drin?Du machst den Fehler die Implikation des Halteproblems nicht zu verstehen. Es ist bewiesen dass das Halteproblem für manche eingaben unlösbar ist, nicht von einem Programm unlösbar, sondern überhaupt unlösbar.
Auf Deutsch: auch für Menschen unlösbar.
Daher gibt es auch keine sinnvolle Aussage über KIs die man daraus herleiten könnte, ausser dass es eben für KIs genauso unlösbar bleiben wird wie für Menschen.
-
Jester schrieb:
Ja genau. Und alle unsere Probleme sind in konstanter Zeit lösbar. Schließlich gibt's nur ne konstante Anzahl an möglichen Zuständen.
in gewisser weise ja
aber es ist doch gar nicht mal unwahrscheinlich das wir in 50 jahren genug rechenpower haben um mit einer "ki" zu überprüfen ob ein programm auf einem gegebenen system die möglichkeit hat in einer endlosschleife zu landen.
sowas können wir doch heute für rechner von vor 50 jahren auch durchsimulieren.
-
borg schrieb:
aber es ist doch gar nicht mal unwahrscheinlich das wir in 50 jahren genug rechenpower haben um mit einer "ki" zu überprüfen ob ein programm auf einem gegebenen system die möglichkeit hat in einer endlosschleife zu landen.
sowas können wir doch heute für rechner von vor 50 jahren auch durchsimulieren.Doch, ist es. Die Anzahl der Zustände von Rechnern wächst doppelt exponentiell. Heutzutage ist man da wohl etwa bei 2^4.000.000.000.000 Zuständen (wenn man mal eine moderne Festplatte als Größenordnung nimmt). Das sind Größenordnungen, die man nicht mehr fassen kann. ...viel mehr Zustände, als es Teilchen im Universum gibt. Wie willst Du da feststellen, dass Du schonmal in einem bestimmten Zustand warst?
-
Gregor schrieb:
borg schrieb:
aber es ist doch gar nicht mal unwahrscheinlich das wir in 50 jahren genug rechenpower haben um mit einer "ki" zu überprüfen ob ein programm auf einem gegebenen system die möglichkeit hat in einer endlosschleife zu landen.
sowas können wir doch heute für rechner von vor 50 jahren auch durchsimulieren.Doch, ist es. Die Anzahl der Zustände von Rechnern wächst exponentiell. Heutzutage ist man da wohl etwa bei 2^4.000.000.000.000 Zuständen (wenn man mal eine moderne Festplatte als Größenordnung nimmt). Das sind Größenordnungen, die man nicht mehr fassen kann. ...viel mehr Zustände, als es Teilchen im Universum gibt. Wie willst Du da feststellen, dass Du schonmal in einem bestimmten Zustand warst?
unsere rechenleistung wächst auch exponetiell (moorsches law).
auch heute schon können modelchecker wie NuSMV algorithmen mit mehr als 10^100 zuständen verifizieren (das sind imo auch schon mehr als atome im universum). das geht in dem man hierarchien schafft und sachen gleich für einen ganzen haufen zustände ausschließt. NuSMV benutzt dafür glaub ich sogar einfach ROBDDs, das ist noch nichtmal kompliziert.
-
borg schrieb:
unsere rechenleistung wächst auch exponetiell (moorsches law).
Ich möchte darauf hinweisen, dass ich meinen Beitrag zwischenzeitlich editiert habe.
PS: Du wirst nicht generell Zustände ausschließen können. ...nur für bestimmte Algorithmen. Es ist nicht schwer, sich Algorithmen auszudenken, die zyklisch alle Zustände durchlaufen, oder eben nach dem Durchlauf aller Zustände terminieren.
-
Gregor schrieb:
PS: Du wirst nicht generell Zustände ausschließen können. ...nur für bestimmte Algorithmen. Es ist nicht schwer, sich Algorithmen auszudenken, die zyklisch alle Zustände durchlaufen, oder eben nach dem Durchlauf aller Zuytände terminieren.
ja, mit sowas hätte NuSMV vermutlich probleme. ich würde es trotzdem nicht ausschließen das eine maschine in 50 jahren vielleicht dazu fähig ist erstmal die korrektheit von 2^3.900.000.000.000 der zustände eines pcs für ein bestimmes programm mit hilfe eines induktionsbeweises oder sonstwas zu verifizieren und so die anzahl der zu überprüfenden zustände erheblich zu verkleinern.
-
borg schrieb:
ich würde es trotzdem nicht ausschließen das eine maschine in 50 jahren vielleicht dazu fähig ist erstmal die korrektheit von 2^3.900.000.000.000 der zustände eines pcs für ein bestimmes programm mit hilfe eines induktionsbeweises oder sonstwas zu verifizieren und so die anzahl der zu überprüfenden zustände erheblich zu verkleinern.
Ist zwar nur ein Beispiel, aber ich kann nicht widerstehen. Sorry:
2^4.000.000.000.000 - 2^3.900.000.000.000 = 2^4.000.000.000.000
Zumindest mit einer sehr hohen Genauigkeit.
Sicherlich kann die Anzahl der Zustände für bestimmte Programme reduziert werden. Das Halteproblem bezieht sich aber nicht auf bestimmte Programme, sondern generell auf beliebige Programme als Eingabe für Deinen Verifizierer. Wenn Du die Annahme machst, dass Du die Anzahl der Zustände stark verringern kannst, dann sieht das für mich erstmal so aus, als ob Du die Menge der Programme, die Du Deinem Verifizierer vorwirfst stark einschränkst. Da müsstest Du erstmal erklären, warum das nicht so sein sollte. Warum Du an dieser Stelle nicht den Gültigkeitsbereich des Halteproblems verlässt (abgesehen davon, dass Du ihn vorher schon durch die Anzahl der Zustände eingeschränkt hast).
-
Gregor schrieb:
Sicherlich kann die Anzahl der Zustände für bestimmte Programme reduziert werden. Das Halteproblem bezieht sich aber nicht auf bestimmte Programme, sondern generell auf beliebige Programme als Eingabe für Deinen Verifizierer. Wenn Du die Annahme machst, dass Du die Anzahl der Zustände stark verringern kannst, dann sieht das für mich erstmal so aus, als ob Du die Menge der Programme, die Du Deinem Verifizierer vorwirfst stark einschränkst. Da müsstest Du erstmal erklären, warum das nicht so sein sollte. Warum Du an dieser Stelle nicht den Gültigkeitsbereich des Halteproblems verlässt (abgesehen davon, dass Du ihn vorher schon durch die Anzahl der Zustände eingeschränkt hast).
naja ich hab ja nicht vor das halteproblem zu lösen, dass das nicht geht ist mir bewusst.
der thread ersteller schrieb:
Wenn man jetzt eine KI hätte, die Programmcode verstehen kann, dann müsste diese doch auch sagen können, ob das Programm terminiert oder nicht oder ob ein Widerspruch im Programm vorliegt.
und ich behaupte das wird für viele dinge, vor allem im embedded bereich möglich sein. das hat aber nix mit dem halteproblem zu tun.
