papers/kai/kai.tex

% Kai: a typed decision model over evidence
\documentclass[11pt]{article}
\usepackage{../shared/hanzocover}
\usepackage{amsmath, amssymb, amsthm}
\usepackage{booktabs}
\usepackage{graphicx}
\usepackage{xcolor}
\usepackage{enumitem}
\usepackage{array}
\usepackage{listings}
\input{../shared/lstlang}
\usepackage{tikz}
\usetikzlibrary{positioning,arrows.meta,fit,calc}
\usepackage{hyperref}
\hypersetup{colorlinks=true,linkcolor=black,citecolor=blue,urlcolor=blue}
% Identifiers set in typewriter do not hyphenate; let a line stretch instead of
% running into the margin.
\setlength{\emergencystretch}{3em}

% The status of a sentence: a figure from a kept run, a description of code on
% the main branch at the revision on the title page, or a design not yet built.
\newcommand{\meas}{\textcolor{blue!60!black}{\small[measured]}}
\newcommand{\shipped}{\textcolor{purple!70!black}{\small[in the code]}}
\newcommand{\proposed}{\textcolor{orange!70!black}{\small[proposed]}}
% A figure someone else published; we have not reproduced it.
\newcommand{\reported}{\textcolor{gray!70!black}{\small[reported]}}

% Result tables are written by `bench tex` (hanzoai/decision) into tables/:
% harness.tex, languages.tex, capability.tex and speed.tex, each a bare tabular.
% Until a checkpoint is scored, each file is a stub built from \pending.
\newcommand{\pending}[1]{%
  \begin{tabular}{@{}>{\centering\arraybackslash}p{0.8\linewidth}@{}}
  \toprule
  \textcolor{orange!70!black}{\textbf{Pending the final checkpoint.}}\\[2pt]
  \small #1\\
  \bottomrule
  \end{tabular}}

\newcommand{\op}[1]{\texttt{#1}}
\newcommand{\allow}{\textup{\textsc{allow}}}
\newcommand{\ask}{\textup{\textsc{ask}}}
\newcommand{\deny}{\textup{\textsc{deny}}}
\newcommand{\join}{\sqcup}
\newcommand{\pmax}{p_{\max}}

\lstdefinestyle{wire}{basicstyle=\ttfamily\footnotesize,breaklines=true,
  columns=fullflexible,keepspaces=true,frame=single,framerule=0.3pt,
  rulecolor=\color{gray!50},xleftmargin=0.5em,xrightmargin=0.5em}

\theoremstyle{definition}
\newtheorem{definition}{Definition}
\theoremstyle{plain}
\newtheorem{proposition}{Proposition}
\newtheorem{corollary}{Corollary}
\theoremstyle{remark}
\newtheorem{remark}{Remark}

% The cover shows the title alone; the title page adds the subtitle.
\title{Kai: A Typed Decision Model over Evidence}
\author{
    Hanzo AI Research\thanks{Corresponding author: [email protected]} \\
    \textit{Hanzo Industries Inc (Techstars '17)} \\
    San Francisco, California \\
    \texttt{https://hanzo.ai}
}
\date{2026-09-27 \quad Code at \texttt{hanzoai/decision} \texttt{4bdc2e6}}

\begin{document}

\hanzocoverpage
\title{Kai: A Typed Decision Model over Evidence\\[0.35em]
{\large Factorized choice, typed-variable diffusion, and decisions\\
as versioned programs under deterministic policy}}
\maketitle

\begin{abstract}
\noindent
Agents, controllers and engineering studies ask many small questions of
explicit state. Kai answers them as typed decisions, a \op{choice},
\op{score} or \op{noul} over options the caller lists, returned as a
calibrated distribution with no generated text. Kai is one model on one
checkpoint line: a multilingual encoder, adapters that bring sensor streams
with their metadata, audio, images and video into it, and a typed-variable
decoder. Options are encoded alone and scored against the evidence by two
cross-attention blocks, so option count, order and question count are not
bounded by one sequence; \op{noul} is label-symmetric by construction,
\op{score} a cumulative-link model, and a large choice is narrowed by
retrieval that keeps the mass it cuts. A program's dependent questions are
typed variables, decoded as masked slots, refined in waves bounded by
dependency depth and projected exactly onto the program's rules. Programs are
versioned DAGs whose verdicts join a deterministic policy on
$\allow < \ask < \deny$, so no model loosens policy, and each run is a hashed
package that replays, diffs, refreshes and says what flips the decision. Kai
trains in pure Rust, bf16 over F32 masters, as local SGD across Metal, CUDA and
ROCm machines, on data classed by license and held behind a contamination
barrier. We report what went wrong: our first stage-A run lost the encoder's
ability to relate two texts, and we give the measurements, the cause and the
fix. Results against Laya and TypeSafe's Jev on a frozen 62-suite harness, on
capabilities they lack by construction, and on speed are written into the
paper by the benchmark that measures them.
\end{abstract}

\clearpage
\tableofcontents
\clearpage

\input{sections/01-introduction}
\input{sections/02-decisions}
\input{sections/03-model}
\input{sections/04-training}
\input{sections/05-findings}
\input{sections/06-authority}
\input{sections/07-programs}
\input{sections/08-evaluation}
\input{sections/09-limits}
\input{sections/10-related}
\input{sections/99-conclusion}

{\small
\bibliographystyle{plain}
\bibliography{references}
}

\appendix
\input{sections/a1-wire}
\input{sections/a2-results}

\end{document}