KALKÜL.
Erst rechnen, dann handeln.
Ein Mensch oder ein Agent schlägt eine Handlung vor. KALKÜL rechnet vorher nach.
- SchalthandlungEin Umschalten im Stromnetz.Regel: Keine Leitung wird überlastet.
- DosisDie Menge eines Wirkstoffs über die Zeit.Regel: Die Konzentration bleibt in ihren Grenzen.
- FlugbahnDer Weg eines Flugzeugs durch den Luftraum.Regel: Es bleibt immer genug Abstand.
Was KALKÜL von einer künstlichen Intelligenz unterscheidet.
- KALKÜL rechnet, es rät nicht.Dieselben Eingaben ergeben immer dasselbe Ergebnis.
- KALKÜL prüft alles, was möglich ist.Ein einziger möglicher Verstoß reicht für ein Nein.
- KALKÜL begründet jedes Ergebnis.Ein Nein nennt Regel und Zeitpunkt, ein Ja trägt ein Siegel zum Nachrechnen.
Das gilt überall, wo sich ein System mit Modell und Regeln beschreiben lässt.
Wofür
Für Systeme, in denen eine Abweichung nicht verziehen wird.
- Luftraum und Flugbahn‖p(t) − c‖ ≥ r für alle t
- WaffensystemeEinsatzregeln als Bedingung: Abstand, Zone, Freigabe
- Netze und SchaltungenN − 1: Iₖ ≤ Iₘₐₓ für jeden Ausfall k
- Medizin und Dosierungc_min ≤ c(t) ≤ c_max
- Bahn und SignalAbstand ≥ Bremsweg + Sicherheit
- Wasser und Reserveh(t) ≥ h_min für alle t
Wie die Prüfung läuft
Fünf Stufen, jede baut auf der vorigen auf.
(1)Modell
Das System steht als Gleichung. KALKÜL rechnet sie Schritt für Schritt vorwärts.
x(t + Δt) = f(x(t), u(t), w(t)) w ∈ W
(2)Regeln
Jede Regel zieht eine Grenze durch den Raum und gilt über die ganze Zeit.
∀ t ∈ [0, T]: g₁(x) ≥ 1 ∧ x₂ ≤ x₂,max ∧ x₂ ≥ x₂,min
(3)Hülle
Statt eines Punkts rechnet KALKÜL alle Zustände, die bei der Unsicherheit möglich sind. Zusammen ergeben sie die Hülle.
R(t) ⊇ { x(t) | w ∈ W } Intervalle, Zonotope
(4)Gegenbeispiel
Die Prüfung teilt den Raum in Kästen und zerlegt jeden, durch den eine Grenze läuft. Liegt ein möglicher Zustand jenseits, kippt das Urteil: KALKÜL nennt Zeitpunkt, Wert und Regel.
B ⊆ verboten ∧ B ∩ R ≠ ∅ ⇒ t* = min { t | R(t) ∩ verboten ≠ ∅ }
(5)Siegel
Findet die Suche bei einem anderen Vorschlag keinen solchen Zustand, ist jeder Kasten geprüft. KALKÜL hält den Prüfweg unter einem Siegel fest, das Dritte ohne Zugang nachrechnen können.
siegel = SHA-256(modell ‖ regeln ‖ eingaben ‖ prüfweg ‖ ergebnis)
Selbst prüfen
Wählen Sie einen Vorschlag und die Unsicherheit. KALKÜL sucht hier im Browser nach einem Gegenbeispiel.
Die Suche startet, sobald Sie wählen.
Modell der Rechnung mit Größen der Zeichnung, keine Messung.
Was nachvollziehbar bleibt
Was nach der Rechnung nachprüfbar bleibt.
- SimulationBelegBahn je Kandidat, mit Eingaben und ModellstandVorab rechnenEine vorgeschlagene Handlung wird am Modell durchgerechnet, bevor sie wirkt, Schritt für Schritt.
- SimulationBelegGegenbeispiel: Regel, Zeitpunkt t*, WertRegeln prüfenRegeln stehen als Bedingungen. Bricht eine Handlung eine davon, steht das Gegenbeispiel mit Zeitpunkt und Wert da.
- KonzeptBelegPrüfwert über Modell, Regeln, Eingaben, ErgebnisVersiegelnEingaben, Regeln und Ergebnis bekommen einen Prüfwert, den Dritte ohne Zugang zum System nachrechnen.
- KonzeptBelegBericht je Zeitraum: Handlung, Regel, PrüfwertNachweisenAlle geprüften Handlungen eines Zeitraums ergeben einen Bericht für Geschäftsführung und Prüfer.
Selbst bedienen
Die Software selbst bedienen.
Die Anwendungen laufen mit Beispieldaten. Die meisten starten direkt im Browser, ohne Konto.
Zu den AnwendungenAngebot · Bootcamp
Fünf Tage an einer Ihrer Regeln.
Wir nehmen eine Regel aus Ihrer Vorschrift. Am Ende steht sie als Bedingung, ein Prototyp rechnet sie auf Beispieldaten, und Sie entscheiden, ob es weitergeht.
- Tag 1 und 2Regel schreibenWortlaut, Grenzen und Ausnahmen als Bedingung.
- Tag 3 und 4RechnenModell anbinden, Kandidaten durchrechnen.
- Tag 5VorführenGegenbeispiel und Siegel zeigen, dann entscheiden.
StandDer Prüfraum rechnet hier im Browser, an einem Rechenmodell mit Größen der Zeichnung. Das Produkt ist Bauplan; für Netzmodelle und Regeln aus echten Vorschriften suchen wir Forschungspartner.