Rei-AIOS に AI より正確かつ厳密な道具を接続するための統合層。 SAT / SMT / 定理証明 / 数式処理 / 数値計算のエンジンを Rei から呼び出せる形にラップします。 Rei の役目は「どの道具に何を投げるかの判断と、 入力の組み立て、 結果の解釈」で、 数値計算そのものではありません。
python -m rei_solver.harness。 v0.2 で Windows 対応 (taskkill /F /T + subprocess.CREATE_NEW_PROCESS_GROUP で POSIX SIGKILL 系と対称化、 lifecycle test は Windows で 5 件 timing-flaky なため明示 skip、 POSIX では従来通り全 pass)。
「AI が何百年掛かっても辿り着けない解析器を作ることは理論的に可能か」 の問いから、 Transformer の 1 回順伝播 = TC⁰ 程度 (Merrill & Sabharwal 2023 系)、 逐次深計算は構造的苦手、 思考連鎖は「疑似 CPU」 で専用ソルバに絶望的に非効率、 という帰結。 「AI が自分の限界を自覚する = calibration」 が最難、 assurance field で機械可読化する提案 → 本実装。
| # | 原則 | 内容 |
|---|---|---|
| 1 | 実装しない、包む | SAT / SMT / 定理証明 / 数値計算の中核を自前で書かない。 数十年の検証実績があるエンジンを呼ぶ。 |
| 2 | 全てのツールは非同期ジョブ | Z3 は数 ms、 DFT/CFD は数時間〜数日。 軽い方に合わせた同期 API は重い方を足した瞬間書き直しになる。 submit → poll に統一。 |
| 3 | 実行前に同期検証 | ソルバは入力を疑わない。 LLM が入力を組み立てる以上、 solver_validate が唯一の防御線。 |
| 4 | 保証の種類を必ず返す | 全結果に assurance フィールド。 「AI 自覚」 問題の operational form。 |
| 値 | 意味 | 例 |
|---|---|---|
| proof | 機械証明。 反証が存在しないことが確定 | SMT unsat、 SAT unsat、 恒等式の成立 |
| witness | 具体的証拠つき。 第三者が独立に検算可能 | SAT のモデル、 反例入力ベクタ |
| numeric | 数値近似。 離散化誤差・収束条件に依存 | FEM、 DFT、 MD (将来) |
| heuristic | 探索打ち切り等。 保証なし | unknown、 timeout |
proof と heuristic を呼び出し側が取り違えると、 この統合層の意味が消える。 TS 側には isProved(job) ガードを用意。
Microsoft Research、 MIT ライセンス、 数十年の検証実績。 4 op: check_sat / prove / circuit_equivalence / optimize。 proof または witness。 回路化パイプラインとの直接接続 layer。 golden 7 件。
純 Python、 BSD ライセンス。 6 op: simplify / solve / integrate / differentiate / limit / verify_identity。 SymPy インジェクション 5 forbidden token (__import__, exec, eval, open, compile, globals...) を検証段階で拒否。 golden 8 件。
CaDiCaL / Kissat / Glucose / MiniSat 内蔵。 MIT ライセンス。 4 op: solve_cnf / solve_dimacs / enumerate_models / maxsat。 バックエンド自動選択 (cadical195 → cadical153 → glucose42 → glucose4 → minisat22)。 golden 6 件。
Apache 2.0 / Microsoft Research + Leonardo de Moura。 3 op: check_proof / verify_axiom_free / verify_with_mathlib (v0.2 追加、 v0.4 R1 拡張)。 assurance 4 段階を Lean/Mathlib 慣習で完全分類: axiom-free または標準基盤 axiom (propext / Classical.choice / Quot.sound / funext) のみ → proof / ユーザ axiom or Lean.ofReduceBool (native_decide) → witness / sorryAx → heuristic。 ★ v0.4 R1: import prefix whitelist を従来の Mathlib / Std / Aesop / Batteries に加え project-scoped namespace (CollatzRei.* 等、 project_root 内の任意 top-level module 名) にも拡張 = Rei 内部 file を Rei-Solver から直接 verify 可能に。 golden 7 件 (standalone 5 + mathlib 2)、 Rei env で 7/7 PASS 実測。 Rei 141+ axiom-free theorem stack (Cantor v0.9-b / Chang 20/29 / Collatz 48 / ExitLayer / Fermat Paper 176 / Paper 26 v3.0 numSurvivors_eq_0 / 層4 Constructor Theory 4/5) と verify_with_mathlib op から直接統合可能。
Pure Python (追加依存なし)。 3 op: compute_limit (Gold 1965 + Putnam 1965 trial-and-error predicate) / decide_halting (bounded TM halting 近似) / advice_query (Karp-Lipton 1980 P/poly non-uniform advice)。 heuristic (compute_limit / decide_halting) または witness (advice_query default)。 golden 6 件全て sub-ms 通過。 層3 の 3 経路 (B/C/D) のうち B (一様性) + C (停止判定) を operational demonstrate (経路 A は v0.4 R2 QRNG で追加、 D は Bekenstein 限界で out-of-scope)。
Pure Python (追加依存なし、 urllib のみ)。 1 op: sample_certified_random — NIST Randomness Beacon v2 most recent pulse (60 秒に 1 回更新、 512-bit outputValue + RSA signature + pulseIndex + timeStamp)。 witness (RSA signature verifiable、 pulseIndex 経由 NIST archive 独立照会可)。 golden 1 件 (Rei env live で pulseIndex 1888414 実 fetch verify)。 ★ 万能 TM の外 経路 A = 「TM で generate 不可能な randomness」 に物理装置なしで触れる。 authenticated randomness beacon (NIST 政府認証) 経由 = 「certified physical entropy」 tier。 network required = offline 環境では skip 推奨。
witness または heuristic 止まり (proof 昇格は原理不可 = Post 1944 Δ₂ 分類の物理的帰結)。
proof に昇格することは原理的にない。 詳細は SPEC.md §4 参照。
tools/list that returns)| Tool | 同期性 | 用途 |
|---|---|---|
| solver_capabilities | 同期 | エンジン・操作・保証レベル・想定実行時間の一覧 |
| solver_validate | 同期 | 実行せず入力だけ検査 |
| solver_submit | 非同期 | ジョブ投入。 即座に job_id を返す |
| solver_poll | 同期 | 状態と結果を取得。 wait_s で待てる |
| solver_run | 準同期 | submit+poll の糖衣。 数秒で終わる問題のみ |
| solver_cancel | 同期 | プロセスグループごと停止 |
| solver_jobs | 同期 | ジョブ一覧 |
| solver_verify | 同期 | 既知解ハーネス実行 |
| 項目 | 結果 |
|---|---|
| 既知解ハーネス (z3: 7 + sympy: 8 + pysat: 6 + lean4: 7 (v0.2 mathlib + v0.4 R1 namespace 拡張) + limit: 6 (v0.3) + qrng: 1 (v0.4 R2 new)) | 35/35 通過 (2026-08-04 v0.4 時点、 Rei env 実測、 QRNG は NIST Beacon live pulseIndex 1888414 fetch verify 済) |
統合テスト (tests/test_rei_solver.py) | 24/24 通過 (Windows は lifecycle 系 5 件を timing-flaky で明示 skip、 POSIX は 24/24 pass 継続) |
| ハードタイムアウト (PHP(11,10)、 3 秒指定) | 3.28 秒で停止 |
| キャンセル後の孤児プロセス | 0 |
| タイムアウト後の孤児プロセス | 0 |
| 12 ジョブ連続実行後のゾンビ | 0 |
| 大容量結果 (5000 モデル) のデッドロック | なし |
| SymPy インジェクション (4 種) | 全て検証段階で拒否 |
TypeScript ブリッジ (tsc --strict) | 通過 + 実行して Python 側と疎通確認 |
| MCP ハンドシェイク + tools/list + tools/call | 正常 |
最初は worker 内の threading.Timer で 見ていたが、 PySAT や Z3 は C 拡張の中で GIL を握ったまま回るため、 Python のタイマースレッドが一切スケジュールされない。 3 秒指定が 18 秒かかっていた (DB リーパー頼み)。 supervisor / child の 2 プロセス構成に変更 → 3.28 秒で停止確認。 supervisor は Queue.get(timeout=…) で待つだけなので GIL に縛られず、 確実に SIGTERM → SIGKILL を送れる。 CFD や DFT を足したとき、 ここが「暴走ジョブを確実に止められる」 保証になる。
supervisor だけ殺すと fork された子が CPU を回し続ける (実測確認)。 spawn_worker が start_new_session=True で独立プロセスグループを作り、 os.killpg でグループごと落とす方式に変更。 ゾンビ蓄積も同時修正。 軽いソルバだけ試していたら気付かず、 重いエンジンを足した後に発覚していた類のもの。
| Rei-solver 機能 | Rei stack 内接続 |
|---|---|
| z3.circuit_equivalence | kairo processor 11-format container spike 議論との直接接続。 「解析結果 → SMT で機械反証」 line。 非等価なら反例入力ベクタが返るので、 Rei の解析結果自体を機械的に反証できる = 「AI が自分より正確な道具を呼ぶ」 の理想形 |
| assurance = "proof" | Rei stack の Lean 4 axiom-free 100+ theorem (Cantor / Chang / Collatz / ExitLayer / Fermat / Paper 26 v3.0 numSurvivors_eq_0) と同 category。 「証明されて正しい」 vs 「99.999% 正しい」 の種類差の operational form |
| assurance = "numeric" | B-16R Coupled-Position Analyser (Boltzmann learning h/J 復元) 系の数値近似と同 category。 将来 OpenMM / PySCF / FEniCSx / OpenFOAM 追加時に増える |
| Rei calibration discipline | [[feedback-projection-self-audit-pattern]] + [[feedback-critique-response-pattern]] + [[feedback-super-naming-siren-family-pattern]] + [[feedback-world-uniqueness-claim-controllable]] 等の Rei 側 self-audit stack と同 vector。 rei-solver assurance field はこれの機械可読 layer |
| Lean 4 engine (standalone + mathlib) | 2026-08-01 実装 → 2026-08-02 v0.2 で mathlib 対応完了 (Rei env 7/7 golden PASS)。 verify_with_mathlib op (payload に project_root、 default data/lean4-mathlib) で Rei の Chang 20/29 + Cantor v0.9-b + Collatz 48 + Fermat F_9 Pratt-style + ExitLayer + 層4 ConstructorTheoryBasic (2026-08-02 追加) 系と直接統合可能。 |
| limit engine (層3 経路 B/C) | 2026-08-02 v0.3 実装済。 層4 ConstructorTheoryBasic.lean (Deutsch-Marletto Constructor Theory の 14 theorem 中 13 zero-axiom + 1 [Classical.choice] のみ) と対を成す設計: 層3 (Python level) = 万能 TM の外を operational demonstrate、 層4 (Lean 4 level) = 物理的可能性の formal framework を axiom-free 型化。 藤本さん 2026-08-02 「層」 議論から派生した単一 arc の 2 layer。 |
| qrng.sample_certified_random | 2026-08-04 v0.4 R2 実装済。 NIST Beacon v2 経由で 万能 TM の外 経路 A (計算不能系列生成) を物理装置なしで cover = 層3 の 3/3 全経路 operational 完成 (A/B/C、 D は Bekenstein 限界で out-of-scope)。 層4 Constructor Theory 4/5 (Superinformation / Time / Thermodynamics / Interoperability、 08-04 marathon で追加、 計 28 theorem axiom-free) と対応する物理装置経路。 assurance = witness (RSA signature verifiable、 pulseIndex 独立照会可)、 「certified physical entropy」 tier に留める (量子性そのものは claim できない)。 |
| # | エンジン | 状態 | 実装量 | 実行時間 | 主な障壁 |
|---|---|---|---|---|---|
| ✅ | Lean 4 (standalone) | 2026-08-01 実装済 | 中 | s | Rei env で 5/5 golden PASS ~1s/case |
| ✅ | Lean 4 + mathlib | 2026-08-02 実装済 (v0.2) | 中 | s〜min | verify_with_mathlib op、 Rei env で 2/2 mathlib golden + 全 7/7 lean4 PASS |
| ✅ | limit (Gold-Putnam + Karp-Lipton) | 2026-08-02 実装済 (v0.3) | 小 | ms | 極限計算 / 停止判定近似 / non-uniform advice、 3 op × 6 golden PASS、 万能 TM の外 経路 B/C を cover |
| ✅ | QRNG (NIST Beacon v2) | 2026-08-04 実装済 (v0.4 R2) | 小 | s (network) | certified physical entropy、 1 op × 1 golden PASS (pulseIndex 1888414 live verify)、 万能 TM の外 経路 A を cover = 3/3 全経路 operational 完成 |
| 1 | OpenMM (分子動力学) | 未着手 | 中 | min〜hour | 力場の選択、 GPU |
| 2 | PySCF (DFT) | 未着手 | 中 | min〜hour | 基底関数・汎関数・収束判定 |
| 3 | FEniCSx / CalculiX (FEM) | 未着手 | 大 | min〜hour | メッシュ生成と境界条件 |
| 4 | OpenFOAM (CFD) | 未着手 | 大 | hour〜day | メッシュ、 乱流モデル、 並列実行 |
OpenMM 以降は assurance="numeric" を返すこと。 proof を返してはならない。
taskkill /F /T /PID + subprocess.CREATE_NEW_PROCESS_GROUP を導入して POSIX SIGKILL 系と対称化したが、 multiprocessing spawn cold start (5-8s) + taskkill cleanup timing の合成 flakiness のため 5 件を明示 skip。 POSIX (Linux / macOS) では 24/24 pass 継続。beacon.nist.gov) への HTTPS fetch 必須 = offline 環境では skip 推奨。 authenticated randomness (RSA signature) だが「量子性そのもの」 は claim できない (NIST 実装詳細非公開) = 「certified physical entropy」 tier に留めるprogress 列の追加待ちverify_identity の非恒等判定は証明ではない (§4 参照)proof に昇格することはないcd experiments/rei-solver pip install -r requirements.txt python -m rei_solver.harness # 全 6 engine (35 golden case、 ~25s + qrng network) python -m rei_solver.harness qrng # QRNG engine のみ (1 case、 NIST Beacon fetch ~1-3s) python -m rei_solver.harness limit # limit engine のみ (6 case、 sub-ms) python -m rei_solver.harness lean4 # Lean 4 のみ (7 case、 mathlib 込 ~30s) python -m pytest tests/ # 統合テスト 24 件 (Windows は 5 件 skip)
experiments/dfumt8-kairo-processor/) — 11-format container spike と z3.circuit_equivalence 接続 linedata/lean4-mathlib/CollatzRei/ConstructorTheoryBasic.lean — 層4 Constructor Theory Basic (2026-08-02 追加)、 Deutsch 2013 + Marletto 諸論文 + Deutsch-Marletto 2025 (arXiv:2505.08692v3) の task algebra + possibility statement の Lean 4 axiom-free skeleton、 14 theorem 中 13 zero-axiom + 1 [Classical.choice] のみ (Zcsg / Lawvere / Sugeno 系譜と同格)data/lean4-mathlib/CollatzRei/Layer4/ — 層4 Constructor Theory 4/5 (2026-08-04 08-04 marathon で追加): (a) Superinformation (Deutsch-Marletto 2015) + (b) Time (Deutsch-Marletto 2025 arXiv:2505.08692v3) + (c) Thermodynamics (Marletto 2016) + (e) Interoperability (Deutsch 2013 §V) の Lean 4 axiom-free skeleton、 計 28 theorem 追加。 (d) Life は siren-family risk で LOW defer。 Rei-Solver 側 QRNG (経路 A) と対応する 層3-4 dual layerexperiments/rei-solver/ (v0.4 時点 6 engine / 21 op / 35 golden、 SPEC.md + README.md + 6 engine + async job model + TS bridge + 24 integration test)