Head of Machine Learning, Normal Computing · Copenhagen
My work combines AI and theory. On the AI side, I build agents that design, formalize and verify chips. On the theory side, I work on hashing with machine-checked guarantees, fast polynomial evaluation, optimization theory, and the foundations of massive data: similarity search, sketching and high-dimensional geometry.
Embedding tables are used by machine learning systems to work with categorical features. These tables can become exceedingly large in modern recommendation systems, necessitating the development of new methods for fitting them in memory, even during training.
The best previous methods for table compression are so called "post training" quantization schemes such as "product" and "residual" quantization. These methods replace table rows with references to k-means clustered "codewords". Unfortunately, clustering requires prior knowledge of the table to be compressed, which limits the memory savings to inference time and not training time. Hence, recent work, like the QR method, has used random references (linear sketching), which can be computed with hash functions before training. Unfortunately, the compression achieved is inferior to that achieved by post-training quantization.
The new algorithm, CQR, shows how to get the best of two worlds by combining clustering and sketching: First IDs are randomly assigned to a codebook and codewords are trained (end to end) for an epoch. Next, we expand the codebook and apply clustering to reduce the size again. Finally, we add new random references and continue training.
We show experimentally close to those of post-training quantization with the training time memory reductions of sketch-based methods, and we prove that our method always converges to the optimal embedding table for least-squares training.
We formulate and optimally solve a new generalized Set Similarity Search problem, which assumes the size of the database and query sets are known in advance. By creating polylog copies of our data-structure, we optimally solve any symmetric Approximate Set Similarity Search problem, including approximate versions of Subset Search, Maximum Inner Product Search (MIPS), Jaccard Similarity Search and Partial Match.
Our algorithm can be seen as a natural generalization of previous work on Set as well as Euclidean Similarity Search, but conceptually it differs by optimally exploiting the information present in the sets as well as their complements, and doing so asymmetrically between queries and stored sets. Doing so we improve upon the best previous work: MinHash [J. Discrete Algorithms 1998], SimHash [STOC 2002], Spherical LSF [SODA 2016, 2017] and Chosen Path [STOC 2017] by as much as a factor n.14 in both time and space; or in the near-constant time regime, in space, by an arbitrarily large polynomial factor.
Turning the geometric concept, based on Boolean supermajority functions, into a practical algorithm requires ideas from branching random walks on Z2, for which we give the first non-asymptotic near tight analysis.
Our lower bounds follow from new hypercontractive arguments, which can be seen as characterizing the exact family of similarity search problems for which supermajorities are optimal. The optimality holds for among all hashing based data structures in the random setting, and by reductions, for 1 cell and 2 cell probe data structures. As a side effect, we obtain new hypercontractive bounds on the directed noise operator.
Kernel methods are fundamental tools in machine learning that allow detection of non-linear dependencies between data without explicitly constructing feature vectors in high dimensional spaces. A major disadvantage of kernel methods is their poor scalability: primitives such as kernel PCA or kernel ridge regression generally take prohibitively large quadratic space and (at least) quadratic time, as kernel matrices are usually dense. Some methods for speeding up kernel linear algebra are known, but they all invariably take time exponential in either the dimension of the input point set (e.g., fast multipole methods suffer from the curse of dimensionality) or in the degree of the kernel function.
Oblivious sketching has emerged as a powerful approach to speeding up numerical linear algebra over the past decade, but our understanding of oblivious sketching solutions for kernel matrices has remained quite limited, suffering from the aforementioned exponential dependence on input parameters. Our main contribution is a general method for applying sketching solutions developed in numerical linear algebra over the past decade to a tensoring of data points without forming the tensoring explicitly. This leads to the first oblivious sketch for the polynomial kernel with a target dimension that is only polynomially dependent on the degree of the kernel function, as well as the first oblivious sketch for the Gaussian kernel on bounded datasets that does not suffer from an exponential dependence on the dimensionality of input data points.
Recent work has established that power-law spectral conditions on data enable tight convergence bounds for deterministic gradient descent, resolving the conflict between classical exponential bounds and observed power-law learning curves. In this work, we extend this result to the stochastic regime of high-dimensional machine learning. We provide two main contributions: (1) We generalize the power-law spectral theory to Stochastic Gradient Descent (SGD), showing that the same spectral exponents govern stochastic dynamics; (2) For the fundamental case of isotropic Gaussian data, we provide a precise analysis of data shuffling, deriving exact constants that prove Single Shuffle is strictly superior to Flip-Flop and IID sampling. Our results bridge the gap between abstract spectral theory and practical stochastic training choices, offering a unified picture of how data geometry drives optimization speed.
Horner's rule evaluates a monic degree-n polynomial using n−1 multiplications. We show that with rational preprocessing of the coefficients, any such polynomial can be evaluated using only ⌊n/2⌋ + 1 multiplications over fields of characteristic zero or of characteristic p > n. This resolves the multiplication side of a conjecture of Rabin and Winograd (Comm. Pure Appl. Math 1972), who achieved n/2 + 2⌈log2 n⌉ multiplications and conjectured the logarithmic overhead was necessary.
We show that this multiplication count can't be beaten in general, proving that three multiplications do not suffice for degree 6. This strengthens the lower bound of Pan (STOC 1978), who proved a tight bound for general, complex preprocessing.
In characteristic 2, for every n > 1 and every finite field of size at least 2n, we prove that an n-multiplication chain cannot parametrize all value vectors at 2n distinct evaluation points, even with arbitrary preprocessing. We give ⌊n/2⌋ + 1 multiplication schedules over characteristic 2, each with an explicit inverse, for every odd degree n ≤ 25 and conjecture that this is possible for all n.
We also give an injective polynomial construction for universal hashing that uses N multiplications to hash 2N values with a single random key. This improves the best previous construction by Daniel J. Bernstein (cr.yp.to).
The primary goal of Design Verification (DV) is to ensure that a proposed chip design implementation (either in code, or physical form) exactly matches its specification and is free of functional errors in order to avoid costly re-designs. Achieving this often demands extensive manual interpretation, translating the specification document into a formal, testable representation. While AI has made progress in DV, current approaches typically focus on narrow, isolated tasks rather than full end-to-end specification compliance of modern chip designs, failing to capture the complexity of real-world verification. Our method automatically formalizes natural language memory chip specifications, for industry relevant Dynamic Random Access Memory (DRAM) standards, into a formal representation called DRAMPyML that can be used for downstream DV tasks like the generation of SystemVerilog assertions, stimulus, and functional coverage. We also release our benchmarking dataset, DRAMBench, which can be used to evaluate the evolution of model capabilities (and new approaches) at hardware autoformalization.
The classic way of computing a k-universal hash function is to use a random degree-(k−1) polynomial over a prime field ℤp. For a fast computation of the polynomial, the prime p is often chosen as a Mersenne prime p = 2b−1.
In this paper, we show that there are other nice advantages to using Mersenne primes. Our view is that the output of the hash function is a b-bit integer that is uniformly distributed in [2b], except that p (the all 1s value) is missing. Uniform bit strings have many nice properties, such as splitting into substrings which gives us two or more hash functions for the cost of one, while preserving strong theoretical qualities. We call this trick “Two for one” hashing, and we demonstrate it on 4-universal hashing in the classic Count Sketch algorithm for second moment estimation.
We also provide a new fast branch-free code for division and modulus with Mersenne primes. Contrasting our analytic work, this code generalizes to Pseudo-Mersenne primes p = 2b−c for small c, improving upon a classical algorithm of Crandall.
Algorithms
Explicit colliding inputs for komihash, a5hash, MuseAir, t1ha2, HighwayHash and others under random seeds, measured as worst-case collision bits, next to hash functions with proven bounds and their speed.
Read moreAI for Hardware
Over 43 days, AI agents landed 2,968 commits on a fork of CIRCT: an event-driven Verilog simulator, UVM and cocotb support, bounded model checking, equivalence checking and mutation testing. Published on the Normal Computing blog.
Read moreMost of my day-to-day posting happens on Bluesky and Twitter.
Announcement of my election to the Board of Directors of the Silicon Integration Initiative for 2026–2027.
Quoted on why compact model representations generalize better.
Podcast interview on using swarms of AI agents to design and formally verify chips, and on Normal Computing's thermodynamic computing work.
Quoted on training surrogate models versus steering real systems end-to-end with AI.
My write-up of how we used AI agents to build an open-source Verilog simulation and formal verification stack on top of CIRCT in 43 days.
Interview on how our company, Normal Computing, is using AI to improve chip design and development.
I was interviewed by the IT workers union on Google's FLoC system and the use of SimHash.
The announcement of my winning the Stibo Travel grant.
Article about my PyChess chess software.
Coverage of my team's participation in the ICPC World Finals.
Interview with my team after we won the Danish university programming championship against 34 other teams.
Announcement of my win in the Oxford programming competition with a Numberlink puzzle solver.
Video interview about PyChess at the 2009 Trophées du Libre in Soissons, where PyChess won first place in the Hobbies category.
