draft v0 — 各判定は要再audit。STEP 未採番。素材のみ。shared tree 不触。
作成: 2026-09-18 / 対象: [[proof-pipeline-device-map]] PIN 7（統合＝端子）候補
0. 位置づけ
「オートマトンを超える」は3つに割れる。本 audit は C のみを対象にする。
| 分岐 | 内容 | 扱い |
|---|---|---|
| A. 表現力で超える | regular の外（register/nominal automata, VASS, WSTS, timed, weighted, alternating/tree, automatic structures） | 対象外。60年分の prior art、Spot/MONA/nuXmv の compose との差分を出すのが困難 |
| B. 計算可能性で超える | オラクル、無限時間TM、BSS、量子 | KILL。物理実装が無いか Church–Turing の外に出ていない |
| C. 判定の様式で超える | 値域・誤り率・全域性・較正の型を変える | 本 audit の対象 |
1-bis ★ 分岐 B の根拠を訂正（2026-09-18 追記、適用04 より）
判定 KILL は維持する。根拠を1点訂正する。
多くの人が使う「ハイパーマシンも自分自身の停止問題に直面するから自己反駁的だ」という対角線論法による反駁は無効である。 Ord & Kieu（arXiv:math/0307020）が示したとおり、対角線論法は相対化する障害であって絶対的な不可能性証明ではない。無限時間TM はチューリング停止性を決定しつつ自分自身の停止問題を持つ。Turing 次数の階層は無矛盾で豊かな構造である。
正しい根拠は二つ：
- Davis の deflationary dilemma（"The Myth of Hypercomputation", Springer 2004）— 提案は「非計算可能な入力を許せば非計算可能な出力が得られる」という自明な観察以上のものでないか、そうでなければハイパーコンピュテーションでない。**Davis は論理的不可能性を主張していない。**主張は「分野としての中身がない」であり、この区別は保つこと
- Piccinini の usability constraint（BJPS 62(4), 2011）— 有限の観測者が有限時間・有限資源で入力を指定し出力を読み出せることを要求すると、Modest PCT は経験的で反証可能な主張になり、現状生き残っている
詳細は [[turing-machine-totality-audit]]（適用04）§4.1。
1-ter ★ 分岐 A にコアルゲブラが無かった（2026-09-18 追記、適用05 より — 取りこぼし）
分岐 A（表現力で超える）に register/nominal automata・VASS・WSTS 等を挙げたが、コアルゲブラを名指ししていなかった。 コアルゲブラはオートマトンの標準的な圏論的抽象であり、分岐 A の最上位に来るべきだった。
判定は変わらない（対象外）。理由を更新する：
- 旧：「60年分の prior art、既存 tool の compose との差分を出すのが困難」
- 新：「コアルゲブラがオートマトンを含む形で既に一般化を完了しており、その外に出る提案は存在しない。」対抗馬に見える応用圏論系（Fong の decorated cospans、Baez らの cospan double categories、Cruttwell らの勾配学習）は coalgebra を引用すらしていない
正確な関係：F = 2 × (−)^A に対し Set^F は「初期状態を持たない決定性オートマトン」の圏と圏同型。初期状態は代数側（1 + A×X → X）、有限性は不可視、ω受理条件は函手の外。詳細は [[algebra-coalgebra-audit]]（適用05）§2.1。
そして本 arc にとって最も重い帰結：四欄のうち V（値域）は Lawvere 1973 の V-豊穣により完全に吸収済みであり、e と c は圏論が扱わない領域にある（適用05 §0・§6）。前4件がすべて c の話だったのは偶然ではない。
1. 判定器の4フィールド
判定器 D を次の4項で書く。
| field | 定義 |
|---|---|
| V（値域） | 装置が返しうる verdict の集合 |
| e（誤り率） | 非ゼロの誤りを許すか、許すならその量が得られるか |
| t（全域性） | どの入力にも答えるか、棄権できるか |
| c（較正） | THEOREM = 健全性定理で構造的に保証／MEASURED = 既知 ground truth に対して実測 |
c の二分が本 audit の主軸。 形式検証の側は THEOREM 一色、統計の側も conformal 系は THEOREM。MEASURED は別分野（天文の injection–recovery、SE の error seeding、生態学の occupancy model、IR の stopping criteria）に集中していて、検証の verdict には接続されていない。
2. 対照表
2.1 形式検証側
| 装置 | V | e | t | c |
|---|---|---|---|---|
| 有限オートマトン / Büchi | {acc, rej} | 0 | 全域 | 不要（定義が ground truth） |
| 3値モデル検査（Bruns–Godefroid 1999） | {tt, ff, ⊥} | なし | 棄権あり（⊥） | THEOREM |
| 3値抽象化精密化（Shoham–Grumberg 2003–06） | {tt, ff, ⊥} | なし | 棄権あり | THEOREM |
| 多値モデル検査 χChek（Chechik et al. 2003） | 任意の de Morgan 束（Kleene 3値・Belnap 4値・積束・鎖束） | なし | 棄権あり | THEOREM（実験は runtime のみ、精度でない） |
| 抽象解釈（Cousot 1977） | {safe, 証明できず} | 片側（false alarm） | 事実上の棄権 | THEOREM |
| Incorrectness logic（O'Hearn 2020） | {real bug, 沈黙} | 片側（逆向き） | 事実上の棄権 | THEOREM |
SMT-LIB の check-sat |
{sat, unsat, unknown} | 量化なし | 棄権あり（実装上の標準） | なし（:reason-unknown は文字列カテゴリ） |
| SV-COMP scoring | {TRUE, FALSE, UNKNOWN} | incorrect-true/false を計数 | 棄権あり | definite verdict のみ MEASURED。UNKNOWN は 0 点＝定義上誤らない |
| SLAM/SDV（EuroSys 2006） | {pass, error, abstraction-fail, tool-fail, timeout} | 正判定の FP 率を実測 | 棄権あり | 正判定のみ MEASURED、don't-know には誤り率なし |
| Mariposa（FMCAD 2023） | 成功率 r ∈ [0,1]（stable / unstable / unsolvable） | a posteriori 実測 | timeout/unknown を failure に算入 | MEASURED（意味保存 mutation を ground truth に、Z検定 α=0.05、Z3 4.12.1 で 2.6% unstable） |
| Abstract Interpretation with Confidence（PACMPL, DOI 10.1145/3808351） | 連続 confidence | 解析的に導出 | あり | THEOREM（仮定したプログラム分布から導出、実測でない） |
2.2 確率的判定・統計側
| 装置 | V | e | t | c |
|---|---|---|---|---|
| Property testing（GGR 1998 / Rubinfeld–Sudan 1996） | {acc, rej} | 定理で境界、多くは片側 | 棄権なし（gap は don't-care として問題文に押し込む） | THEOREM |
| PCP（Arora–Safra 1998 / ALMSS 1998） | {acc, rej} | soundness ≤ 1/2、反復で 2^-k | 棄権なし | THEOREM |
| SMC / SPRT（Younes–Simmons 2002） | {acc, rej} | Type I ≤ α, Type II ≤ β、indifference region | 棄権なし | THEOREM |
| SMC black-box（Sen–Viswanathan–Agha 2004） | verdict + p値 | 検定統計量から | "don't know" を返しうる | THEOREM |
| Bayesian SMC（Zuliani et al. 2010） | Bayes factor / 事後確率 | 事前分布を所与に境界 | 進行中は未決 | THEOREM（事前分布は較正されない） |
| Randomized smoothing（Cohen et al. 2019） | class + certified radius、ABSTAIN | Monte-Carlo 信頼限界 | 明示的 ABSTAIN | THEOREM（棄権率のみ実測報告） |
| Conformal prediction（Vovk–Gammerman–Shafer 2005） | 集合値（空集合／単集合／多集合／全体） | ユーザが ε を指定 | あり | THEOREM（交換可能性の下、有限標本・分布非依存） |
| Mondrian/conditional conformal（Vovk 2012 / Gibbs et al. 2023） | 集合値、宣言された taxonomy 毎 | 区分毎の ε | あり | THEOREM。保証が「事前宣言」に indexed される唯一の統計装置。ただし未宣言でも拒否せず marginal に落ちるだけ |
| Conformal risk control（Angelopoulos et al. 2022） | 閾値族 | 任意の単調損失（FNR 直接制御可） | あり | THEOREM |
| Reject option（Chow 1970） | label ∪ {reject} | error–reject tradeoff 曲線 | 棄権の起点 | 真の事後確率を所与なら THEOREM、実際は推定＝要 MEASURED |
| Selective classification（El-Yaniv–Wiener 2010 / Geifman–El-Yaniv 2017） | predict / abstain + coverage | (r*, δ) をユーザが指定 | あり | THEOREM（held-out 上の数値境界） |
| Learning to defer（Madras et al. 2018） | predict / defer（宛先付き） | 実測 | あり | MEASURED（分布非依存の保証なし） |
| Platt scaling / ECE（Guo et al. 2017） | 確率値 | 保証でなく読み取り | なし | MEASURED（ECE は実測されたミスキャリブレーション） |
2.3 設計中の3装置（Rei 側）
| 装置 | V | e | t | c |
|---|---|---|---|---|
| 停止条件較正装置 | 8値（D-FUMT₈、FLOWING/NEITHER が「まだ分からない」を型として持つ） | 非ゼロ、偽陰性を実測 | 棄権あり | MEASURED を志向（B₄/B₅ 非対称を ground truth に） |
| 修正機器（rei-repair-mcp） | reject + 座標 | reject stream を計数 | — | 修正成功率を測る設計 |
| Ctx チェッカ（STEP 1894） | verdict / refusal-until-declared | — | 未申告なら判定を拒む | — |
3. 差分候補3点の判定
差分候補 (i) 較正が実測 ground truth 由来 → CONFINE
既存：方法論としては5分野で成熟している。
- 系統的レビューの統計的停止基準（Callaghan & Müller-Hansen 2020）— 目標 recall 到達の信頼度を返す。既知の完全集合で検証済み
- TREC Total Recall track（Cormack & Grossman）— 停止規則を既知の完全関連集合に対して較正する評価トラックそのもの
- LAVA（IEEE S&P 2016）— 既知バグを大量注入してバグ発見器の false-negative 率を実測
- error seeding / mutation testing（Mills 1972、DeMillo–Lipton–Sayward 1978）— 既知欠陥の検出率から残存欠陥を推定
- occupancy model（MacKenzie et al. 2002）— 「不在」と「居たが見逃した」を検出確率 p で分離。Q2 の最もきれいな既存定式化
- injection–recovery completeness（天文）— 合成信号の回収率で非検出を定量的上限に変換
未見：形式検証の abstain verdict に実測誤り率が付いた例。3値/多値モデル検査では ⊥ は「誤りえないように定義された論理値」であり、確率的内容を持たない。SV-COMP は UNKNOWN を 0 点にして誤りを定義上消している。Mariposa が唯一の MEASURED だが、測っているのは verdict の正しさでなく安定性。
判定 CONFINE：主張範囲を「形式検証の abstain verdict への適用」に限定する。「既知 ground truth で探索の偽陰性を較正する」という方法論そのものの新規主張は禁止（5分野に先行あり）。
差分候補 (ii) 棄権が副情報の申告義務と結合 → SURVIVE（3点中最も強い）
棄権側の既存：conformal、selective classification、Chow 1970、randomized smoothing、SMT の unknown。トリガは例外なく装置自身の不確実性であり、呼び出し側の未申告ではない。
申告ゲート側の既存：
- SPEC CPU2017 Run Rules §4.6 —「flag description file が付随しない限り結果は invalid とマークされる」（verbatim）。文字通りの refusal-until-declared。 ただし withhold されるのは publication status であって測定値でなく、申告対象は手続きであって「スコアの意味を変える副情報」ではない
- TPC Full Disclosure Report、Registered Reports（事前登録＝結果前の in-principle acceptance）、Kaggle の外部データ開示ルール — いずれも社会的/編集的ゲートで誤り率なし・部分性の概念なし
- Proof-Carrying Code（Necula 1997）— evidence-until-supplied であって declaration-until-supplied ではない。検証器は「何を仮定したか」を問わない
圧縮界は別解で解いている：Mahoney の LTCB は「decompressor と辞書・設定ファイル等を同梱し、そのサイズをスコアに算入」させる。MDL の2部符号も同型。これは gating でなく pricing。最も近い知的祖先だが機構が違う。
唯一の近縁：Mondrian/conditional conformal は保証が事前宣言された taxonomy に indexed される。だが未宣言でも拒否せず、黙って弱い marginal 保証に落ちる。宣言は入力であってゲートではない。
判定 SURVIVE：UNDECIDABLE-UNTIL-DECLARED（reject とも「不確かです」とも異なる第3値で、未申告の decoder/辞書/補助入力によって発火し、その棄権率自体が実測される）という装置は見つからなかった。
併記必須：これは約6通りの query 定式化に基づく bounded search の negative であって不在証明ではない。本装置が扱おうとしている問題（探して見つからない ≠ 存在しない）が、この audit 自身にそのまま適用される。
差分候補 (iii) reject が座標を持ち修正ループに戻る → CONFINE（最も弱い）
正規化の半分は完成済み：SARIF 2.1.0（OASIS 標準 2020）が既に異種ツールを1つの result（ruleId + physicalLocation：artifact URI + start/end line/column、オプションで fixes）に載せている。ただし修正の試行結果を記録する場が無く、SARIF ログ単体からは修正成功率が計算できない。
測定の半分も完成済み：
- Tricorder（ICSE 2015）/ Lessons from Building Static Analysis Tools at Google（CACM 2018）— 複数解析器 → 1つの located finding schema → not-useful 率 10% 超の解析器は除去という deploy gate。形は正しいが、装置の多様性が lint 系に限られる
- Google の build error 研究（ICSE 2014、2660万ビルド）、DeepDelta（FSE 2019、error kind 別の修正精度）、Graph2Diff、Repairnator
- CS教育の Error Quotient / Repeated Error Density / Watwin — 「reject 列に対する修正成功」を真面目に測ってきた唯一のコミュニティ。ただし常に単一コンパイラ
最も近い miss：Vericoding benchmark（2025）は Dafny/Verus/Lean の3つの異なる検証装置で修正ループを回すが、エラーは raw のまま渡され、正規化されず、kind 別の内訳も出していない（言語別の集計のみ：Dafny 82% / Verus 44% / Lean 27%）。ExVerus（2026）は kind 別 triage（InvFailFront/InvFailEnd + JSON 反例）と kind 別成功率を持つが Verus 単体。
判定 CONFINE：「異種検証装置の reject を1座標系に正規化し、kind 別修正成功率を測る」統合体は未見。ただし部品は全て存在するので、これは発明ではなく統合工事。「新機構」と名乗らず「SARIF に outcome を足した統合」という記述に固定する。
4. 縮退条件（「超える」を名乗るための必要条件）
D = (V, e, t, c) として、
オートマトン = (V = {acc, rej}, e = 0, t = 全域, c = 不要)
「超える」と言えるのは、V を2値に縮約し e→0 と置いたとき automaton の判定型に一致することを示した場合に限る。示せないなら語を「別の判定器」に落とす。
Collatz の Büchi 形式化（約95%）が automaton 側の実例として手元にあるので、縮退の片側は実物で押さえられる。これが最初に書く部分。
5. braid 較正 arc への影響 — 訂正2件・追加3件
訂正1（要反映）：118 → 120
Bigelow 1999 の原文は verbatim で "This is a word of length 120 in the generators."（直接確認済）。118 の出典は見つからず、これより短い元も見当たらない。arc 記述の訂正が要る。
訂正2（要反映）：B₄ の ground truth の格が上がった
Bharathram, Birman & Brendle, "The Burau representation is faithful for n = 4", arXiv:2607.05283（2026-07） が B₄ の Burau 忠実性の証明を主張。Moody 多項式・disk sequence・winding number・point-pushing map による非計算的証明、B₄ ↪ B₅ の埋め込みと Long の定理経由で Brunnian 部分群に帰着。系として B₄ の Jones 表現の忠実性も。査読前。
通れば control arm は「空だと信じている」から「空だと証明されている」へ昇格する。arc にとって有利だが、記述を変える必要がある：「空だと信じている場合で較正する」ではなく「空だと既知の場合で較正する」。
追加1：documented false negative が既に文献にある
Kim, Djun M. (1993), "A Search for Kernels of Burau Representations", Topics in Knot Theory, NATO ASI Series — β₄ と β₅ の核元を計算機探索し、abstract で "(so far unsuccessful!)" と記録。B₅ には実在する（Bigelow 1999）ので、これは実在する対象を見逃した記録済みの偽陰性事例。較正素材として一次資料の価値が高い。
追加2：より tight な matched pair の候補
Burau mod 2 の B₄ は核が非自明（Cooper–Long 1997、Lee 2023 arXiv:2309.05547 が [yxy,x]⁴ を提示）。BBB 2026 が通れば「同じ群・同じ表現・係数環だけが違う」対になり、B₄/B₅ より交絡が少ない。第2の control arm 候補。 ※ Lee 2023 の Smythe / Brendle–Margalit–Putman の帰属関係は要素読み。
追加3：Bigelow 自身が先例の形を持っている
同論文に verbatim で "A similar computer search for the case n = 4 has shown that any pair of arcs on D4 satisfying the requirements of Theorem 1.4 must intersect each other at least 500 times."（直接確認済）。同一手続きを両側に走らせ、片側を bound として報告する形は arc の設計と同形。ただし較正は行っていない。 arc の差分はここに置ける。
6. 反証条件（事前登録）
| # | 条件 | 発火時の処置 |
|---|---|---|
| (a) | §4 の縮退条件が書けない | 「超える」語を撤回、「別の判定器」に降格 |
| (b) | 差分候補 (ii) について、未申告ゲートと誤り率を同時に持つ既存装置が1件でも出る | (ii) を KILL、主張は (i)+(iii) のみ |
| (c) | MEASURED 較正が3装置（停止条件・修正機器・Ctx）で揃わない | 統合主張を保留、装置単体の記述に落とす |
| (d) | SARIF に outcome field を足すだけで (iii) が再現できる | (iii) を KILL（Pattern 5：既存 tool の compose で足りる） |
| (e) | 118→120 の類の一次資料不一致が他にも出る | arc 全体を素材段階に差し戻し |
| (f) | BBB 2026 が査読で崩れる | B₄ control arm を「未証明の信念」に戻し、mod 2 対（追加2）を主 control に切替 |
7. 引用一覧
✓ = 本 audit で直接 fetch して確認 / △ = 検索結果由来、原典未確認
直接確認 ✓
- Bigelow, "The Burau representation is not faithful for n = 5", Geometry & Topology 3 (1999) 397–404 — https://msp.org/gt/1999/3-1/gt-v3-n1-p16-p.pdf ✓（120文字・n=4 の 500 交差の両方を verbatim 確認）
- Bharathram, Birman & Brendle, "The Burau representation is faithful for n = 4", arXiv:2607.05283 — https://arxiv.org/abs/2607.05283 ✓（題・著者・abstract・証明手法を確認）
- Bruns & Godefroid, CAV 1999 — https://patricegodefroid.github.io/public_psfiles/cav99.pdf ✓（実験節なし・⊥ の頻度測定なしを確認）
- Shoham & Grumberg, LICS 2006 — https://www.cs.tau.ac.il/~sharonshoham/papers/lics06.pdf ✓（実験節なしを確認）
- Sen, Viswanathan & Agha, CAV 2004 — http://vmahesh.cs.illinois.edu/papers/cav04.pdf ✓（p値・"don't know" を abstract で確認）
- Mariposa, FMCAD 2023 — https://www.jaybosamiya.com/publications/2023/fmcad/mariposa.pdf ✓（2.6% unstable・Z検定 α=0.05・60 mutants を確認）
- Cohen, Rosenfeld & Kolter, ICML 2019 — https://proceedings.mlr.press/v97/cohen19c/cohen19c.pdf ✓（ABSTAIN の Proposition 1/2 を確認）
- SPEC CPU2017 Run Rules — https://www.spec.org/cpu2017/Docs/runrules.html ✓（§4.6 を verbatim 確認）
- Large Text Compression Benchmark rules — https://www.mattmahoney.net/dc/textrules.html ✓（decompressor + 辞書の同梱要件を確認）
- cvc5 outputs — https://cvc5.github.io/tutorials/beginners/outputs.html ✓（unknown の 2 由来を確認）
- SMT-COMP 2024 rules — https://smt-comp.github.io/2024/rules.pdf ✓（unknown = e0/n0 を確認）
- Angelopoulos et al., "Conformal Risk Control", arXiv:2208.02814 ✓
- Mohri & Hashimoto, "Language Models with Conformal Factuality Guarantees", arXiv:2402.10978 ✓
- Lean.Message API — https://lean-lang.org/doc/api/Lean/Message.html ✓（fileName/pos/endPos/MessageData を確認）
- Vericoding benchmark, arXiv:2509.22908 — https://arxiv.org/pdf/2509.22908 ✓（raw error・kind 別内訳なしを確認）
- ExVerus, arXiv:2603.25810 — https://arxiv.org/pdf/2603.25810 ✓
検索結果由来 △（引用前に原典確認が要る）
- Larsen & Thomsen, "A Modal Process Logic", LICS 1988 △（DOI は file path から推定）
- Belnap, "A Useful Four-Valued Logic", 1977 — DOI 10.1007/978-94-010-1161-7_2 △
- Chechik, Devereux, Easterbrook & Gurfinkel, "Multi-Valued Symbolic Model-Checking", TOSEM 12(4) 2003 — https://www.cs.toronto.edu/~sme/papers/2003/TOSEM-mvmodelchecking.pdf
- Cousot & Cousot, POPL 1977 — https://www.di.ens.fr/~cousot/COUSOTpapers/POPL77.shtml
- O'Hearn, "Incorrectness Logic", POPL 2020 △
- Ball et al., "Thorough Static Analysis of Device Drivers", EuroSys 2006 — https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/eurosys2006-1.pdf △（カテゴリ別件数は要再読、自動要約で整合しなかった）
- SV-COMP rules — https://sv-comp.sosy-lab.org/2025/rules.php
- "Abstract Interpretation with Confidence", DOI 10.1145/3808351 △（ACM 403、OpenAlex 経由のメタデータ）
- Goldreich, Goldwasser & Ron, JACM 45(4) 1998 △（巻号ページ未確認）
- Rubinfeld & Sudan, SICOMP 25(2) 1996 — https://people.csail.mit.edu/ronitt/papers/rs.pdf
- Younes & Simmons, CAV 2002 — doi:10.1007/3-540-45657-0_17
- Legay, Delahaye & Bensalem, RV 2010 — doi:10.1007/978-3-642-16612-9_11
- Vovk, Gammerman & Shafer, Algorithmic Learning in a Random World, Springer 2005 / 2nd ed. 2022 — https://www.alrw.net/
- Vovk, "Conditional validity of inductive conformal predictors", ACML 2012 — https://arxiv.org/abs/1209.2673
- Chow, "On Optimum Recognition Error and Reject Tradeoff", IEEE TIT 16(1) 1970 △（DOI 未確認）
- El-Yaniv & Wiener, JMLR 11 (2010) — https://jmlr.org/papers/v11/el-yaniv10a.html
- Geifman & El-Yaniv, NeurIPS 2017 — https://arxiv.org/abs/1705.08500
- Madras, Pitassi & Zemel, NeurIPS 2018 — https://arxiv.org/abs/1711.06664
- Guo et al., "On Calibration of Modern Neural Networks", ICML 2017 — https://arxiv.org/abs/1706.04599
- Callaghan & Müller-Hansen, Systematic Reviews 9:273 (2020) — https://doi.org/10.1186/s13643-020-01521-4
- Cormack & Grossman, TREC 2016 Total Recall — https://trec.nist.gov/pubs/trec25/papers/WaterlooCormack-TR.pdf
- Dolan-Gavitt et al., "LAVA", IEEE S&P 2016 — https://seclab.nu/static/publications/sp2016lava.pdf
- MacKenzie et al., Ecology 83(8) 2002 — https://www.sfu.ca/~lmgonigl/materials-qm/papers/mackenzie-2002-2248.pdf
- Bringolf, Winterer & Su, ASE 2022 — https://dl.acm.org/doi/10.1145/3551349.3560435
- Livshits et al., "In Defense of Soundiness", CACM 2015 — https://yanniss.github.io/Soundiness-CACM.pdf
- SARIF v2.1.0 — https://docs.oasis-open.org/sarif/sarif/v2.1.0/os/sarif-v2.1.0-os.html
- Sadowski et al., "Tricorder", ICSE 2015 — https://static.googleusercontent.com/media/research.google.com/en//pubs/archive/43322.pdf
- Seo et al., "Programmers' Build Errors", ICSE 2014 — https://research.google.com/pubs/archive/42184.pdf
- Mesbah et al., "DeepDelta", ESEC/FSE 2019 — https://people.ece.ubc.ca/amesbah/resources/papers/deepdelta-fse19.pdf
- Becker et al., "Compiler Error Messages Considered Unhelpful", ITiCSE-WGR 2019 — https://amirkamil.com/papers/iticse19.pdf
- Jose & Majumdar, "Cause Clue Clauses", PLDI 2011 — https://bugassist.mpi-sws.org/MJPLDI11.pdf
- Zeller & Hildebrandt, TSE 2002 — https://www.cs.purdue.edu/homes/xyzhang/fall07/Papers/delta-debugging.pdf
- Ringer et al., "Proof Repair Across Type Equivalences", PLDI 2021 — https://arxiv.org/abs/2010.00774
- First et al., "Baldur", ESEC/FSE 2023 — https://arxiv.org/abs/2303.04910
- Kim, Djun M., "A Search for Kernels of Burau Representations", 1993 — doi:10.1007/978-94-011-1695-4_17 △
- Long & Paton, Topology 32(2) 1993 △ / Moody, Bull. AMS 25 1991 △
- Lee 2023 — https://arxiv.org/abs/2309.05547 △（帰属関係の記述に要注意）
- Heule–Kullmann–Marek, arXiv:1605.00723 / Heule, arXiv:1711.08076 / Brakensiek et al., arXiv:1910.03740（DRAT/LRAT による不在の証明書化の先例）
- Clarke, Kroening, Ouaknine & Strichman, VMCAI 2004（completeness threshold） / Angluin 1987 §4（PAC 等価性）/ Chow 1978（W-method）
8. この audit 自体の限界
- 差分候補 (ii) の negative は約6通りの query 定式化に基づく bounded search の結果であり、不在証明ではない。本装置が扱う問題そのものが、この audit 自身にも適用される。
- §7 の △ 項目は原典未確認。引用に使う前に direct verify が要る。
- 検索は英語文献中心。日本語・ロシア語文献（Vasilevskii 1973 など）は未踏。