rei-verify

Машина опровержения (refutation machine) — инфраструктура верификации + MCP-сервер, специализирующаяся на отрицании, а не на генерации.

Версия: 0.1.0a1 (2026-08-19) — 4 примитива + 4 инструмента опровержения + 8 MCP-инструментов + демонстрация интеграции. Тесты 198/0 PASS.

Почему «машина опровержения»

Генерация насыщается. Опровержение не насыщается.

Современные LLM беглы. Они способны выдавать правдоподобные цепочки доказательств, правдоподобный код, правдоподобные названия теорем независимо от их истинности. Даже если бенчмарки насыщаются до 96%, эта структура не меняется. Миру не хватает не «машины, создающей правдоподобное», а «машины, надежно убивающей правдоподобное».

Основное обещание машины опровержения:

• Получив утверждение, выделяет вычислительные ресурсы на поиск контрпримеров. Попытки доказательства откладываются.

• Если контрпример не найден, явно возвращает «форму пространства поиска, в котором он не найден» (не маскирует молчание под успех).

• К выходным данным обязательно прилагается «место, которое сломается, если утверждение ложно». Нулевое количество sorry в Lean 4 — самый строгий частный случай этого.

• «Не удалось опровергнуть» и «верно» обрабатываются как разные сущности на уровне типов.

Related MCP server: prova-mcp

4-значный вердикт (основная дисциплина «никогда не лгать»)

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 でない

Не сводится к бинарному TRUE/FALSE = не опровергнуто ≠ верно. Типизация дисциплины, выдерживаемой IUT в течение 12 лет.

Типовая гарантия «не маскировать молчание под успех»: для всех вердиктов, кроме CONFIRMED, обязательно наличие 1 или более IncompleteMarker (измерение + что_было_испытано + что_не_было_испытано + причина) (инвариант dataclass, нерушимо).

4 примитива (rei_verify)

4 инструмента опровержения (rei_verify.*)

Сердце машины опровержения. Все инструменты возвращают единообразную структуру VerdictWithMarkers (4-значный вердикт + маркеры + audit_hashes).

★ Инструмент выдает CONFIRMED только для refute_lean_source (только в случае, когда ядро Lean 4 подтверждает отсутствие sorry). Остальные 3 инструмента всегда возвращают REFUTED или HOLDING = типовая гарантия дисциплины «отсутствие контрпримера не является доказательством».

8 MCP-инструментов

Могут быть вызваны напрямую из LLM-клиентов, таких как Claude Desktop / Cursor / Cline:

MCP-безопасные выражения используют ограниченный eval = предварительное отклонение __import__ / exec / eval / open / префикса __, разрешен только белый список _SAFE_BUILTINS (abs/min/max/sum/len/int/float/str/bool/round/any/all/range).

Установка

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

или из исходного кода:

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

Требуется Python 3.10+ (новые возможности dataclass + Enum + typing). Основные примитивы работают только со стандартной библиотекой (импорт возможен даже при отсутствии пакета mcp).

Использование — библиотека

VerifiedExecution (пользовательский)

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)

Разрешенные аксиомы по умолчанию = основа Mathlib [propext, Classical.choice, Quot.sound]. sorry / native_decide / запрещенные аксиомы направляются в HOLDING.

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)

• Исчерпание → HOLDING (маркер search_space, «отсутствие ≠ доказательство»)

• Ограничение по времени/количеству образцов → HOLDING (маркер compute_budget)

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 実行 (集計目的)
)

• Любая точка останова False → REFUTED (метка + контекст в качестве свидетеля)

• Все пройдены → HOLDING («исчерпание перечисленных контрольных точек ≠ покрытие всех случаев»)

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)

Использование — MCP (Claude Desktop)

claude_desktop_config.json:

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

или (установленный скрипт):

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

Примеры MCP-выражений (привязка x для поиска, привязка ctx для точек останова):

{
  "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}}
    ]
  }
}

Демонстрация интеграции

examples/collatz_t1_ones_lyapunov_demo.py — выполнение сканирования α-спуска Ляпунова для нечетных чисел Коллатца n с trailing_ones(n)=1 с помощью assert_breakpoints.

python examples/collatz_t1_ones_lyapunov_demo.py

Пример вывода (1 048 575 образцов / 76,7 мс):

α=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

Свидетель n увеличивается по мере ужесточения α (n=9 → n=14 601) = прямое наблюдение конечного отражения r(n) → 1 при n → ∞, инструмент соблюдает дисциплину «не автоматически повышать конечное отсутствие до CONFIRMED». Подробное честное описание области применения см. в комментариях внутри демонстрации.

Покрытие тестами

Всего 198/0 PASS (6 файлов тестов):

# 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

Для сопровождающих: настройка Trusted Publisher PyPI

Файл .github/workflows/publish.yml в этом репозитории выполняет публикацию в PyPI при пуше тега v* + пробный запуск TestPyPI при workflow_dispatch. Перед использованием необходима регистрация Trusted Publisher на обеих сторонах (PyPI / TestPyPI) и создание окружения GitHub.

Подробные инструкции см. в TRUSTED_PUBLISHER_SETUP.md.

⚠️ Перед пушем тега обязательно дважды проверьте workflow.yml и регистрацию Trusted Publisher (предотвращение случайного срабатывания «тег = триггер релиза»).

Дизайн

См. DESIGN.md для полного обоснования (8 разделов):

• Отправная точка дизайна (4 принципа стека Rei)

• Подробности 4 примитивов

• Таблица правил вердиктов (единый источник истины)

• Сопоставление 3+1 инструментов машины опровержения

• Связь с детектором дрейфа фрейма

• Нецели (выходящие за рамки скелета)

• Зависимости (намерение нулевых внешних зависимостей)

• Честная область применения

Связанные проекты

• fc0web/rei-automator-mcp — MCP для автоматизации Windows PC, происхождение AuditChain (обобщенное извлечение из STEP 1340 AuditLogWriter)

• fc0web/grounded — Проверка прозаического grounding (2-уровневая верификация)

• fc0web/grounding-check — Проверка grounding SCPI-аппаратуры

Автор

Нобуки Фудзимото (Nobuki Fujimoto)

Лицензия

MIT (безотзывно для v0.x). Возможна двойная лицензия AGPL-3.0 + коммерческая для v1.0+. См. LICENSE.

Честная область применения (непреложные границы)

• (i) Инструменты опровержения скелета работают только напрямую с Lean 4 (выполнение одного файла lean), доказательства, зависящие от Mathlib, требуют отдельной итерации (через проект lake)

• (ii) Словарь IncompleteMarker.dimension изначально содержит только 4 типа, расширение будет основано на операционном опыте

• (iii) Хеш-цепочка предназначена для обнаружения подделки, криптографическое подписание (Sigstore и т.д.) — отдельная задача

• (iv) Ограниченный eval слабее, чем AST-анализ (asteval и т.д.), для требований высокой надежности потребуется добавление зависимостей в отдельной итерации

• (v) Нулевое утверждение новизны «машины опровержения» ([[feedback-world-uniqueness-claim-controllable]]) = только дисциплинарный слой интеграции property-based testing (Hypothesis) + проверки sorry в Lean 4 + отраслевых стандартов Coq / Isabelle, новизна заключается только в комбинаторной дисциплине «4-значный вердикт + инвариант маркера + хеш-цепочка + MCP-обертка»

• (vi) Демонстрация интеграции (Collatz t1=1) не является воспроизведением реального анализа Ляпунова г-на Фудзимото — это упрощенная V = log2(n) и демонстрация работы ИНСТРУМЕНТА на конечной выборке, истинное воспроизведение потребует реальной V г-на Фудзимото + условий + формализации в Lean 4 в отдельной итерации

• (vii) Определение "без sorry" в refute_lean зависит от #print axioms = если в самом ядре Lean есть ошибка, верификация не будет выполнена (ошибки ядра выходят за рамки Rei)