rei-verify

Widerlegungsmaschine (Refutation Machine) — Spezialisiert auf Negation statt Generierung. Validierungsinfrastruktur + MCP-Server.

Version: 0.1.0a1 (2026-08-19) — 4 Primitive + 4 Widerlegungswerkzeuge + 8 MCP-Werkzeuge + Integrationsdemo. Test 198/0 BESTANDEN.

Warum „Widerlegungsmaschine"

Generierung ist gesättigt. Widerlegung ist nicht gesättigt.

Aktuelle LLMs sind fließend. Sie können plausible Beweisstränge, plausiblen Code, plausible Theoreme-Namen ausgeben, unabhängig davon, ob sie wahr sind. Auch wenn Benchmarks bei 96% gesättigt sind, ändert sich diese Struktur nicht. Was der Welt fehlt, ist nicht eine „Maschine, die Plausibles erzeugt", sondern eine „Maschine, die Plausibles zuverlässig tötet".

Das Kernversprechen der Widerlegungsmaschine:

• Erhält man eine Behauptung, wird Rechenleistung für die Gegenbeispielsuche aufgewendet. Beweisversuche werden zurückgestellt.

• Wird kein Gegenbeispiel gefunden, wird explizit die „Form des durchsuchten Raums" zurückgegeben (keine Tarnung von Schweigen als Erfolg).

• Der Ausgabe wird zwingend eine „Stelle, an der die Behauptung bricht, wenn sie falsch wäre" beigefügt. Lean 4 sorry-Null ist der strengste Spezialfall davon.

• „Nicht widerlegt" und „wahr" werden auf Typebene als verschiedene Dinge behandelt.

Related MCP server: leanscreen

4-Wert-Urteil („Lügt niemals" – Kern-Disziplin)

class Verdict(str, Enum):
    CONFIRMED = "confirmed"           # post-condition PASS + marker 空
    REFUTED = "refuted"               # 具体的な counter-witness が 得られた
    HOLDING = "holding"               # counter-witness 未発見 かつ marker 非空
    INCOMPLETE_FRAME = "incomplete_frame"  # 主張自体が well-formed でない

Kein binäres TRUE/FALSE = nicht widerlegt ≠ wahr. Typisierung der 12-jährigen Holding-Disziplin des IUT.

„Tarnung von Schweigen als Erfolg wird unterbunden" – Typgarantie: Allen Urteilen außer CONFIRMED ist mindestens 1 IncompleteMarker (Dimension + was_versucht + was_nicht_versucht + Grund) zwingend erforderlich (Dataclass-Invariante, unverletzbar).

4 Primitive (rei_verify)

4 Widerlegungswerkzeuge (rei_verify.*)

Das Herzstück der Widerlegungsmaschine. Alle Werkzeuge geben VerdictWithMarkers (4-Wert-Urteil + Marker + Audit-Hashes) als konsistente Form zurück.

★ Nur refute_lean_source gibt CONFIRMED aus (nur Fälle, die der Lean 4-Kernel als sorry-frei bestätigt hat). Die anderen drei Werkzeuge geben stets REFUTED oder HOLDING zurück = „Abwesenheit eines Gegenbeispiels ist kein Beweis" – Disziplin auf Typebene.

8 MCP-Werkzeuge

Direkt von LLM-Clients wie Claude Desktop / Cursor / Cline aufrufbar:

MCP-sichere Ausdrücke sind eingeschränktes Eval = __import__ / exec / eval / open / __-Präfix werden vorab abgewiesen, Whitelist _SAFE_BUILTINS (abs/min/max/sum/len/int/float/str/bool/round/any/all/range) ist alles, was erlaubt ist.

Installation

pip install rei-verify           # core primitives (no external deps)
pip install rei-verify[mcp]      # + MCP server

oder aus dem Quellcode:

git clone https://github.com/fc0web/rei-verify.git
cd rei-verify
pip install -e .[mcp]

Erfordert Python 3.10+ (Dataclass + Enum + neue Typing-Funktionen). Die Kernprimitive funktionieren mit der Standardbibliothek allein (Import auch ohne mcp-Paket möglich).

Verwendung – Bibliothek

VerifiedExecution (benutzerdefiniert)

from pathlib import Path
from rei_verify import (
    Verdict, IncompleteMarker, PostCheckResult,
    VerifiedExecution, AuditChain,
)

audit = AuditChain(Path("./reasoning.jsonl"))
ve = VerifiedExecution(
    claim="1 + 1 == 2",
    pre_check=lambda: True,
    post_check=lambda r: PostCheckResult(refuted=(r != 2), markers=[]),
    audit=audit,
)
result = ve.run(lambda: 1 + 1)
# result.verdict == Verdict.CONFIRMED
# result.audit_hashes == [h1, h2, h3, h4, h5]  # 5 phase entry

refute_lean_source

from rei_verify.refute import refute_lean_source

result = refute_lean_source(
    claim="trivial True holds",
    lean_source="theorem trivial_true : True := trivial\n",
    audit=audit,
    theorem_name="trivial_true",
    timeout_sec=60,
)
# result.verdict == Verdict.CONFIRMED  (axiom-free, ~1200 ms)

Standard-allow_axioms = Mathlib-Basis [propext, Classical.choice, Quot.sound]. sorry / native_decide / unerlaubte Axiome werden an HOLDING weitergeleitet.

search_counterexample

from rei_verify.search import search_counterexample

result = search_counterexample(
    claim="no n in [1,100] equals 42",
    predicate=lambda x: x == 42,
    space=range(1, 101),
    audit=audit,
    space_description="range(1, 101)",
)
# result.verdict == Verdict.REFUTED  (witness marker: n=42)

• Erschöpfung → HOLDING (search_space-Marker, „Abwesenheit ≠ Beweis")

• Zeit-/Stichprobenbudget → HOLDING (compute_budget-Marker)

assert_breakpoints

from rei_verify.breakpoint import Breakpoint, assert_breakpoints

result = assert_breakpoints(
    claim="Collatz t1=1 orbits descend",
    breakpoints=[
        Breakpoint("n=27", assertion=lambda: descent(27), context={"n": 27}),
        Breakpoint("n=703", assertion=lambda: descent(703), context={"n": 703}),
        Breakpoint("n=6171", assertion=lambda: descent(6171), context={"n": 6171}),
    ],
    audit=audit,
    stop_on_first_failure=True,  # False で 全 breakpoint 実行 (集計目的)
)

• Beliebiger breakpoint False → REFUTED (Label + Kontext als Zeuge)

• Alle bestanden → HOLDING („aufgelistete Prüfpunkte erschöpft ≠ alle Fälle abgedeckt")

hold_verdict

from rei_verify.hold import hold_verdict

result = hold_verdict(
    claim="my analytical claim under investigation",
    markers=[
        IncompleteMarker(
            dimension="search_space",
            what_was_tried="5 counterexample approaches",
            what_was_not_tried="structural refutation via categorical semantics",
            reason="categorical angle deferred to next session",
        ),
    ],
    audit=audit,
    notes="manual reasoning pause",
    require_multi_dimension=True,  # 単一 dim なら augmentation marker 追加
)
# result.verdict == Verdict.HOLDING  (audit chain 4 phase entries + caller markers)

Verwendung – MCP (Claude Desktop)

claude_desktop_config.json:

{
  "mcpServers": {
    "rei-verify": {
      "command": "python",
      "args": ["-m", "rei_verify"]
    }
  }
}

oder (installiertes Skript):

{
  "mcpServers": {
    "rei-verify": {
      "command": "rei-verify"
    }
  }
}

MCP-Ausdrucksbeispiele (x bindet für Suche, ctx bindet für Haltepunkte):

{
  "tool": "search_counterexample_explicit",
  "arguments": {
    "chain_id": "chain-abc123",
    "claim": "no perfect square in [1,100] equals 42",
    "samples": [1, 4, 9, 16, 25, 36, 49, 64, 81, 100],
    "predicate_expr": "x == 42",
    "space_description": "perfect squares up to 100"
  }
}

{
  "tool": "assert_breakpoints_explicit",
  "arguments": {
    "chain_id": "chain-abc123",
    "claim": "Collatz t1=1 descent",
    "breakpoints": [
      {"label": "n=27 case", "assertion_expr": "ctx['descent'] < 0",
       "context": {"n": 27, "descent": -0.5}},
      {"label": "n=703 case", "assertion_expr": "ctx['descent'] < 0",
       "context": {"n": 703, "descent": 0.2}}
    ]
  }
}

Integrationsdemo

examples/collatz_t1_ones_lyapunov_demo.py – Collatz ungerade n mit trailing_ones(n)=1, Lyapunov-α-Abstiegsscan mit assert_breakpoints ausgeführt.

python examples/collatz_t1_ones_lyapunov_demo.py

Beispielausgabe (1.048.575 Stichproben / 76,7 ms):

α=0.5〜0.85: WITNESS  n=9         r(n)=0.885622  → α refuted ✓
α=0.9:       WITNESS  n=17        r(n)=0.905315  → α refuted ✓
α=0.93:      WITNESS  n=57        r(n)=0.930288  → α refuted ✓
α=0.95:      WITNESS  n=313       r(n)=0.950121  → α refuted ✓
α=0.97:      WITNESS  n=14,601    r(n)=0.970001  → α refuted ✓
α=0.99:      NO WITNESS in range  max r=0.981135 < 0.99  → α NOT refuted in sample

VERDICT: REFUTED  (α=0.99 が サンプル範囲 で 未 refute = finite absence report)
audit chain: 6 entries、 sha256 hash chain intact

Zeugen-n wachsen mit α-Verschärfung (n=9 → n=14.601) = r(n) → 1 für n → ∞ wird direkt als endliche Spiegelung beobachtet, das Werkzeug befolgt die Disziplin „Keine automatische Hochstufung endlicher Abwesenheit auf CONFIRMED". Detaillierter ehrlicher Umfang siehe Kommentare in der Demo.

Testabdeckung

Kumuliert 198/0 BESTANDEN (6 Testdateien):

# individual
python test/test_skeleton.py
python test/test_refute.py       # requires 'lean' on PATH for live smoke

# all
for f in test/test_*.py; do PYTHONIOENCODING=utf-8 python -u "$f" | tail -3; done

Für Betreuer: Einrichtung des PyPI Trusted Publishers

Die .github/workflows/publish.yml dieses Repos führt bei v-Tag-Push die Veröffentlichung auf PyPI in Produktion* durch + bei workflow_dispatch einen TestPyPI-Trockenlauf. Vor der Nutzung ist die Registrierung des Trusted Publishers auf beiden Seiten (PyPI / TestPyPI) sowie die Erstellung der GitHub-Umgebung erforderlich.

Ausführliche Schritte siehe TRUSTED_PUBLISHER_SETUP.md.

⚠️ Vor einem Tag-Push Doppelprüfung von workflow.yml + Trusted Publisher-Registrierung (Unfallvermeidung „Tag = Release-Trigger").

Design

Siehe DESIGN.md für die vollständige Begründung (8 Abschnitte):

• Ausgangspunkt des Designs (Rei-Stack 4 Prinzipien)

• Details der 4 Primitive

• Urteilstabelle (einzige Quelle der Wahrheit)

• Abbildung der 3+1 Widerlegungswerkzeuge

• Beziehung zum Framing-Drift-Detektor

• Nicht-Ziele (außerhalb des Rahmens für das Skelett)

• Abhängigkeiten (Absicht: null externe Abhängigkeiten)

• Ehrlicher Umfang

Verwandtes

• fc0web/rei-automator-mcp — Windows-PC-Automatisierungs-MCP, Herkunft von AuditChain (generische Extraktion von STEP 1340 AuditLogWriter)

• fc0web/grounded — Prosa-Grounding-Checker (2-stufige Verifikation)

• fc0web/grounding-check — SCPI-Hardware-Grounding-Checker

Autor

Nobuki Fujimoto

Lizenz

MIT (v0.x unwiderruflich). Ab v1.0+ möglicherweise AGPL-3.0 + kommerziell dual. Siehe LICENSE.

Ehrlicher Umfang (unverhandelbare Grenzen)

• (i) Die Widerlegungswerkzeuge des Skeletts arbeiten nur mit direkter Anbindung an Lean 4 (Einzeldatei lean-Ausführung), Mathlib-abhängige Beweise sind ein separater Durchlauf (über lake-Projekt)

• (ii) Das Vokabular von IncompleteMarker.dimension ist zunächst auf 4 Arten beschränkt, Erweiterungen erfolgen aus operativer Erfahrung

• (iii) Die Hash-Kette dient der Manipulationserkennung, kryptografische Signierung (z. B. Sigstore) ist ein separates Anliegen

• (iv) Das eingeschränkte Eval ist schwächer als AST-Level-Analyse (z. B. asteval), für hohe Zuverlässigkeitsanforderungen sind in einem separaten Durchlauf Abhängigkeiten hinzuzufügen

• (v) Die Neuheitsbehauptung der „Widerlegungsmaschine" ist null ([[feedback-world-uniqueness-claim-controllable]]) = nur eine integrierte Disziplinschicht aus Property-basiertem Testen (Hypothesis) + Lean 4 sorry-Check + Coq / Isabelle-Industriestandard, die Neuheit liegt allein in der Kombinationsdisziplin von „4-Wert-Urteil + Marker-Invariante + Hash-Kette + MCP-Wrapper"

• (vi) Die Integrationsdemo (Collatz t1=1) ist keine Reproduktion der tatsächlichen Lyapunov-Analyse von Herrn Fujimoto – sie demonstriert nur die WERKZEUGFUNKTION mit vereinfachtem V = log2(n) und endlicher Stichprobe, die echte Reproduktion erfolgt in einem separaten Durchlauf über das tatsächliche V von Herrn Fujimoto + Bedingungen + Lean 4-Formalisierung

• (vii) Die „sorry-frei"-Bestimmung von refute_lean hängt von #print axioms ab = wenn der Kernel von Lean selbst einen Bug hat, wird nicht verifiziert (Kernel-Bug liegt außerhalb des Rei-Umfangs)