▲
AI: Safety, Scaling, Interpretability
Machine learning results with formal guarantees
Results about large language models, neural scaling, adversarial robustness, and AI safety — all framed as mathematical theorems with Lean-verified components. Some of these rederive known empirical scaling laws from first principles.
6 papers
machine_learning
Short Draft
Lean
DOI
Architectural Optimizations of the In-Context Gradient-Descent Mechanism
The companion core paper establishes, and machine-checks, a single identity: a transformer's forward pass can implement one gradient-descent step on an implicit least-squares objective (the ICL=GD mechanism).
machine_learning
Short Draft
Lean
DOI
Capacity, Scaling, and Grokking from the In-Context Learning = Gradient Descent Mechanism
The companion core paper establishes, and machine-checks, a single identity: a transformer's forward pass can implement one gradient-descent step on an implicit least-squares objective (the ICL=GD mechanism). This satellite asks what that verified identity forces to be true about *representational capacity and scaling*.
machine_learning
Short Draft
Lean
DOI
Training Dynamics and Inference Guarantees of the In-Context Gradient-Descent Mechanism
The companion core paper establishes, and machine-checks, a single identity: a transformer's forward pass can implement one gradient-descent step on an implicit least-squares objective (the ICL=GD mechanism).
machine_learning
Draft
Lean
DOI
When In-Context Learning Implements Gradient Descent: A Learned Mechanism, Mechanically Verified and Empirically Tested
We turn the gradient-descent account of in-context learning (ICL) into machine-checked mathematics and falsifiable predictions about real transformers. The formal target is the linear-attention regression identity: a forward pass can implement one gradient-descent step on an implicit least-squares objective.
Machine Learning
Draft
DOI
The Knowledge Artifact and Knowledge Algebra of Machine Learning Models
A 200-tree Random Forest has 126,074 parameters. Its knowledge? Three numbers and a basis.
We introduce the **Knowledge Artifact** — a portable representation of what any ML model has learned — and the **Knowledge Algebra** — provably exact arithmetic on these artifacts.
Formal Verification
Draft
Lean
DOI
Conditional Bounds on AI Self-Improvement in an Antitone Threshold Model
We establish conditional bounds in a stylized antitone threshold model of recursive AI self-improvement. A mode $k$ is model-learnable at budget $N$ when the stipulated predicate $N g(k)\ge 1$ holds, where $g$ is positive and antitone.