papers/zen/zen4-max_whitepaper.tex

\documentclass[11pt,a4paper]{article}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{amsmath,amsfonts,amssymb}
\usepackage{graphicx}
\usepackage{hyperref}
\usepackage{listings}
\usepackage[dvipsnames]{xcolor}
\usepackage{booktabs}
\usepackage{float}
\usepackage{geometry}
\geometry{margin=1in}

\definecolor{zenblue}{RGB}{41,121,255}
\definecolor{zengreen}{RGB}{52,199,89}
\definecolor{zenorange}{RGB}{255,149,0}
\definecolor{codegray}{RGB}{245,245,245}

\hypersetup{
    colorlinks=true,
    linkcolor=zenblue,
    urlcolor=zenblue,
    citecolor=zenblue
}

\lstset{
    backgroundcolor=\color{codegray},
    basicstyle=\ttfamily\small,
    breaklines=true,
    captionpos=b,
    frame=single,
    numbers=left,
    numberstyle=\tiny\color{gray}
}

\title{
    \vspace{-2cm}
    \Large \textbf{Zen AI Model Family} \\
    \vspace{0.5cm}
    \Huge \textbf{Zen4-Max} \\
    \vspace{0.3cm}
    \large Fourth-Generation High-Performance Research Model \\
    \vspace{0.5cm}
    \normalsize Technical Whitepaper v2026.01
}

\author{
    Zach Kelling\thanks{[email protected]} \\
    \texttt{[email protected]} \\
    \\
    Zoo Labs Foundation \\
    \texttt{[email protected]}
}

\date{January 2026}

\begin{document}

\maketitle

\begin{abstract}
We present \textbf{Zen4-Max}, a 480B total parameter Mixture-of-Distilled-Experts model
activating 48B parameters per token, optimized for research-grade scientific reasoning,
mathematical proof verification, and complex long-horizon analysis. Zen4-Max achieves
93.4\% on MMLU, 90.1\% on MATH, 79.8\% on GPQA Diamond, 94.7\% on HumanEval, and
61.2\% on FrontierMath, establishing it as the highest-performing model for formal
reasoning tasks at the 48B active parameter inference cost. Through a novel
\textbf{Proof-Augmented Training} (PAT) methodology that incorporates formal verification
signals into the pretraining and post-training pipeline, Zen4-Max demonstrates qualitatively
superior performance on tasks requiring logical completeness and self-consistency.
\end{abstract}

\tableofcontents
\newpage

\section{Introduction}

Scientific progress increasingly depends on AI systems capable of reliably assisting
with tasks that require sustained, logically consistent reasoning: deriving mathematical
proofs, designing experiments, interpreting empirical results, and synthesizing findings
across hundreds of papers. These tasks share a common requirement that distinguishes them
from most benchmarks: correctness cannot be approximated by fluency. A mathematical proof
is either valid or it is not; a synthesized research hypothesis is either consistent with
its supporting evidence or it contradicts it.

Zen4-Max is designed for this regime. Its primary architectural innovation, Proof-Augmented
Training, introduces formal verification signals into both the pretraining corpus and the
post-training reward function, teaching the model to distinguish correct chains of reasoning
from plausible-but-incorrect ones. The result is measurable improvement on FrontierMath
(61.2\%), competition-level mathematics benchmarks, and scientific reasoning tasks that
require multi-step argument validation.

Positioned between Zen4-Pro (72B dense) and Zen4-Ultra (1T MoE), Zen4-Max provides a
practical inference cost (48B active parameters, achievable on 4 H100s) while approaching
the capability ceiling of the Zen4 family on reasoning-intensive tasks.

\subsection{Key Contributions}

\begin{itemize}
    \item \textbf{Proof-Augmented Training (PAT)}: A training methodology incorporating
    formal verification signals (lean4, isabelle, and symbolic computation results) into
    the pretraining corpus and using verifier outputs as post-training rewards.
    \item \textbf{480B/48B MoDE}: 480B total parameter MoE with 48B active, using 64 experts
    per layer with top-6 routing, optimized for research-domain specialization.
    \item \textbf{FrontierMath Performance}: 61.2\% on FrontierMath, representing a significant
    advance on research-mathematics benchmarks that are resistant to pattern matching.
    \item \textbf{Long-Horizon Coherence}: Maintained logical consistency over outputs
    exceeding 8,000 tokens, enabling full proof derivations and experimental design documents.
\end{itemize}

\section{Architecture}

\subsection{Model Specifications}

\begin{table}[H]
\centering
\begin{tabular}{ll}
\toprule
\textbf{Component} & \textbf{Specification} \\
\midrule
Total Parameters          & 480B \\
Active Parameters         & 48B per token \\
Architecture              & Zen MoDE (Mixture of Distilled Experts) \\
Number of Layers          & 80 \\
Dense Base Layers         & 24 \\
MoE Upper Layers          & 56 \\
Attention Mechanism       & Hierarchical Hybrid Attention (HHA) \\
Local Window Size         & 16,384 tokens \\
Global Anchor Tokens      & 2,048 per layer \\
Context Length            & 131,072 tokens (128K) \\
Hidden Dimension          & 7,168 \\
Experts per MoE Layer     & 64 \\
Active Experts per Token  & 6 (top-6 routing) \\
Expert Intermediate Dim   & 2,816 \\
Attention Heads           & 56 \\
Key-Value Heads           & 8 (GQA) \\
Vocabulary Size           & 151,936 \\
Positional Encoding       & RoPE ($\theta = 10{,}000{,}000$) \\
Normalization             & RMSNorm \\
Activation                & SwiGLU \\
\bottomrule
\end{tabular}
\caption{Zen4-Max Architecture Specifications}
\end{table}

\subsection{Expert Specialization for Research Domains}

Zen4-Max uses 64 experts per MoE layer organized into four research-domain clusters:

\begin{table}[H]
\centering
\begin{tabular}{lcc}
\toprule
\textbf{Expert Cluster} & \textbf{Count} & \textbf{Primary Data Sources} \\
\midrule
Mathematics and formal proof    & 16 & ArXiv math, Lean4 libraries, OEIS \\
Physical sciences               & 14 & ArXiv physics, NIST databases \\
Life sciences and chemistry     & 12 & PubMed, ChEMBL, protein databases \\
Computer science and systems    & 14 & ArXiv CS, GitHub, formal specs \\
General reasoning               & 8  & All domains \\
\midrule
\textbf{Total}                  & 64 & --- \\
\bottomrule
\end{tabular}
\caption{Zen4-Max Expert Cluster Configuration}
\end{table}

Top-6 routing across 64 experts activates 9.4\% of expert parameters per token.
The routing mechanism uses a sigmoid-normalized gating function rather than softmax,
which reduces routing sensitivity to outlier logit values and improves stability
on long contexts where token distributions shift significantly.

\subsection{Proof-Augmented Training Architecture}

PAT operates at two levels: the pretraining corpus and the post-training reward function.

\subsubsection{Corpus-Level PAT}

The pretraining corpus includes formal proof corpora that provide ground-truth logical
structures:

\begin{itemize}
    \item Mathlib4 (Lean4): 250,000+ theorems with complete formal proofs.
    \item Isabelle Archive of Formal Proofs: 720+ theory developments.
    \item HOL Light standard library: 12,000+ theorems.
    \item Symbolic computation results from SymPy and Mathematica (open datasets).
\end{itemize}

These corpora are presented in a unified format that interleaves the formal statement,
the tactic proof steps, and the verified status of each step. The model learns to
distinguish verified from unverified reasoning by observing this structure.

\subsubsection{Reward-Level PAT}

During post-training, mathematical generation tasks use a hybrid reward:

\begin{equation}
R_{\text{PAT}} = \alpha \cdot R_{\text{outcome}} + \beta \cdot R_{\text{verify}} + \gamma \cdot R_{\text{style}}
\end{equation}

where $R_{\text{outcome}}$ is the binary correctness of the final answer, $R_{\text{verify}}$
is the output of a learned step-level verification model that scores each reasoning step's
logical validity, and $R_{\text{style}}$ penalizes informal hedging language in mathematical
contexts (phrases like ``approximately'' or ``should be'' in proof steps). Empirically,
$\alpha = 0.6, \beta = 0.3, \gamma = 0.1$ produces optimal FrontierMath performance.

\section{Training}

\subsection{Pretraining Data}

\begin{table}[H]
\centering
\begin{tabular}{lcc}
\toprule
\textbf{Data Category} & \textbf{Proportion} & \textbf{Tokens} \\
\midrule
Web (quality-filtered)          & 30\%  & 7.5T \\
Code and formal specifications  & 25\%  & 6.25T \\
Scientific literature (ArXiv)   & 20\%  & 5.0T \\
Mathematical content            & 12\%  & 3.0T \\
Formal proofs (Lean4, Isabelle) & 5\%   & 1.25T \\
Tool-call trajectories          & 5\%   & 1.25T \\
Books and long-form prose       & 3\%   & 0.75T \\
\midrule
\textbf{Total}                  & 100\% & 25.0T \\
\bottomrule
\end{tabular}
\caption{Zen4-Max Pretraining Data Composition (25T tokens)}
\end{table}

Formal proof data (5\%) is over-represented relative to its natural occurrence in the web
corpus by approximately 50$\times$. This over-representation is critical for PAT: without
sufficient formal proof exposure, the verification reward signal cannot be internalized.

\subsection{Training Infrastructure}

\begin{table}[H]
\centering
\begin{tabular}{ll}
\toprule
\textbf{Parameter} & \textbf{Value} \\
\midrule
Hardware               & 8,192 $\times$ H100 80GB SXM \\
Expert Parallelism     & 64 (one expert per device) \\
Tensor Parallelism     & TP=4 \\
Pipeline Parallelism   & PP=10 \\
Data Parallelism       & DP=32 \\
Global Batch Size      & 12M tokens \\
Peak Learning Rate     & $1 \times 10^{-4}$ \\
LR Schedule            & Cosine with warmup (2500 steps) \\
Optimizer              & AdamW ($\beta_1=0.9, \beta_2=0.95$) \\
Training Duration      & 52 days \\
\bottomrule
\end{tabular}
\caption{Zen4-Max Training Infrastructure}
\end{table}

\subsection{Post-Training Stages}

\begin{enumerate}
    \item \textbf{SFT} (5M pairs): Heavy emphasis on mathematical derivation and
    scientific analysis tasks. Includes 200K formal proof demonstrations in natural
    language augmented with lean4 verification certificates.
    \item \textbf{PAT-GRPO}: Proof-Augmented GRPO over 80K mathematics tasks with
    SymPy-verified answers. $G=16$ rollouts per task; the step-level verifier provides
    intermediate rewards at each reasoning step.
    \item \textbf{DPO}: 900K comparison pairs, weighted 3:1 toward research tasks.
    \item \textbf{Safety Alignment}: Standard constitutional AI pass.
\end{enumerate}

\section{Evaluation}

\subsection{Standard Benchmarks}

\begin{table}[H]
\centering
\begin{tabular}{lcccc}
\toprule
\textbf{Benchmark} & \textbf{Zen3-Max} & \textbf{Zen4-Pro} & \textbf{Zen4-Max} & \textbf{$\Delta$ vs Zen3} \\
\midrule
MMLU (5-shot)         & 87.3\% & 91.8\% & 93.4\% & +6.1\% \\
MATH (4-shot)         & 84.6\% & 87.6\% & 90.1\% & +5.5\% \\
HumanEval (0-shot)    & 89.7\% & 93.2\% & 94.7\% & +5.0\% \\
GPQA Diamond          & 72.1\% & 74.3\% & 79.8\% & +7.7\% \\
IFEval                & 84.3\% & 88.4\% & 89.1\% & +4.8\% \\
BBH (3-shot)          & 84.9\% & 89.7\% & 91.4\% & +6.5\% \\
\bottomrule
\end{tabular}
\caption{Standard Benchmark Results: Zen4-Max vs. Prior Art}
\end{table}

\subsection{Research and Formal Reasoning}

\begin{table}[H]
\centering
\begin{tabular}{lcc}
\toprule
\textbf{Benchmark} & \textbf{Zen3-Max} & \textbf{Zen4-Max} \\
\midrule
FrontierMath (overall)        & 48.3\% & 61.2\% \\
FrontierMath (Level 1)        & 71.4\% & 82.7\% \\
FrontierMath (Level 2)        & 45.8\% & 59.3\% \\
FrontierMath (Level 3)        & 27.7\% & 41.6\% \\
AIME 2024 (avg 2 sets)        & 71.3\% & 81.4\% \\
OlympiadBench                 & 59.2\% & 68.7\% \\
ProofWriter (deductive)       & 83.4\% & 91.2\% \\
FOLIO (first-order logic)     & 79.8\% & 87.6\% \\
\bottomrule
\end{tabular}
\caption{Research and Formal Reasoning Benchmarks}
\end{table}

\subsection{Scientific Domain Evaluation}

\begin{table}[H]
\centering
\begin{tabular}{lcc}
\toprule
\textbf{Domain Benchmark} & \textbf{Metric} & \textbf{Zen4-Max} \\
\midrule
GPQA Diamond (physics)     & Accuracy & 81.3\% \\
GPQA Diamond (chemistry)   & Accuracy & 78.4\% \\
GPQA Diamond (biology)     & Accuracy & 79.7\% \\
SciBench (university-level)& Accuracy & 86.2\% \\
MedQA USMLE (4-opt)        & Accuracy & 88.7\% \\
ClimateBench               & Accuracy & 74.3\% \\
\bottomrule
\end{tabular}
\caption{Scientific Domain Evaluation}
\end{table}

\subsection{Long-Output Coherence}

A key capability for research assistance is maintaining logical consistency across
long generated outputs. We evaluate this using a custom \textbf{Proof Coherence Score}
that measures the rate at which self-contained mathematical arguments in long outputs
are free of logical contradictions, verified by a symbolic checker.

\begin{table}[H]
\centering
\begin{tabular}{lccc}
\toprule
\textbf{Output Length} & \textbf{Zen4-Pro} & \textbf{Zen4-Max} & \textbf{Zen4-Thinking} \\
\midrule
1K tokens              & 94.1\% & 96.8\% & 97.3\% \\
4K tokens              & 87.3\% & 92.4\% & 95.1\% \\
8K tokens              & 74.2\% & 86.7\% & 91.8\% \\
16K tokens             & 61.8\% & 78.3\% & 85.4\% \\
\bottomrule
\end{tabular}
\caption{Proof Coherence Score by Output Length}
\end{table}

\section{Related Work}

FrontierMath \cite{glazer2024frontiermath} provides a benchmark of research-mathematics
problems designed to be resistant to pattern matching and memorization, representing a
meaningful signal of genuine mathematical reasoning capability. Prior published scores on
this benchmark range from single digits for standard instruction-tuned models to the
mid-50s for extended-thinking models; Zen4-Max's 61.2\% represents the current best result
in our evaluation.

Formal verification integration into language model training has been explored in the
context of Lean-based theorem provers \cite{polu2022formal} and RLHF with verifier reward
models \cite{lightman2023let}. PAT extends this by incorporating verification signals at
the pretraining stage, not only during post-training, which we find is critical for
deep internalization of proof structure.

Expert specialization in MoE models through domain-partitioned data mixtures was explored
in prior work on mixture-of-experts for multilingual models \cite{artetxe2021efficient}.
Zen4-Max applies this principle to scientific domains with more granular expert routing.

\section{Deployment}

\subsection{Hardware Requirements}

\begin{table}[H]
\centering
\begin{tabular}{llll}
\toprule
\textbf{Format} & \textbf{VRAM} & \textbf{Context} & \textbf{Hardware} \\
\midrule
FP8              & 4$\times$ H100 80GB & 128K & Recommended \\
FP8              & 2$\times$ H100 80GB & 64K  & Reduced context \\
INT4 (AWQ)       & 4$\times$ A100 80GB & 32K  & Budget option \\
INT4 (AWQ)       & 2$\times$ A100 80GB & 16K  & Minimal config \\
\bottomrule
\end{tabular}
\caption{Zen4-Max Deployment Configurations}
\end{table}

\subsection{Research Workflow Integration}

\begin{lstlisting}[language=Python, caption=Zen4-Max for Mathematical Proof Assistance]
from hanzo import HanzoAI

client = HanzoAI()

system_prompt = """You are a mathematical research assistant.
When proving theorems, proceed step by step.
Each step should follow logically from prior steps or stated axioms.
Flag any step requiring an unproved assumption.
"""

response = client.chat.completions.create(
    model="zen4-max",
    messages=[
        {"role": "system", "content": system_prompt},
        {"role": "user", "content": "Prove that sqrt(2) is irrational."}
    ],
    max_tokens=4096,
    temperature=0.0,       # deterministic for proof generation
)
\end{lstlisting}

\section{Safety and Alignment}

\begin{table}[H]
\centering
\begin{tabular}{lcc}
\toprule
\textbf{Metric} & \textbf{Zen3-Max} & \textbf{Zen4-Max} \\
\midrule
Harmful content refusal       & 96.1\% & 98.4\% \\
Over-refusal rate             & 5.3\%  & 3.1\%  \\
Jailbreak resistance          & 94.8\% & 97.9\% \\
TruthfulQA                    & 76.8\% & 84.7\% \\
Scientific claim accuracy     & 83.4\% & 89.2\% \\
\bottomrule
\end{tabular}
\caption{Safety and Alignment Metrics}
\end{table}

Scientific claim accuracy measures the rate at which the model's scientific assertions
match peer-reviewed consensus, evaluated by domain experts on 500 sampled claims per
scientific domain. The improvement from 83.4\% to 89.2\% reflects the increased
scientific literature proportion in pretraining and the PAT reward signal penalizing
unsupported assertions.

\subsection{Limitations}

\begin{itemize}
    \item FrontierMath performance (61.2\%) indicates significant headroom on research-level
    mathematics; Zen4-Thinking is recommended for tasks where extended reasoning budget
    is more important than knowledge breadth.
    \item Formal proof output is not guaranteed to be machine-verifiable without post-processing;
    the model learns proof style from Lean4 but does not run a lean4 kernel during inference.
    \item Expert routing is non-deterministic across batch sizes; results may vary slightly
    when comparing single-item and batched inference.
\end{itemize}

\section{Conclusion}

Zen4-Max establishes the highest standard for research-grade AI assistance at a practical
inference cost. Through Proof-Augmented Training, it internalizes formal reasoning
structure during pretraining rather than only imitating it during fine-tuning. The 480B/48B
Zen MoDE architecture concentrates domain expertise in research clusters that are
selectively activated by the routing mechanism for each token. With 90.1\% on MATH,
79.8\% on GPQA Diamond, and 61.2\% on FrontierMath, Zen4-Max is the recommended choice
for research institutions, quantitative finance, pharmaceutical discovery, and any
application where logical completeness and scientific accuracy are primary requirements.

\section*{Acknowledgments}

We thank the formal methods research community whose open Lean4 and Isabelle corpora
made Proof-Augmented Training possible, the Zoo Labs Foundation science team for
domain evaluation design, and the Hanzo AI infrastructure team for the training cluster.

\bibliographystyle{plain}
\bibliography{references}

\appendix

\section{Model Card}

\begin{table}[H]
\centering
\begin{tabular}{ll}
\toprule
\textbf{Field} & \textbf{Value} \\
\midrule
Model Name       & Zen4-Max \\
Version          & v2026.01 \\
Release Date     & January 2026 \\
Total Parameters & 480B \\
Active Parameters& 48B per token \\
Context Length   & 131,072 tokens \\
License          & Apache 2.0 (weights) \\
Repository       & \href{https://huggingface.co/zenlm/zen4-max}{huggingface.co/zenlm/zen4-max} \\
Documentation    & \href{https://papers.zenlm.org/zen4-max}{papers.zenlm.org/zen4-max} \\
Contact          & [email protected] \\
\bottomrule
\end{tabular}
\caption{Zen4-Max Model Card}
\end{table}

\section{PAT Ablation Study}

\begin{table}[H]
\centering
\begin{tabular}{lccc}
\toprule
\textbf{Training Configuration} & \textbf{MATH} & \textbf{FrontierMath} & \textbf{GPQA} \\
\midrule
Base (no PAT)                   & 85.3\% & 48.1\% & 74.8\% \\
+ Formal corpus (pretraining)   & 87.4\% & 53.6\% & 76.3\% \\
+ Step-level reward (GRPO)      & 89.1\% & 58.4\% & 78.7\% \\
+ Style penalty ($\gamma$ term) & 90.1\% & 61.2\% & 79.8\% \\
\bottomrule
\end{tabular}
\caption{PAT Ablation: Contribution of Each Component}
\end{table}

Each PAT component contributes incrementally. The formal corpus provides the largest
gain on FrontierMath (5.5 points), while the step-level reward provides the largest
gain on MATH (1.7 points, where intermediate step quality is most important).
The style penalty provides a smaller but consistent benefit across all three benchmarks.

\end{document}