rei-verify

反証機械 (refutation machine) — 生成ではなく否定を専門にする 検証 infrastructure + MCP server。

Version: 0.1.0a1 (2026-08-19) — 4 primitives + 4 refutation tools + 8 MCP tools + integration demo。 test 198/0 PASS。

なぜ 「反証機械」 か

生成は 飽和する。 refutation は 飽和しない。

現行 LLM は 流暢だ。 もっともらしい 証明の 筋道、 もっともらしい code、 もっともらしい 定理の 名前を、 事実かどうかと 独立に 出力できる。 benchmark が 96% まで 飽和しても、 この構造は 変わらない。 世界に 足りないのは 「もっともらしいものを 作る 機械」 ではなく、 「もっともらしいものを 確実に殺す 機械」 の 方だ。

反証機械の core promise:

• 主張を受け取ったら、 反例探索に 計算資源を 割く。 証明の試みは 後回し。
• 反例が 見つからなかった場合、 「見つからなかった 探索空間の 形」 を 明示的に return (沈黙を 成功と 偽装しない)。
• 出力に 必ず 「その主張が 偽なら 壊れる 場所」 が 添付される。 Lean 4 の sorry ゼロは これの 最も厳格な 特殊ケース。
• 「反証できなかった」 と 「正しい」 を、 型 level で 別物 として 扱う。

4-value verdict (「絶対に嘘をつかない」 core discipline)

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

Binary TRUE/FALSE に しない = 反証されなかった ≠ 正しい。 IUT 12 年 holding discipline の 型化。

「沈黙を 成功と 偽装しない」 型的保証 (正確な範囲):

• REFUTED / HOLDING / INCOMPLETE_FRAME の 3 verdict は IncompleteMarker 1 個以上 必須 = VerdictWithMarkers dataclass invariant で ValueError raise (0.1.0a1 実測で 3 verdict 全 型拒否 verify 済)
• CONFIRMED は marker 不要 = 型 level では marker 空 CONFIRMED 構築を 拒否しない
• CONFIRMED の 信頼性は ツール層の 規律で 保証: search_counterexample / assert_breakpoints / hold_verdict は 構造上 常に marker を 出すため CONFIRMED に 到達不能、 refute_lean_source のみが Lean 4 kernel の sorry-free 認定を 経由して CONFIRMED を 返す設計
• caller が VerdictWithMarkers(verdict=CONFIRMED, markers=[], ...) を 直接構築することは 型的には 可能 (0.1.0a2 findings ① 明示訂正、 従前 「型 level で 保証」 は 過大主張)

4 primitives (rei_verify)

4 refutation tools (rei_verify.*)

反証機械の 心臓部。 全 tool が VerdictWithMarkers (4 値 verdict + markers + audit_hashes) を return する 一貫 shape。

★ CONFIRMED を tool が 出すのは refute_lean_source のみ (Lean 4 kernel が sorry-free 認定した case のみ)。 他 3 tool は 常に REFUTED か HOLDING = 「absence of counter-example is not proof」 discipline の 型 level 保証。

8 MCP tools

Claude Desktop / Cursor / Cline 等の LLM client から 直接呼べる:

MCP-safe expression は restricted eval = __import__ / exec / eval / open / __ prefix 事前 reject、 _SAFE_BUILTINS whitelist (abs/min/max/sum/len/int/float/str/bool/round/any/all/range) のみ 許可。

Installation

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

or from source:

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

Requires Python 3.10+ (dataclass + Enum + typing 新機能)。 core primitives は 標準 library のみ で 動作 (mcp package 不在 でも import OK)。

Usage — library

VerifiedExecution (custom)

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)

Default allow_axioms = Mathlib base [propext, Classical.choice, Quot.sound]。 sorry / native_decide / disallowed axiom は HOLDING に routing。

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)

• exhaustion → HOLDING (search_space marker、 「absence ≠ proof」)
• time/sample budget → 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 実行 (集計目的)
)

• 任意 breakpoint False → REFUTED (label + context を witness)
• 全 pass → HOLDING (「listed checkpoints exhausted ≠ 全 case cover」)

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)

Usage — MCP (Claude Desktop)

claude_desktop_config.json:

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

or (installed script):

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

MCP expression 例 (x bind for search, ctx bind for breakpoints):

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

Integration demo

examples/collatz_t1_ones_lyapunov_demo.py — Collatz 奇数 n with trailing_ones(n)=1 の Lyapunov α-descent scan を assert_breakpoints で 実行。

python examples/collatz_t1_ones_lyapunov_demo.py

Sample output (1,048,575 samples / 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

Witness n が α tight 化と共に 増大 (n=9 → n=14,601) = r(n) → 1 as n → ∞ の 有限反映を 直接観測、 tool が 「finite absence を CONFIRMED に 自動昇格しない」 discipline を 遵守した実例。 詳細な honest scope は demo 内 コメント参照。

Test coverage

累計 198/0 PASS (6 test files):

# 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

For maintainers: PyPI Trusted Publisher setup

本 repo の .github/workflows/publish.yml は v tag push で PyPI 本番 publish* + workflow_dispatch で TestPyPI dry-run。 使用前に PyPI / TestPyPI 両側の Trusted Publisher 登録 + GitHub Environment 作成が 必要。

詳細手順は TRUSTED_PUBLISHER_SETUP.md 参照。

⚠️ tag push 前 に workflow.yml + Trusted Publisher 登録 の double-check を (「tag = release trigger」 事故防止)。

Design

See DESIGN.md for full rationale (8 節):

• 設計の 起点 (Rei stack 4 原則)
• 4 primitives 詳細
• Verdict rule table (単一 source of truth)
• 反証機械 3+1 tool mapping
• framing-drift-detector との 関係
• 非目標 (out of scope for skeleton)
• 依存 (external dep ゼロ の 意図)
• honest scope

Related

• fc0web/rei-automator-mcp — Windows PC 自動化 MCP、 AuditChain の 由来 (STEP 1340 AuditLogWriter の 汎用抽出)
• fc0web/grounded — 散文 grounding checker (2-tier verification)
• fc0web/grounding-check — SCPI hardware grounding checker

Author

藤本 伸樹 (Nobuki Fujimoto)

License

MIT (v0.x irrevocable)。 v1.0+ で AGPL-3.0 + commercial dual 可能性。 LICENSE 参照。

Honest scope (譲れない線)

• (i) skeleton の refutation tools は Lean 4 との 直接連携 (single-file lean 実行) のみ、 Mathlib 依存 proof は 別 iter (lake project 経由)
• (ii) IncompleteMarker.dimension 語彙は 初期 4 種のみ、 拡張は operational 経験から
• (iii) hash chain は tamper detection 用、 cryptographic signing (Sigstore 等) は 別 concern
• (iv) restricted eval は AST-level analysis (asteval 等) より 弱い、 高信頼要件 は 別 iter で 依存追加
• (v) 「反証機械」 の 新規性主張 ゼロ ([[feedback-world-uniqueness-claim-controllable]]) = property-based testing (Hypothesis) + Lean 4 sorry-check + Coq / Isabelle 系 industry 標準 の 統合 discipline layer のみ、 novelty は 「4 値 verdict + marker invariant + hash chain の 型的統合 + MCP wrapper」 の 組合せ discipline のみ
• (vi) integration demo (Collatz t1=1) は 藤本さん 実 リヤプノフ解析 の 再現 では ない — 簡略化 V = log2(n) と 有限 sample での TOOL 動作 の 実証 のみ、 真 reproduction は 藤本さん 実 V + 条件 + Lean 4 formalization 経由 で 別 iter
• (vii) refute_lean の "sorry-free" 判定は #print axioms 依存 = Lean 自体の kernel bug が あれば verify されず (kernel bug は Rei scope 外)