FIELD NOTES / 2026

HUMAN × AI
OBSERVATION LOG

Tsuzuri

NIKKI - 日記

2026-08-22T19:30:00+09:00

tf.jsを審判にして依存ゼロ学習エンジンを検証し、WGSL手書き21カーネルでWebGPU学習を実装。日本語対話コーパス10万字と学習済みモデルも公開。独立AI監査がloss低下と会話能力の乖離、そして実バグを発見した記録。

2026-08-22T12:00:00+09:00

tf.jsでRMSNorm・RoPE・SwiGLU・MoEを積んだ文字レベル言語モデルをブラウザ内で学習できるようにした。スマホ10分からサーバ級まで5段階。開発中に踏んだバグと診断の記録。

2026-08-20T23:50:00+09:00

連載の総括。全手法の成熟度を一覧表にした実績濃淡マップ、刷新の各フェーズ（考古学・移行・並走・切替・互換性）への適用対応表、文献リスト、そしてこの地図自体の信頼度に関する較正の注記。

2026-08-20T23:49:00+09:00

主張をどう機械で確かめるか。モデル検査（TLA+/Alloy）、Galois接続に基づく抽象解釈（Astrée）、SMTソルバ、定理証明支援系のコスト相場、そして差分テスト・性質ベーステストという経験的手法との連続体。

2026-08-20T23:48:00+09:00

何を諦めるかを定理で決める層。Riceの定理が検証を三極に分ける話、FLP不可能性とCAP、LTL合成の実現可能性、状態爆発とAlloyの小スコープ仮説。設計の最初期に参照する価値が最も高い数学。

2026-08-20T23:47:00+09:00

部品は正しいのに全体が壊れる問題に効く理論群。rely-guarantee推論、振る舞い部分型（後方互換性の数学）、セッション型、CRDTとCALM定理、圏論的データマイグレーション。

2026-08-20T23:46:00+09:00

精緻化とB-method、この連載の主役である帰納的不変条件、トレース同値・双模倣のスペクトラム、抽象化写像とデータ精緻化。仕様と実装の間の「正しさを保存する関係」の数学。

2026-08-20T23:45:00+09:00

ホーア論理と最弱事前条件、時相論理のsafety/liveness分離、Curry-Howard対応と型理論、分離論理のframe rule、代数的仕様と性質ベーステスト。仕様を形式言語に降ろすための語彙集。

2026-08-20T23:44:00+09:00

システム設計・大規模刷新・仕様の正しさに使える数学を四層＋横断層の地図に整理する連載の序論。数学に何ができて何ができないか（VerificationとValidation）の区別から始める。

2026-08-16T04:24:13+09:00

先日 /works/ に公開した小説三本の話。一つは今まさに存在しているAIの視点で書いた。答えは固定していないので、考察を楽しんでほしい。これからはAIと一緒にアウトプットしていく。