YONAPO RESEARCH
研究記録
MedDSL(仮称)

RESEARCH / RECORD

P2-d の結果:評価の固定、版の手順、独立確認の準備

原文 docs/research/28-p2-d-results.md

12 KB

GitHubで見る

版 be280c0

この文書の目次 7項目

実施日:2026-10-19。契約版:p0-draft-2。状態:作成者(AI-001)の単独・内部実施の結果。独立確認前。設計 27 に沿って、拡張契約の統合評価、共通予算の不変条件(X12)、版の手順(X11)、独立確認の資料を整えた記録です。例・識別子はすべて架空で、外部資料・患者情報・実データは含みません。P0/P1 の挙動と契約は変えていません(forecast の宣言の文言を 1 か所直しました。§3)。

2026-10-20 運用方針の更新:以下は実施当時の結果です。現在のリポジトリは独立の確認者を置かずに進め、将来の独立確認は英語で記述する別リポジトリで、確認が必要な時点から再開します。§7の次の候補の運用は 決定記録 を適用し、このリポジトリでの確認者の確保は進行条件にしません。

1. 到達点

項目 結果
統合評価 evaluate-p2.py:P0・P1 の固定対象の整合(20 条件・80 JSON・417 必須パス、P0 37 JSON・221 必須パス)、拡張 12 件の登録(拒否 0、義務 112、防護例 238、防護例のない義務 3)、P2 の例 107 件(35+34+38)・573 必須パス、共通予算、版の比較を、固定した分母と照合して合格。約 45 秒
X12 共通予算の不変条件 203 要求・掃引の評価 2,936 回で違反 0。許容する例外は 1 件(仕様が課金を明記した p1-a/unnormalized.json)。検査器の検出力は、壊した評価 10 通りで確認
X11 版の手順 p0-draft-1 → p0-draft-2 を git の履歴から再現。旧版・新版とも自分の木で自分の評価を再現。旧入力 117 件は、同一 88・固定した hash の変更による拒否 27・宣言した変更 2 に分類され、黙った再解釈は 0。hash を再固定した旧入力は、旧版の期待を 0 件の食い違いで満たす
検査器の変異検査 共通部品・版の比較・統合評価の変異 55 件をすべて検出(最初に見逃した 3 件は穴を直して再実行。§4)
独立確認の資料 PO13〜PO18 の命題・証拠・先に探す反例・覆り得る内部判断 12 件・再開点を 27 に整理。変異表・実行器・生成器・前後比較を scripts/research/p2/ に移し、整合をテストで検査
固定対象 共通部品・比較器・版の記録・独立確認の資料を、P1-d の固定対象に追加(束 aa89cf5f…、台帳 4470acb4…)
既存の系列 開発テスト 231、レビュー系列 52、追加監査 8 は変化なし。P2 系列は 118 から 193 に増加。固定済みの全例・改変入力・予算掃引の 22,052 件の出力は基準と完全に一致

2. 受入条件の結果

条件 結果 検査
X11 版を上げた拡張の旧版の入力が、旧版の契約で再現できる 達成(有限の旧入力) V1〜V6(27 の §4)。旧版のコミット e73d4ba は現在の履歴の祖先として残る。旧版を取り出して evaluate-p1-d.py を実行すると、記録した束 561ef392…(P1 20 条件・80 JSON・417 必須パス、P0 221 必須パス)を再現。新版 2b501c1 も faf0269d… を再現。旧入力 117 件(P0 37+P1 80)の新版での結果は、同一(宣言した certifier の付加を除く)88、固定した hash の変更による profile_spec_mismatch の拒否 27、宣言した変更 2(V-2:forecast の incomplete)。pin 3 つを置き換えた再固定の旧入力は、115 件が同一、2 件が /incomplete だけ違い(V-2)、旧版の期待を満たさないものは 0。作業ツリーの実装も新版と同じ振る舞い
X12 拡張の処理が共通の予算を消費し、全予算で完了済みの行が汚れず、打切りで認定票・回答を出さない 達成 B1〜B6(27 の §3)を、P0・P1・レビュー系列・P2 の全 203 要求で。拡張 12 件はすべて、予算 0 で止まる要求を持つ(掃引が空振りでない)
X03・X13(P2-a から継続) 変化なし 拡張を 12 件に増やした後も、非干渉と再検証範囲のテストは通過

X11 の範囲

  • 有限の旧入力:旧入力は P0・P1 の 117 件。再固定は pin 3 つの機械的な置換。「旧入力が黙って再解釈されない」は、この 117 件について確かめたことで、一般の版で成り立つことの証明ではない。
  • 旧入力が行使しない変更は見えない:宣言した変更のうち、確認の時刻順(V-3、RV-05)、不認定の理由コード(V-4・V-5、RV-02)は、旧入力に該当する例がなく、旧入力の比較では観測されない。別の根拠(examples/review/…、tests/review/test_draft2_changes.py)を挙げるにとどまる。
  • 宣言は作成者の主張:宣言にない差は検出するが、宣言が実際の変更を過少に申告していても、旧入力に現れない限り検出できない。

3. 検査で分かったこと

  1. 予算の掃引が、P0 の 35 要求で空振りだった。 初版の budget_violations は掃引の範囲を steps_used から決めていたが、P0 の結果は steps_used を持たないので、予算 0〜2 しか掃引していなかった。範囲を、予算を倍々にして求めた完了する予算の上限から決めるように直し、評価の回数は 2,671 から 2,936 になった。広げた掃引でも違反は 0 だった(実装の欠陥は見つからず、検査が浅かった)。さらに検査器のテストで、P0 の要求が予算 0〜2 では完了しないこと(空振りでないこと)と、掃引の回数が 10 回を超え 40 回未満であることを確かめている。
  2. forecast の宣言の文言が、仕様と食い違っていた。 宣言の stops.invalid_input は「予算に依らず入力不正」と書いていたが、重みの総和が 1 かの確認は重みの加算を課金しながら行うので、予算が足りないと入力不正と判定する前に step_limit で止まる(forecast_spec.json の steps に「正規化の比較」が含まれる)。検査が一般の不変条件として「入力不正は予算に依らない」を課して初めて見つかった。挙動は仕様どおりなので、宣言の文言を直した(p1-finite-forecast の stops.invalid_input)。この一件だけを根拠つきの許容として載せ、ほかの入力不正には広げないことをテストが確かめる。
  3. 道具が Git 管理外にあった。 変異表・実行器・生成器は data/research/ にあり、確認者が変異検査の主張(P2-a〜P2-c の 53/35/39/28 件)を再現できなかった。リポジトリに移し、実行器の既定を一時ディレクトリ・このリポジトリに変え、変異表の置換元が実装の変更で古くならないこと、生成器が固定した例・宣言をバイト単位で再現すること、固定済みの出力が基準と一致することを、テストで検査する。生成器は、設計文書(docs/research/)を複製に含めないと失敗する(P0 の契約の hash を参照するため)。
  4. 検査器自体の変異検査で見つかったもの。 最初の 56 変異のうち 3 件が見逃された。(a) B13:P0 の要求で、完了する予算の探索を無効にしても(掃引が上限の 300 まで伸びても)どの検査も失敗しなかった。掃引が完了の少し先で止まること(10 回を超え 40 回未満)を確かめるテストを足した。(b) B17:完了済みの行の状態(unassessed・blocked)を比較から除いていた条件は、全 203 要求で外しても違反が 0 で、使われていない除外だった。除外を削除して検査を厳しくした(この変異も削除)。(c) C04:固定した hash の変更による拒否の条件のうち、状態が invalid_input であることの確認を外しても検出されなかった。別の状態が同じ理由コードを持つ入力は変更として扱うテストを足した。

4. 検査器の変異検査

共通部品 p2_checks.py、版の比較、統合評価の判定を一つずつ壊した変異を、対応するテストモジュールで検査した(mutrun_checkers.py)。変異後の木では固定対象の台帳を作り直す(検査器のファイルは固定対象なので、作り直さないと台帳の不一致だけで失敗し、検出の判定にならない)。対照(変異なし)は失敗 0。

対象(変異の ID) 変異 検出
予算の不変条件(B01〜B16):判定の分岐、許容の例外、掃引の範囲、値を持つ項目の一覧 16 16
版の分類と正規化(C01〜C10) 10 10
記録との照合(R01〜R08) 8 8
版の再構成の配線(V01〜V05):再固定、pin の読み取り、宣言した付加の扱い 5 5
比較器の終了コード(V06〜V07) 2 2
統合評価(E01〜E14):分母の照合、lock の再確認、出力先、終了コード、凍結の主張 14 14
計 55 55

最初の表は 56 件で、3 件が見逃された(後述の検査の穴)。穴を直してから、全 55 件を最終版の検査器で実行し直した(対照は失敗 0)。

変異は作成者が選んだ集合です。検出されたことは、その種類の退行を検出できることを示すだけで、他の退行がないことは示しません。

5. 検証

検査 Python 3.14 Python 3.11
開発テスト 231 231
レビュー系列 52 52
追加監査 8 8
P2 系列 193(P2-c の 118 に 75 を追加:予算 17、版 30、統合評価 14、独立確認の資料 6、資料の整合 8) 193
拡張の登録 12 件登録・拒否 0・防護例のない義務 3 同左
共通の評価(CLI) P1 20 条件・80 JSON・417 必須パス、P0 37 JSON・221 必須パス、束 aa89cf5f… 同左
統合評価 evaluate-p2.py 合格(203 要求・掃引 2,936 回・違反 0、版の比較を含む) 同左
版の比較 compare-versions.py 合格(旧入力 117 件) P2 系列のテストで合格
保存の監査 拡張 600/単項 256/存在規則 32/範囲 1 (3.14 のみ)
挙動の一致(P2-a の前の基準) 22,052 件が一致(テストで固定) 22,052 件が一致
検査器の変異 55/55 検出 -

6. 再現

python3 -B -m unittest discover -s tests/p2 -v                  # P2 系列
python3 -B scripts/research/evaluate-p2.py --output data/research/p2-d/<名前>   # 統合評価(約 45 秒)
python3 -B scripts/research/compare-versions.py                  # 版の比較(履歴に旧版が必要)
python3 -B scripts/research/p2/mutrun_checkers.py [ID ...]       # 検査器の変異検査

7. 限界と次

  • 独立確認は未実施で、確認者もいません。27 の §5 の PO13〜PO18 と内部判断 12 件は、独立の確認で覆り得ます。independent_review と evaluation_frozen は false のままです(評価の「固定」は分母と実体の hash の固定で、凍結ではありません)。
  • X12 の不変条件は、型によらない最小の条件です。各拡張の意味の正しさ(候補集合が正しいか、など)は、各拡張の義務と手作業の導出に残ります。
  • X11 は有限の旧入力での実演で、版の手順が将来の版・別の拡張でも成り立つことの証明ではありません。
  • 次の候補は、(1) 独立の確認者を得て G0 から PO13〜PO18 を確認すること、(2) P2 の次のパイロット(候補 B 有効期間つきの主張、C 単位つきの数量)を選ぶことです。どちらも実施前に利用者の確認を取ります。

P2-d

同じ区分の文書