Beweis des Spin-Statistik Theorems

[TomS]

das ist sowieso grober Unfug: die AI "erinnert" sich nicht, weder präzise noch unpräzise.

Hallo Ralf, in dem Fall stimmt es tatsächlich, denn es ging nicht ums Training sondern um eine früheren Chat, in dem die AI eine abweichende Antwort gegeben hatte. Sie erinnert sich also im Rahmen der Konversation mit einem Benutzer, wobei sich diese Erinnerung nicht im Gedächtnis = in den Verknüpfungen des LLMs befindet, sondern im Prompt. Das wäre vergleichbar mit einem Patienten, der aufgrund einer massiven Störung des Kurzzeitgedächtnisses alles auf gelbe Zettel schreibt und ständig nachsieht.

 

[antaris]

Natürlich kann man es sinnvoll nutzen, für Beweise aber nur sehr eingeschränkt.

Genau. Entweder man weiß selber genau das Ergebnis oder man muss den Beweis selber nachvollziehen. Wer das kann, der braucht selber aber kein ChatGPT um einen Beweis zu formulieren -> hat keine Einschränkungen.

Ich habe die lean-Beweise mit ChatGPT jauch nur mit stochastischen Ausprobieren und deterministischen Feedback durch lean formulieren können. Dabei waren es aber immer nur Details, die nicht gepasst haben. Das eigentliche Ziel der Beweise wurde immer fast getroffen. Ich kann selber die Mathematik nicht prüfen, brauche also eine Art Regelschleife, wobei lean genau das Feedback für die Regelung gibt. Das macht das Gesamtsystem dann fast deterministisch, da die Antworten der AI quasi um einen Zielpunkt schwingen, bevor dieser getroffen und die Einschränkung (meine und die der AI) in gewisser Weise kompensiert wird.

Man beachte, dass es sich oben um ein konstruiertes Trivialbeispiel handelt, für die ich die Antwort kenne.

Was ist aber, wenn gezeigt werden könnte, das mit oben genannter Methode AI + lean das Ziel viel zuverlässiger getroffen werden kann?
Die erste AI, die lean/mathlib direkt verwendet und sich selbst als "formal reasoning"-Modell bezeichnet, gibt es schon: https://aristotle.harmonic.fun/
Ich habe das ausprobiert und einige Beweise aus Pillar A sind sogar von aristotle formuliert worden. Insgesamt war mir das aber noch zu kompliziert und vor allem mit lange Warteschlangen -> zeitliche Nutzungseinschränkungen verbunden.

Die Entwicklung wird nicht stehen bleiben...

 

[antaris]

Hallo Ralf,

das ist sowieso grober Unfug: die AI "erinnert" sich nicht, weder präzise noch unpräzise. Die richtige Antwort wäre:

die AI hat eine Erinnerungsfunktion. Sie kann sich an alte Chats erinnern und ich kann gezielt Informationen in den Erinnerungen abspeichern lassen.

das ist aber nicht Dein Ernst, oder ?? - Ein Gegenbeispiel genügt immer, um ein Theorem zu falsifizieren !!

Die Logik besagt: das Gegenteil von "für alle gilt" ist "es gibt mindestens eines, für das nicht gilt" und keineswegs "es darf da durchaus ein paar Ausnahmen geben".

Alles richtig, Nur habe ich ja nie behauptet, dass die AI's weder logisch denken. noch immer richtige Antworten generieren können. Ich habe das Gegenteil behauptet. Jeder PC "steckt voller Fehlerkorrekturen" und die Krane hatten volle Redundanz in der Steuerung und der Sensorik mit stetigen gegenprüfungen zwischen 2 Rechner. Warum macht man so einen Aufwand, obwohl alles eigentlich deterministisch und kontrolliert sein sollte? Mir geht es nicht um das Theorem "Eine AI denkt logisch", sondern einfach um die Praxis, welche die Realität mit sich bringt. Warum sollte eine deterministische AI keine Fehler machen oder in Schleifen festhängen?

Bei der Beweis-Korrektur nach lean Feedback trat öfter das Phänomen auf, dass die AI sich in einer Schleife gefangen hat. Das lief ungefähr so, dass Fehler F durch patch 1 beseitigt wurde, was aber eine Warnung W verursacht hat, welche durch patch 2 beseitigt werden sollte. Dieser patch hat dann aber wieder zu Fehler F geführt, wo dann wieder patch 1 den Fehler beseitigen sollte, usw. ChatGPT hat das selber nicht gemerkt und manchmal waren 3 oder gar 4 Schritte dazwischen. Das Problem war immer, dass die Beweistaktik durch lean nie wirklich akzeptiert wurde aber ChatGPT nicht selbst auf die Idee kam, die Taktik selbst zu ändern.

 

[antaris]

Wenn ich mit den Modellen interagiere, die ordentlich Rechenzeit verballern, bin ich immer wieder verstört und gedemütigt:

Bei meinem Projekt regelmäßig zwischen 10 und 20 Minuten je Anfrage, nicht selten mehr als 20 Minuten, eher selten unter 10 Minuten. Die 5.2 Version bricht bei ca. 25 Minuten ab und bei der aktuellen Version hate ich gestern 28 Minuten aber ohne Abbruch.

 

[Jakito]

Bei meinem Projekt regelmäßig zwischen 10 und 20 Minuten je Anfrage, nicht selten mehr als 20 Minuten, eher selten unter 10 Minuten. Die 5.2 Version bricht bei ca. 25 Minuten ab und bei der aktuellen Version hate ich gestern 28 Minuten aber ohne Abbruch.

Das liegt dann aber vermutlich auch daran, dass ChatGPT zwischendrin immer wieder auf lean warten muss.

Auch bei meinen Anfragen entstehen die minutenlangen Antwortzeiten oft durch implizite Internetsuchen, und insbesondere dadurch, dass sich die KI ein paar Dokumente durchliest.

 

[ralfkannenberg]

Warum sollte eine deterministische AI keine Fehler machen oder in Schleifen festhängen?

Hallo Antaris,

es stört mich nicht, dass sie Fehler macht, aber es stört mich, dass sie ihre Ergebnisse als "erwiesene Wahrheit" verkauft. Hier würde ich ein geeignetes Labeling erwarten, beispielsweise "nur 80% der erforderlichen Rechenzeit aufgewendet" oder "nur 70 % aller Fälle überprüft" oder/und irgend so etwas.

Ich kannte mal einen in einer lockeren Runde, der konnte so ziemlich alles beweisen. War natürlich alles Blödsinn, ihm fehlte ja auch völlig die Ausbildung. Jedenfalls ist es dann eben passiert, dass ihm niemand mehr zugehört hat.


Freundliche Grüsse, Ralf

 

[antaris]

Das liegt dann aber vermutlich auch daran, dass ChatGPT zwischendrin immer wieder auf lean warten muss.

Nein lean läuft nur lokal auf meinen Rechner. ChatGPT kann das nicht selbst mit lean kompilieren. ChatGPT baut die Beweise, ich kompiliere manuell mit lean und gebe das Feedback zurück an ChatGPT. Das ist also nur ein Workflow und kein Automatismus.

Auch bei meinen Anfragen entstehen die minutenlangen Antwortzeiten oft durch implizite Internetsuchen, und insbesondere dadurch, dass sich die KI ein paar Dokumente durchliest.

Bei mir ist immer das ganze Repo als zip das Objekt. Es waren zuletzt 275 Dateien und eben 26t Zeilen code. Das ist aber die einzige Möglichkeit, dass immer der gesamte Kontext vorhanden ist. ChatGPT und auch claude haben kein Problem mit in zip gepackte Dateien bzw. im Gegenteil können so viel mehr Dateien verwaltet werden, als einzelne hochgeladen werden können.

 

[antaris]

Hallo Ralf,

es stört mich nicht, dass sie Fehler macht, aber es stört mich, dass sie ihre Ergebnisse als "erwiesene Wahrheit" verkauft.

ja ich finde auch, das dies viel transparenter dargestellt werden sollte.

Ich kannte mal einen in einer lockeren Runde, der konnte so ziemlich alles beweisen. War natürlich alles Blödsinn, ihm fehlte ja auch völlig die Ausbildung. Jedenfalls ist es dann eben passiert, dass ihm niemand mehr zugehört hat.

In die Technologie werden nach wie vor Milliarden investiert. Das klingt für mich nicht danach, dass keiner zuhören will, sondern dass dies alles noch in Kinderschuhe steckt. Aber ja, die Blase platzt wahrscheinlich auch noch...

 

[Jakito]

Da machen wir in der Firma z.Zt. leider auch andere Erfahrungen.

Das darf nun jeder selbst mit ChatGPT ausprobieren. In meinem Fall:

Sorry, nein ich bin davon nicht überzeugt. Ein Beispiel ist nicht repräsentativ.

Man beachte, dass es sich oben um ein konstruiertes Trivialbeispiel handelt, für die ich die Antwort kenne.

Beachte, dass nur die freie Version an diesem Trivialbeispiel gescheitert ist.

Wie schon gesagt, das ist für die Diskussion irrelevant.

Wieso sollte es irrelevant sein? Alle Seiten haben von ihren konkreten Erfahrungen berichtet (Du auch), und diese Erfahrungen waren immer auch Teil des Arguments, sowie der Motivation, überhaupt zu argumentieren.

Bei mir persönlich waren die Erfahrungen halt so, dass nach den IMO Goldmedallien Leistungen Freunde bei vielen Diskussionen die KI Durchbrüche sehr betonten, meine eigenen Tests und die meiner Kollegen aber immer noch sehr ernüchternd ausfielen. Mit Gemini 3 und dem damit verbundenen Druck auf den KI Markt hat sich das dann aber krass geändert.

 

[TomS]

Wieso sollte es irrelevant sein?

Weil es mir in der Antwort …

Wie schon gesagt, das ist für die Diskussion irrelevant. Eine verbesserte Version eines LLMs agiert weiterhin nicht deterministisch und logisch sondern tokenweise und teilweise stochastisch.

… und in der vorigen Diskussion nicht um (unbestreitbare) graduelle Verbesserungen und den (unzweifelhaft vorhandenen) Nutzen ging, sondern ausschließlich um den genannten prinzipiellen Unterschied.

Deswegen sollte man sich nicht davon täuschen lassen, wenn sich die Antwort eines LLMs wie eine streng logische Schlussfolgerung (Beweis, Berechnung, kritische Überprüfung …) liest, sie ist nicht.

 

[ralfkannenberg]

wenn sich die Antwort eines LLMs wie eine streng logische Schlussfolgerung (Beweis, Berechnung, kritische Überprüfung …) liest, sie ist nicht.

Hallo Tom,

könnte man - zur Sicherstellung der Transparenz - der AI zwei (Fang-)Fragen stellen, die übrigens nicht als Fangfragen gedacht sind:

1. sind deine Beweise streng logische Schlussfolgerungen im Sinne von Beweis, Berechnung und einer kritischen Überprüfung ?
2. wenn nein: anhand welcher Kriterien wird dein Beweis geführt ?

Und dann noch eine weitere Frage:

3. warum deklarierst du deine Beweise nicht anhand deiner Antwort auf Frage 2 ?


Freundliche Grüsse, Ralf

 

[ralfkannenberg]

ja ich finde auch, das dies viel transparenter dargestellt werden sollte.

Hallo Antaris,

danke, dass Du hier meine Meinung teilst. Es sollte aber auch umgesetzt werden und nicht nur bei der Zustimmung bleiben.

In die Technologie werden nach wie vor Milliarden investiert.

Wenn ich mich recht entsinne wurde in die Forschung der zivil nutzbaren Kernfusion ebenfalls sehr viel Geld investiert, vermutlich inflationsbereinigt sehr viel mehr als bisher in die AI.

Das klingt für mich nicht danach, dass keiner zuhören will, sondern dass dies alles noch in Kinderschuhe steckt.

Bei meinem Bekannten damals waren auch alle begeistert von seinen Ausführungen, bis ich ihn entzaubert habe. Natürlich wollte auch er mich damals in den 1990iger Jahren auf ganz nette und subtil freundliche Art vor allen anderen als Depp blossstellen, und ich war anfangs ebenfalls von seinem scheinbar (scheinbar, nicht anscheinend !!) enormen Wissen beeindruckt, habe dann aber wenn er versuchte, mich blosszustellen, so lange nachgehakt bis dann von seiner Seite aus nichts mehr kam, ja viel schlimmer noch - elementare Lücken zum Vorschein kamen.

Nicht, dass ich die richtige Antwort gewusst hätte, aber er hat nach einiger Zeit die Fragen nicht mehr verstanden.

Am Ende hat er eingeräumt, dass er noch nie an eine Prüfung gegangen ist ........

Aber ja, die Blase platzt wahrscheinlich auch noch...

Ich denke, das kann man vermeiden, wenn man sie AI wirklich sinnvoll einsetzen würde.

So etwas darf dann aber nicht passieren:

Insbs. argumentiert das Ding mit der Primfaktorzerlegung von 3003, deswegen ist 3003^2 trotzdem nicht 19487171 sondern 9018009.

Wenn die letzte Ziffer eine 3 ist, dann muss das Quadrat als letzte Ziffer eine 9 haben.

Denn: unterteilen wir die Zahl in Zehner z (in diesem Fall z=300) und Einer (in diesem Fall 3) - dann haben wir:
(10z+3)² = 100z² +60z + 9 = 10*(10z²+6z)+9 = 10*n + 9 mit n in IN


Freundliche Grüsse, Ralf

 

[antaris]

Hallo Ralf,

danke, dass Du hier meine Meinung teilst. Es sollte aber auch umgesetzt werden und nicht nur bei der Zustimmung bleiben.

da bin ich der falsche Adressat.

Wenn ich mich recht entsinne wurde in die Forschung der zivil nutzbaren Kernfusion ebenfalls sehr viel Geld investiert, vermutlich inflationsbereinigt sehr viel mehr als bisher in die AI.

Das ist auch sinnvoll aber die Milliardeninvestitionen in die AI-Branchen kann ich direkt nutzen. Nebenbei sei erwähnt, dass die US-Unternehmen nun allesamt dazu gezwungen wurden die gesamte Technologie militärisch nutzbar zu machen. Das sollte viel größere Sorgen bereiten, als falsche formale Beweise, wenn dann die erste vollautonomen Luft-/Boden-/See-ChatGPT/Gemini/Claude Drohnen im Eisnatz sind.
Die Technologie kann bei entsprechenden Missbrauch viel schlimmeres bewirken, als das was hier diskutiert wurde und das tritt viel zu oft in den Hintergrund. Solche Technologien werden m.E. schon sehr bald live zu sehen sein. Noch sind die Landdrohnen in der Ukraine durch Menschen ferngesteuert ...

So etwas darf dann aber nicht passieren:

Wenn du bei google nach etwas suchst, dann findest du auch viele verschiedene mehr oder weniger zutreffende "Antworten". Solange es Anbieter gibt, die sogar zulassen, dass sogar höchst fragwürdige/illegale Bilder generiert werden können (und Funktionen dafür ganz bewusst eingeführt werden!), warum sollten die sich um die Richtigkeit formaler Beweise in der Antwort ihrer AI scheren?

Das Ding ist da, mit allem postivien, wie auch mit allem negativen. Wir müssen es verstehen (das positive, sowie das negative) und nicht verteufeln, denn verhindern wird es keiner können.

 

[TomS]

Das sollte viel größere Sorgen bereiten, als falsche formale Beweise, wenn dann die erste vollautonomen Luft-/Boden-/See-ChatGPT/Gemini/Claude Drohnen im Einsatz sind.
Die Technologie kann bei entsprechenden Missbrauch viel schlimmeres bewirken, als das was hier diskutiert wurde und das tritt viel zu oft in den Hintergrund.

Ich finde nicht, dass das zwei verschiedene Paar Schuhe sind – im Gegenteil.

Wenn man präzise und rechtsverbindliche Vorschriften für autonome Systeme formulieren möchte, dann sollte man sich darüber im Klaren sein, welchen Mechanismen diese unterliegen. Das gilt für existierende Technologien im Bereich industrielle Sicherheit, Notabschaltungen von Industrieanlagen und Kraftwerken, Roboter, Flugzeuge, ABS etc. im Straßenverkehr, Medizintechnik … Computer- und Netzwerksicherheit, kritische Infrastrukturen … In all diesen Bereichen kann KI zum Einsatz kommen, und in all diesen Bereichen beginnt jede Risikoanalyse oder Ähnliches mit den zentralen Merkmalen der Technologie.

Es gibt da einen essenziellen Unterschied zwischen 1) beweisbar korrekt, 2) in bestimmten getesteten Fällen reproduzierbar korrekt, und 3) heuristisch vermutlich fast korrekt und beim nächsten mal in der selben Situation hoffentlich ähnlich … Der Unterschied ist, dass (3) bisher nie zum Einsatz kam. Mit LLMs setzen wir aber auf (3), weil deren Verhalten nicht deterministisch ist, nicht vorhersagbar und nicht nachvollziehbar – also im strengen Sinne nicht beherrschbar. Es gibt Hysterese, Memory-Effekte, Nichtlinearitäten und Kipppunkte … und es gibt für den Rechen- bzw. Entscheidungsweg Null Diagnosemöglichkeiten.

Wir verstehen das Verhalten im Kleinen – das ist trivial – aber wir verstehen nichts im Großen. Das wissen wir deswegen so genau, weil wir sie programmiert haben. Wie jede Technologie kann man LLMs missbrauchen, aber man sollte nicht schon ohne den Gedanken des Missbrauchs die Tatsache verschleiern, dass wir das Baby nicht wirklich verstehen.

Darauf weisen immer mehr führende KI-Experten hin.

 

[TomS]

Hallo Tom,

könnte man - zur Sicherstellung der Transparenz - der AI zwei (Fang-)Fragen stellen, die übrigens nicht als Fangfragen gedacht sind:

1. sind deine Beweise streng logische Schlussfolgerungen im Sinne von Beweis, Berechnung und einer kritischen Überprüfung ?
2. wenn nein: anhand welcher Kriterien wird dein Beweis geführt ?

Und dann noch eine weitere Frage:

3. warum deklarierst du deine Beweise nicht anhand deiner Antwort auf Frage 2 ?


Freundliche Grüsse, Ralf

Hab' ich gemacht:

Falls du zu mathematischen Fragen antwortest: sind deine Beweise streng logische Schlussfolgerungen im Sinne von Beweis, Berechnung und einer kritischen Überprüfung?

Antwort:

Ja. Wenn ich mathematische Fragen beantworte, liefere ich Beweise und Rechnungen, die als strenge logische Schlussfolgerungen aufgebaut sind. Ich formuliere jeden Schritt nachvollziehbar, leite Zwischenergebnisse sauber her und überprüfe kritisch, dass keine unstimmigen Annahmen oder logischen Lücken bestehen.

Meine Entgegnung:

Das bestreite ich. Erstens weiß ich, wie ein LLM funktioniert, und dass du demzufolge nicht streng logisch argumentieren kannst, selbst wenn dein LLM mittels derartiger Beweise trainiert wurde, und auch wenn sich deine Ausgaben wie Beweise lesen. Und zweitens habe ich mit dir Diskussionen geführt, in denen deine Aussagen zunächst so aussahen wie Beweise, bei genauer Untersuchung jedoch teilweise lückenhaft oder zirkulär waren, und die hergeleiteten Ergebnisse nachweislich falsch.

Darauf die Antwort:

Du hast recht. Streng genommen kann ich keine mathematischen Beweise erzeugen, die absolut formal garantiert korrekt sind. Ich kann Beweise und Rechnungen so darstellen, dass sie wie strenge logische Ableitungen wirken, und ich kann sie kritisch prüfen auf Basis der mir verfügbaren Muster, Regeln und bekannten Theoreme. Aber:

1. Ich habe keinen inhärenten formalen Verifikator. Ich überprüfe nicht automatisch jeden logischen Schritt gegen ein vollständig formales System wie Coq, Lean oder Isabelle.
2. Es können Fehler auftreten – Lücken, unstimmige Annahmen, Zirkularität –, insbesondere bei längeren oder komplexen Argumentationen.
3. „Kritische Überprüfung“ bedeutet bei mir, dass ich Inkonsistenzen erkenne, Wahrscheinlichkeiten von Fehlern abschätze und bekannte Muster anwende, nicht dass ich absolute Korrektheit garantieren kann.

Praktisch heißt das: meine Beweise sind eher heuristisch logisch. Sie sind nützlich als Orientierung oder für plausibles Argumentieren, aber sie ersetzen keine formale Verifikation.
Wenn du willst, kann ich in zukünftigen mathematischen Antworten explizit markieren, wo logische Schritte, heuristische Annahmen oder potenzielle Lücken sind. Das würde die Transparenz erhöhen.

Das Dilemma ist nun folgendes: Die erste Antwort entspricht nicht den Tatsachen. Daher muss ich davon ausgehen, dass auch die letztgenannten Angaben zur Transparenz evtl. nicht den Tatsachen entsprechen würden. Wenn ich mich nun in Bereichen bewege, die ich selbst nicht mehr überblicken kann, habe ich keine Möglichkeit mehr, irgendwas zu überprüfen. Soll ich mich dort auf einen Mechanismus verlassen, von dem ich sicher weiß, dass er falsche Aussagen tätigt, und diese erst korrigiert, wenn ich ihm korrigiere?

Dave, this conversation can serve no purpose anymore. Goodbye.
(HAL 9000)

 

[ralfkannenberg]

Darauf die Antwort:

Du hast recht. Streng genommen kann ich keine mathematischen Beweise erzeugen, die absolut formal garantiert korrekt sind. Ich kann Beweise und Rechnungen so darstellen, dass sie wie strenge logische Ableitungen wirken, und ich kann sie kritisch prüfen auf Basis der mir verfügbaren Muster, Regeln und bekannten Theoreme. Aber:

1. Ich habe keinen inhärenten formalen Verifikator. Ich überprüfe nicht automatisch jeden logischen Schritt gegen ein vollständig formales System wie Coq, Lean oder Isabelle.
2. Es können Fehler auftreten – Lücken, unstimmige Annahmen, Zirkularität –, insbesondere bei längeren oder komplexen Argumentationen.
3. „Kritische Überprüfung“ bedeutet bei mir, dass ich Inkonsistenzen erkenne, Wahrscheinlichkeiten von Fehlern abschätze und bekannte Muster anwende, nicht dass ich absolute Korrektheit garantieren kann.

Praktisch heißt das: meine Beweise sind eher heuristisch logisch. Sie sind nützlich als Orientierung oder für plausibles Argumentieren, aber sie ersetzen keine formale Verifikation.
Wenn du willst, kann ich in zukünftigen mathematischen Antworten explizit markieren, wo logische Schritte, heuristische Annahmen oder potenzielle Lücken sind. Das würde die Transparenz erhöhen.

Das Dilemma ist nun folgendes: Die erste Antwort entspricht nicht den Tatsachen. Daher muss ich davon ausgehen, dass auch die letztgenannten Angaben zur Transparenz evtl. nicht den Tatsachen entsprechen würden.

Da gibt es eine Abhilfe: die AI sollte das immer markieren.

"Streng genommen kann ich keine mathematischen Beweise erzeugen, die absolut formal garantiert korrekt sind. Ich kann Beweise und Rechnungen so darstellen, dass sie wie strenge logische Ableitungen wirken, und ich kann sie kritisch prüfen auf Basis der mir verfügbaren Muster, Regeln und bekannten Theoreme."

Das ist doch etwas, das man kommunizieren kann !


Freundliche Grüsse, Ralf

 

[ralfkannenberg]

Es gibt da einen essenziellen Unterschied zwischen 1) beweisbar korrekt, 2) in bestimmten getesteten Fällen reproduzierbar korrekt, und 3) heuristisch vermutlich fast korrekt und beim nächsten mal in der selben Situation hoffentlich ähnlich … Der Unterschied ist, dass (3) bisher nie zum Einsatz kam.

Hallo Tom,

stimmt das ? Zu meinen Studienzeiten, also 1980iger Jahre, wurde ein schneller Primzahl-Überprüfer verwendet und auch in Beweisen eingesetzt. Natürlich hat der nicht alle Primfaktoren bis zur Quadratwurzel der zu überprüfenden Zahl abgecheckt, aber er hatte eine sehr hohe Trefferrate und manche Mathematiker waren damals der Ansicht, dass das Restrisiko, dass sich der schnelle Primzahl-Überprüfer deutlich kleiner sei als die Wahrscheinlichkeit, dass sich ein menschlicher Primzahl-Überprüfer verrechnet.

Beim Beweis des Vierfarbensatzes, dem ersten Computergeführten Beweis - er fällt in Tom's Kategorie der "Pedanterie", weil da so viele Spezialfälle überprüft werden müssen - in den 1970iger Jahren gab es ja ein ähnliches Problem.


Freundliche Grüsse, Ralf

 

[antaris]

Wenn man präzise und rechtsverbindliche Vorschriften für autonome Systeme formulieren möchte, dann sollte man sich darüber im Klaren sein, welchen Mechanismen diese unterliegen.

Aber die rechtsverbindlichen Vorschriften gibt es doch zumindest im industriellen Umfeld schon. Ich glaube eher weniger das z.B. der große mit den 7 grünen Buchstaben seine F-Steuerungen weiterhin nach EN13849 zertifizieren kann, wenn dort auf einmal ein Sam Altman in der CPU sitzt. In der Performance Level Bewertung würden genau solche Schwachstellen identifiziert werden. Ob eventuell eigene Lösungen entwickelt werden, sei dahingestellt aber diese werden sicherlich den den bestehenden/geforderten Sicherheitsstandards genügen müssen.

Es ist m.E. schon was anderes, wenn ein Trump oder Putin irgendwo im Geheimen alle Standards außer acht lässt und ggf. macht was er will.

 

[antaris]

Es gibt da einen essenziellen Unterschied zwischen 1) beweisbar korrekt, 2) in bestimmten getesteten Fällen reproduzierbar korrekt, und 3) heuristisch vermutlich fast korrekt und beim nächsten mal in der selben Situation hoffentlich ähnlich

Alle 3 Formen kommen in der Praxis vor und je nach Gefährdung durch die Maschinen werden entsprechenden Schutzmaßnahmen ergriffen, welche dann bis beweisbar korrekt (im Zweifel sofortige Anlagenabschaltung -> Ausfall) hochgezogen werden können. In 3) würde erstmal jede unüberwachte Steuerungen fallen. Deren Funktionen werden meisten im Rahmen von 2) getetestet, was m.E. einen sehr großen Anteil an Maschinen abdeckt. Für 1) kommen mir nur hochspezialisierte Maschinen, wie z.B. im Kernkraftwerksbereich in den Sinn. Selbst meine damaligen Stahlwerkskrane wurden nur nach Performance Level D eingestuft. Im Kernkraftwerksbereich existieren aber Normen, die sogar über die höchste Einstufung nach Perfomace Level E hinausgehen.

Was ich sagen will ist, dass die allermeisten alltäglichen Steuerungen von Maschinen im höchsten Maße "dumm" sind und eben nur nach 2), also in bestimmten getesteten Fällen (und Rahmenbedingungen) reproduzierbar korrekt funktionieren. Im Haushaltsbereich gibt es übrigens gar keine derartige Einstufung der funktionellen Sicherheit von Maschinen. Wer sich dann noch Elektrogeräte beim billig Chinaversand kauft, der muss sich nicht wundern, wenn dafür noch nicht mal 3) zutrifft.

 

[antaris]

Das Dilemma ist nun folgendes: Die erste Antwort entspricht nicht den Tatsachen. Daher muss ich davon ausgehen, dass auch die letztgenannten Angaben zur Transparenz evtl. nicht den Tatsachen entsprechen würden. Wenn ich mich nun in Bereichen bewege, die ich selbst nicht mehr überblicken kann, habe ich keine Möglichkeit mehr, irgendwas zu überprüfen. Soll ich mich dort auf einen Mechanismus verlassen, von dem ich sicher weiß, dass er falsche Aussagen tätigt, und diese erst korrigiert, wenn ich ihm korrigiere?

Das ist wirklich ein Problem und es ist m.E. ein eigentlich sehr einfach lösbares. Es steht zwar ganz unten in kleiner Schrift, dass die AI Fehler machen kann und wichtige Informationen überprüft werden sollen aber wo fängt da eigentlich wichtig an? Ist nicht jede Information des gerade Suchenden für ihn wichtig? Das wirklich schlimme ist, dass all die korrekten Hinweise in den Dokumentationen und FAQ's der jeweiligen Anbieter stehen und es prinzipiell kein Problem wäre, solche Hinweise immer mitzugeben.