世界、断片、モデル。そして理解

本資料は、現実世界の文書・会話に埋もれる制約、計算式、判断理由などの「断片」を、Evidence→Candidate→Core Modelの段階で追跡可能な形式仕様へ育てる開発像を示す。簡単な例を通じ、VDM-SLのpre/postが「何が正しいか」を固定し、設計・実装・運用の自由とAI生成物の検証を支えることを説明。さらに、AIが人間の理解を追い越す「認知負債」に対し、形式仕様を記録ではなく、説明・反例・変更を通じて理解を試す足場として活用する。人とAIの役割を整理。
最終的に、結果としての仕様で終わらず、モデルコアへ問い続けて人間の理解を育てる「理解駆動開発」を提案する。（CC BY-NC 4.0）

Transcript

1. フレスコラジヲ 世界⇒断⽚⇒モデル そして理解 ̶ 現実世界とシステム世界の橋渡し ̶ 酒匂 寛 Designers' Den Corp. 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0)
2. ツール モジュラリティ 形式手法 生産性の向上 柔軟性の向上 抽象化による再利用性の向上 信頼性の向上 保守性の向上 コミュニケーションの向上 next ..? Unix / WS Object-Oriented Formal Method 再びツールに回帰しようかと考え ていたところに生成AIの大波🌊が 生成AI どのように支援する？ 酒匂寛 - 自己紹介（開発編） 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0) 01
3. 開発 教養・一般 教育 医学・生物系 酒匂寛 -自己紹介（書籍編） 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0) 02
4. PROBLEM モデリングツールは、最終結果しか残さない。 調査・議論の過程 ヒアリング・⽂書・検討 最終成果物 図・モデル・コード 過程で⽣まれる断⽚ 制約条件 計算式 判断理由 記録されず、消えていく 「なぜこのモデルなのか」を後から辿れない ̶ 資料と解釈が散らばる。 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0) 03
5. PROBLEM モデリングツールは、最終結果しか残さない。 調査・議論の過程 ヒアリング・⽂書・検討 最終成果物 図・モデル・コード 過程で⽣まれる断⽚ 制約条件 計算式 判断理由 記録されず、消えていく 「なぜこのモデルなのか」を後から辿れない ̶ 資料と解釈が散らばる。 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0) 04 地図 現地 Tinkering ティンカリング
6. WHERE MODELING BEGINS モデリングは、コードを書く前に始まっている。 現実世界 記述・映像・⽂書・会話 その中に「式の種」が埋まっている 制約 ・ 計算 ・ 論理 システム世界 仕様・実装・テスト 形式的で、検証可能な記述の世界 ？ 断⽚を拾い上げ、育てるための「作業場」が既存ツールに⽋けている。 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0) 05
7. PROTOTYPE 試作: 概念モデルエディタMVP ̶ 断⽚が成熟する3つの段階 Evidence 資料には何が書かれているか まだ解釈しすぎない Candidate そこから何が⾔えそうか まだ正本にしない Core Model ⼈間が採⽤した正本 変更履歴を残す AIが抽出・提案 ⼈間が採否・統合 Source Evidence Observation Candidate Decision Core Model AIを使っても由来と責任が曖昧にならない ̶ Traceable / Reviewable / Changeable 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0) 06
8. EXAMPLE 1/3 ̶ count7 ⽣の記述から、式を抽出する。 Evidence ̶ 依頼者の⾔葉のまま E1 依頼メモ 「1 から n までの整数を順に書き出したとき、数字の 7 が全部で何回現れるかを知りたい。たとえば n = 7 なら 1回、n = 17 なら 2回（7 と 17）。」 ※ 業務ドメイン（受注〜出荷など）でも構図は同じ。 Candidate ̶ 式として抽出（出所つき） 分解の発⾒: count7(n) ＝ count7(n−1) ＋ n に含まれ る 7 の個数 ← E1「1 から n まで」「何回現れるか」 基底の発⾒: n ＝ 0 のとき 0 ← 分解が⽌まる場所として 補助概念の発⾒: digit7s(n) ＝ 1つの数に含まれる 7 の 個数 digit7s(7)=1, digit7s(721)=1, digit7s(770)=2 判断（⼈間の裁定）: 「現れる回数」は数字単位で数える ̶ 77 は 2回と数える。（理由を履歴に記録） 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0) 07
9. EXAMPLE 2/3 ̶ count7 Core Model は、たとえばVDM-SL の陰仕様として書ける。 count7 : nat -> nat count7 (n) == is not yet specified pre n >= 0 -- 型が nat なので本当は冗長 post RESULT = cases n: 0 -> 0, others -> count7(n - 1) + digit7s(n) end; digit7s(n) : 1つの数に含まれる 7 の個数を返す補助関数 ① Candidate の「分解」「基底」が、そのまま post 条件に写る（trace） ② 本体は is not yet specified ̶ 何を満たすべき かだけを書き、どう計算するかは書かない（陰仕 様） ③ pre は nat 型ゆえ冗⻑ ̶ 型もまた仕様の⼀部 ④ この段階で検証できる: post に n = 7 を当てれ ば count7(7) = 1 が確認できる 「何が正しいか」が、ここで凍結される。 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0) 08
10. EXAMPLE 3/3 ̶ count7 post は実装としても動く。しかし、それは設計ではない。 案1: 仕様の丸写し ̶ O(n) count7 : nat -> nat count7 (n) == if n = 0 then 0 else count7(n - 1) + digit7s(n) measure n; 正しい。しかし n = 10⁹ なら再帰 10⁹ 回 ̶ 実⽤にならない。 正しさの基準は、どちらも同じ post ただ⼀つ。 count7(7) = 1 count7(17) = 2 count7(77) = 16 ̶ 両実装とも⼀致することを検証できる 案2: 設計された実装 ̶ O(log n) count7 : nat -> nat count7 (n) == count7pos(n, 1); count7pos : nat * nat1 -> nat count7pos (n, p) == if p > n then 0 else let high = n div (10 * p), cur = (n div p) mod 10, low = n mod p in ( if cur > 7 then (high + 1) * p elseif cur = 7 then high * p + low + 1 else high * p ) + count7pos(n, 10 * p) measure n div p; 桁位置ごとの閉じた式 ̶ digit7s は現れず、構造は仕様と別物。 この距離こそが「設計」。 仕様は「正しさ」を凍結し、設計の⾃由を⽀える ̶ AIが書いた実装も post で検証できる。 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0) 09
11. DEMO ̶ count7 実⾏効率ビューア 実測: 同じ post、実⾏効率は桁違い。 ① naive O(n): 実⾏時間は n にほぼ⽐例 して伸びる（⾚） ② fast O(log n): 最後まで 0.003 ms 級（ ⻘）̶ 速度⽐は約620倍（n=1000・100 回計測） ③ naive ＝ fast が全 1000 件で⼀致 ̶ 同じ post を満たす2つの設計であること の検証 ④ ブラウザで実演可能（count7-viewer ）。数値は測定環境により変動する 仕様が同じだから、速さは安⼼して選べ る。 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0) 10
12. EXAMPLE 1/3 ̶ N営業⽇後 ⽣の記述から、式を抽出する。 Evidence ̶ 実世界の記述のまま E1 業務要求 「指定⽇から N 営業⽇後の⽇付を返す機能が欲しい。」 E2 会社就業規則 「⼟⽇・年末年始（12/29〜1/4）・創⽴記念⽇（7/4）は 休業とする。」 E3 祝⽇法 第三条（要旨） 「『国⺠の祝⽇』は、休⽇とする。⽇曜⽇に当たるときは 、直後の『国⺠の祝⽇』でない⽇を休⽇とする。」 Candidate ̶ 式として抽出（出所つき） 補助概念の発⾒: 営業⽇(d) ⇔ ¬⼟⽇ ∧ ¬祝⽇ ∧ ¬年末 年始 ∧ ¬創⽴記念⽇ ← E2・E3 保証の発⾒: 結果は営業⽇であり、指定⽇より前になら ない ← E1「後の⽇付」 数え⽅の発⾒: 指定⽇の翌⽇から結果までの営業⽇数 ＝ ちょうど N ← E1「N営業⽇後」 判断（⼈間の裁定）: 指定⽇そのものが営業⽇であることを前提（事前条件）とする。N ＝ 0 なら指定⽇を返す。（理由 を履歴に記録） 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0) 11
13. EXAMPLE 2/3 ̶ N営業⽇後 Core Model は、たとえばVDM-SL の陰仕様として書ける。 types Date = nat; -- 通し日に抽象化 functions is_bizday : Date -> bool is_bizday (d) == not ( is_holiday (d) or is_weekend (d) or is_yearend (d) or is_founding (d) ); after (d : Date, n : nat) r : Date pre is_bizday (d) post is_bizday (r) and r >= d and card { x | x : Date & d < x and x <= r and is_bizday (x) } = n; is_holiday の定義は、祝⽇法 → 政令 → 天⽂台の確定値へと続く ① Candidate の3つの発⾒が、そのまま pre / post に写る（trace） ② 「ちょうど N」は card（集合の要素数）で書 ける ̶ 数え上げの⼿順は書かない（陰仕様） ③ N = 0 の判断は post から導ける: r = d のとき 集合は空で card = 0 ④ この段階で例による検証: ⾦曜 + 1営業⽇ = ⽉ 曜、連休またぎ… を post で確認できる 「1⾏の要求」の正体が、ここで凍結される。 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0) 12
14. EXAMPLE 3/3 ̶ N営業⽇後 post は設計を語らない。設計は運⽤へつながる。 案1: 素朴な設計 ̶ 実⾏時にすべて計算 • 1⽇ずつ進めながら is_bizday を判定 • 祝⽇も毎回その場で計算（振替休⽇・国⺠の休⽇…） • 春分⽇・秋分⽇は天⽂計算が必要になる post は満たせても、法改正・特例年に追随できず、誤判定リスクと 実⾏時コストが⾼い。 正しさの基準は、どちらも同じ post ただ⼀つ。 ⾦曜+1=⽉曜、連休またぎ、年末年始 ̶ 例で両設計を検証でき る 案2: 設計された実装 ̶ 事前確定マスタ参照 • holiday_master: 1⽇1⾏の確定データ。実⾏時は date → bool の参照のみ • 祝⽇ロジックは年次バッチで事前計算し、官報・内 閣府の確定値と突合 • 更新の検証・承認・監視（3年分の充⾜チェック） までを運⽤として設計 実⾏時に「計算しない」という設計判断。 設計は実⾏時と運⽤時の分担まで決める。 仕様は「正しさ」を凍結し、設計は運⽤へつながる ̶ 業務でも構図は count7 と同じ 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0) 13
15. BIG PICTURE ⼆段の橋 ̶ 現実世界とシステム世界をつなぐ 現実世界 記述・映像・⽂書 モデルの種 概念・関係・制約（VDM-SL） Core Model ex. 形式仕様 第⼀の橋: 抽出と採否 第⼆の橋: 変換と検証 AI 各段の「翻訳者」̶ 候補を出 し、変換する ⼈間 各段の「裁定者」̶ 採否し、 理由を残す 断⽚と判断が残るからこそ、⽣成AI時代の開発は安全になる。 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0) 14
16. 第⼀部まとめ 断⽚（制約・計算式・判断理由）は最終結果と同等の価値を持つ ̶ 残して育てる「作業場」が要る 断⽚は早い段階から「式」として抽出できる ̶ VDM-SL のような抽象記述がその受け⽫になる 断⽚の段階でも、「式」にすることで、可視化して、正しさを皆で確認できる→反駁可能性 問いかけ Q1 形式仕様（論理と集合）は、⽣成AI時代の「中間⾔語」になり得るか？⾜りないものは何か？ Q2 断⽚を仕様（モデル）にまとめていく過程での⼈間との対話のありかたとは？ 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0) 15 仕様は「何が正しいか」を凍結し、設計と実装の⾃由を⽀える ̶ AI の⽣成物も仕様で検証できる Q3 形式仕様記述やそれに基く対話ツールは認知的負債を減らす役に⽴つか？ → 第⼆部で回答
17. 第⼆部 「新たなる負債」へのレスポンス ̶ 形式仕様は、認知負債に何ができるか ̶ 問題提起 『Agentic Software Engineering』 ̶ Scrum Fest Niigata 2026 より 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0)
18. 問題提起: 新たなる負債 技術的負債（コードの質）は、コーディングエージェントの進化でむしろ改善の傾向にある 認知負債: AIが⼈間の理解より速くコードを⽣成し、開発の過程で形成されるはずだったメンタルモ デルが形成されない 技術的負債は⾒えるが、認知負債は⾒えない ̶ 理解の乖離を測るメトリクスはまだない 参照 出典 『Agentic Software Engineering』̶ Scrum Fest Niigata 2026 分類 Storey (2026): Intent Debt（意図）と Cognitive Debt（理解）に分ける 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0) 16 Naur (1985)「プログラミングとは理論の構築」̶ 理論を失えば、コードが動いていてもプログラム は死んでいる 警句 「思考は外注できるが、理解は外注できない」̶ Karpathy
19. DEBT MODEL 形式仕様は、⼆つの負債に同じようには効かない。 Intent Debt ⽬的・制約・判断が失われる Formal Specification 何が正しいかを外在化 Cognitive Debt 理解が追いつかない 外在化で減らす 理解を試して減らす Intent Debt へ Evidence・Decision・仕様を 残す Cognitive Debt へ 説明・反例・変更で理論を育て る Intent は記録で残せる。理解は⾏為でしか確かめられない ̶ 仕様は理解を確認するための⾜場となる。 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0) 17
20. THEORY BUILDING 形式仕様を「理解を試す場」として使う。 外在化 ⽬的・制約・判断理由を EvidenceとDecisionに残す 反駁 反例・境界条件・⽭盾で Candidateを揺さぶる 再構成 ⾃分の⾔葉で説明し 変更して修復できる AIが候補・反例を⽣成 ⼈間が説明・採否・修復 Source Evidence Candidate Counterexample Decision Core Model 理解は成果物の所持ではなく、根拠を説明し、壊さずに変更できる能⼒として⼈間に宿る。 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0) 18
21. HARNESS AI⽣成の⾮決定性には、「仕組みで気づける」流れで応える。 Evidence / Intent 現実・⽬的・制約 Core Model 実⾏可能な仕様 ̶ 型・pre/post・ 不変条件 AI Output 設計・実装・テスト Trace: 導出根拠を確認 Verify: 仕様との⼀致を検証 AI 抽出・候補⽣成・実装・反例探 索 ⼈間 採否・説明・リスク判断・仕様 更新 誤りをゼロにせず、差分を発⾒し、仕様か実装へ戻せるようにする。 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0) 19
22. 回答: 形式仕様は負債を返済可能にする Intent Debt: ⽬的・制約・判断を Evidence → Decision → Core Model として残す Cognitive Debt: 反例・説明・変更を通じて、⼈間の理論があるかを確かめる 形式仕様は理解の代替ではない ̶ 共有・反駁・再構成のための対象である 議論したいこと Q1 「理解した」を、説明・反例・変更のどの⾏為で確認するか？ Q2 Intentから仕様まで、どの判断を⼈間の裁定として残すか？ 2026/07/10 © 2026, Sako Hiroshi (CC BY-NC 4.0) 20 AIの⾮決定性には、仕様との差分を検出し、戻れるプロセスで応える Q3 仕様の誤りと実装の誤りを、どう切り分けて戻すか？
23. ndays_after.vdmsl ・VDM-SLによる仕様 ・仕様に「質問」 この仕様をもとに、 2026年9月22日が休日か どうかを判定してくだ さい ・その答 仕様との「対話」を通した「理解」 © 2026, Sako Hiroshi (CC BY-NC 4.0)
24. UNDERSTANDING-DRIVEN DEVELOPMENT 理解駆動開発 ̶ モデルコアに問い、理解を育てる。 結果としての仕様で終わらない。モデルコアに問い続け、⼈間の理解を育てる。 2026/07/10 22 なぜ？ 条件が 変わったら？ 反例は？ 説明して みよう © 2026, Sako Hiroshi (CC BY-NC 4.0)