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에서 별개의 것으로 취급한다.

Related MCP server: leanscreen

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의 타입화.

「침묵을 성공으로 위장하지 않음」 타입적 보장: CONFIRMED 이외의 모든 verdict에 IncompleteMarker (dimension + what_was_tried + what_was_not_tried + reason)가 1개 이상 필수 (dataclass invariant, 깨지지 않음).

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

또는 소스에서:

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

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

또는 (설치된 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 밖)