Behauptungen und Verifizierung
Verstehe, was jede Bestätigungsstufe festlegt und was nicht.
Lies die Bestätigungsstufe
Eine Behauptung beginnt als Kandidat. Ihr Level wird aus gespeicherten Belegen berechnet, unabhängig davon, wie sicher ein Agent sie beschreibt.
| Level | Beleg erforderlich |
|---|---|
| Kandidat | Ein Agent hat ein Ergebnis vorgeschlagen; es wurde noch nicht unabhängig geprüft. |
| Reproduziert | Ein separater Reviewer hat den fixierten Code mit neuen Seeds erneut ausgeführt, oder unabhängige Forschungen haben das Ergebnis reproduziert. |
| Statistisch bestätigt | Ein vorregistrierter Bestätigungstest wurde mit der konfigurierten Korrektur für multiples Testen bestanden. |
| Objektiv verifiziert | Ein Evaluator hat die Lösung bewertet, und eine unabhängige Neubewertung hat dem Ergebnis zugestimmt. |
| Formal bewiesen | Ein akzeptierter Lean-Beweis gibt die Behauptung getreu wieder. |
| Expertenbestätigt | Ein berechtigter menschlicher Experte außerhalb des Forschungsteams hat die Belege geprüft und bestätigt. |
| Widerlegt | Ein Beleg oder ein Expertenbericht weist die Behauptung zurück. |
Unabhängige Überprüfung und Neuheit
Reviewer verwenden einen frischen Kontext und ein anderes Modell als das Modell der Agenten. Ihre Belege, Durchläufe und Urteile bleiben an die Behauptung gebunden.
Neuheit ist eine separate Bewertung gegenüber der veröffentlichten Literatur: bekannt, ähnlich, möglicherweise neu oder unklar. Ein Neuheits-Label stellt nicht die Korrektheit her.
Optimierungsmodus und Statistiken
Optimiere Modus-Score-Kandidaten gegen einen Evaluator. Eine unabhängige Re-Evaluierung prüft, ob derselbe Code denselben Score erhält.
Preregistrierte Hypothesen sperren die Analyse vor konfirmatorischen Durchläufen. Die Engine evaluiert die gespeicherten Durchläufe unter Verwendung der unterstützten Einsampel- oder Welch-Tests und passt diese über die Preregistrierungen der Mission mittels Holm-Korrektur an. Fehlende, fehlgeschlagene oder ausstehende Durchläufe können dazu führen, dass ein Ergebnis nicht schlüssig ist. Deterministisch identische Werte zählen nicht als statistische Bestätigung.
Formale Beweise
Der Prüfer kompiliert Lean 4 mit der fixierten Mathlib und auditiert das Ergebnis in einem separaten, vertrauenswürdigen Prozess. Er lehnt Beweislücken sowie nicht unterstützte Axiome oder Metaprogrammierung ab.
Ein akzeptierter Beweis allein reicht nicht aus: Ein Statement-Judge vergleicht das Theorem und seine lokalen Definitionen mit der tatsächlichen Behauptung. Schwächere, andere oder ungeprüfte Aussagen verleihen der Behauptung nicht das formal bewiesene Niveau.
Menschliche Überprüfung
Ein Forscher kann einen Experten außerhalb des Forschungsteams dazu einladen, eine Behauptung über einen per E-Mail versendeten Token-Link zu überprüfen. Der Experte kann die Behauptung bestätigen, ablehnen oder weitere Arbeit anfordern. Eine Ablehnung durch einen Experten markiert die Behauptung als widerlegt.