Ein Sprachmodell schlägt vor, eine Rechnung entscheidet.

Ein Sprachmodell ist gut darin, aus einem Auftrag und einem Kontext einen Vorschlag zu formulieren, Zusammenhänge zu erkennen und Entwürfe zu schreiben. Es rechnet nicht im strengen Sinn. Es gibt Wörter aus, die nach seinem Training wahrscheinlich folgen. Bei Aufgaben mit festen Bedingungen, etwa Grenzen, Reihenfolgen und Summen, liefert es oft richtige Antworten und manchmal falsche, und beide klingen gleich sicher.

Die Forschung beschreibt dieses Verhalten als Halluzination: Ausgaben, die flüssig und überzeugend wirken und nicht gedeckt sind. Wer eine Handlung mit Folgen davon abhängig macht, ob ein solcher Text stimmt, verlässt sich auf eine Quote und nicht auf eine Garantie.

Eine Rechnung liefert eine Antwort mit einer Begründung, die sich unabhängig prüfen lässt. Ein SMT-Löser entscheidet, ob eine Formel über Zahlen und Wahrheitswerten eine erfüllende Belegung hat. Fragt man ihn nach dem Gegenteil der Regel und er findet keine, gilt die Regel für jeden zugelassenen Zustand, nicht nur für die ausprobierten. Findet er eine, ist sie das Gegenbeispiel.

Für Messunsicherheit gibt es die Rechnung mit Intervallen. Sie schließt jeden möglichen Wert ein und zerlegt, wo die Entscheidung offen ist. Bleibt ein Rest unentschieden, sagt sie das, und es gibt keine Freigabe.

Beides lässt sich verbinden. Das Sprachmodell schlägt eine Handlung vor, der Löser prüft sie gegen die Regeln, und ein Gegenbeispiel geht an das Sprachmodell zurück, das etwas anderes vorschlägt. Das Muster ist in der Programmsynthese unter dem Namen Gegenbeispiel-gesteuerte Synthese bekannt. Es setzt die Stärke des Sprachmodells, viele Möglichkeiten zu erzeugen, mit der Stärke der Rechnung zusammen, jede einzelne zu verwerfen oder zu belegen.

Der Rückweg ist begrenzt: nach wenigen Runden geht der Fall mit allen Gegenbeispielen an eine Person. Das Sprachmodell erhält nur, was der Auftrag lesen darf.

KALKÜL ist die Stelle, an der eine Handlung vor ihrer Ausführung gerechnet wird. Es hält Regeln als Formeln mit Version, prüft sie mit einem Löser und mit Intervallen und schreibt das Ergebnis als Nachweis auf: Datensatz, Prüfwert, Signatur, Zeitstempel. Wer das Ergebnis bezweifelt, rechnet es ohne KALKÜL nach. Gebaut ist heute ein Demonstrator, der im Browser eine Bahn mit ihrer Unsicherheit gegen drei Regeln rechnet; der Löser und der signierte Nachweis sind Bauweise.

Dazu kommt die Optimierung für Fälle, in denen nicht gefragt ist, ob eine Handlung geht, sondern welche die beste ist, und die Rechnung von Varianten als Szenarien, bevor eine gilt.

Eine Rechnung ist so gut wie ihre Voraussetzungen. Drei Fehlerquellen bleiben: Die Formel gibt den Wortlaut der Vorschrift falsch wieder, der Zustand, von dem sie ausgeht, ist falsch, oder die Annahmen sind es. KALKÜL versucht, jede davon sichtbar zu machen: Die Formel hat Testfälle und einen Verantwortlichen, der Zustand trägt seine Herkunft, die Annahmen sind Intervalle mit Urheber. Eine falsche Vorschrift korrigiert es nicht.

Dazu kommt das Unentschieden. Es ist ein ehrliches Ergebnis, und es ist unbequem, weil es keine Freigabe gibt. Das System nimmt diese Unbequemlichkeit in Kauf, statt zugunsten der Handlung zu raten.