Functions of one variable are special in numerics: thanks to equioscillation , unary functions can be approximated efficiently by polynomials. For this reason, it can be useful to rewrite functions of multiple variables so that you get large unary fragments. For example, log(exp(a) + exp(b)) can be rewritten to: a + log(1 + exp(b - a)) The fragment log(1 + exp(x)) is a unary function; if we call…
The LLMs have gotten impressively good at certain intellectual activities. And one of the big promises that the AI labs seem to see here is the possibility of accelerating science; Dario talks about this in Machines of Loving Grace and OpenAI has had GPT-5 propose wet lab experiments . This is very cool. I like science! But Opus and Codex are sometimes kind of doofuses. And real science is not…
I guess we are building software factories now. Dunno about that, but we do know how to build factories: the Toyota Production System . Information over Materials Materials flow through a factory: metals become parts become assemblies become cars. Each station can only produce so much. You might try to make each station more efficient, producing more materials in less time; but this is not the…
I do most of my AI coding using Amp . It is an AI "agent", meaning it is composed of two pieces. There's the AI model itself—currently Claude Opus 4.5—which runs on the model provider's servers over an API, and the agent harness, which runs on my machine and allows the AI to run commands, edit files, and so on. The AI model, eh, it crunches numbers. But the agent harness is an…
On the one hand this is the most hyped topic ever so you'd think I have nothing to add. I don't feel that I do. But I'm known as the "AI Coding hype man" in my department and among many friends. They keep asking me how they're supposed to do AI coding. This blog post is an attempt to save time explaining. If you are happy with your AI coding setup, please just skip this blog post. This is an…
CSS is hard. The layout rules are quite complex. Most people don't know the details. Centering a <div> is famously a challenge. Remember the 2000s, when A List Apart would run all sorts of crazy ways to achieve the "Holy Grail" layout—a header, a main body and sidebar of equal heights, and a footer? Should CSS layout—given that it's such a mess—just be thrown out, to start over with a totally…
A number of 70s computing systems had nine-bit bytes, most prominently the PDP-10, but today 1 [ 1 Apparently, it was the System/360 that really set the standard here. ] all systems use 8-bit bytes and that now seems natural. 2 [ 2 Though you still see RFCs use "octet", and the C standard has a CHAR_BITS macro, to handle the possibility of a different-sized byte. ] As a power of two, eight is…
I had a blast at PLDI'25 this year! The best part, of course, was Marisa's talk about Spineless Traversal , but I wanted to take list the other highlights of the event, both for my own memory and for others who share my research taste. My inspiration is Phil Zucker , whose PLDI post is just phenomenal. I think of the papers below as getting a "Distinguished Paper" award from me. EGRAPHS'25 This…
Ok, here's the story so far. Way back when I wanted to test whether sort + FastTwoSum is faster than TwoSum. But as I started optimizing it , I kept getting frustrated with how hard it is to benchmark low-level code, and eventually I wrote a simulator for my CPU, the Apple M1 chip. At this point, I was in too deep and wanted to keep improving the simulator. Compiling to Assembly As of the last…
I just read David's paper on floating-point accumulation networks. It's fantastic work: he's developed a new abstraction of floating-point numbers that allows him to verify error bounds for sequences of TwoSum-like operations, and then used that abstraction to design new, faster double-double addition algorithms. Since I already had a Apple M1 simulator on hand , I figured I'd give his algorithms…
I've been thinking about quantifier elimination, and one thing I have gained a new appreciation for is how much of our ordinary mathematical syntax exists in order to get quantifier elimination for common logics. This page lists a few examples. Modular arithmetic The mod operation, as in x % 3 , is necessary to eliminate existentials like: ∃ x, y = 3 x + 2 Here the quantifier elimination results…
I've recently been on a tear writing about Egraphs modulo T , first writing about polynomials specifically and later about the general case . My main insight is that pattern-matching, specifically relational e-matching, is related to quantifier elimination and the related notion of cell decomposition, which in fact lots of theories have. So I wanted to try to make this explicit in one of the…
One thing Herbie does is simplify stuff, and one that I am personally interested in is simplifying trigonometric expressions. For example, did you know that sin(x) / (1 + cos(x)) and (1 - sin(x)) / cos(x) are the same? Or that both are equal to tan(x / 2) ? But how can we do this automatically? Before I move on, a thank you to ChatGPT, mostly o3 and 4.1, for generative discussions. The Weirstrass…
Phil Zucker has been writing about Egraphs modulo T for a while now; see his latest blog post and latest paper for up to date efforts. I've been thinking about this too, and this post is my attempt to summarize. I'll be referencing Phil's ideas repeatedly, since all of my thoughts trace back to his. What is an E-graph (abstractly) An e-graph is for conjunctive reasoning with equality. Conjunctive…
I have recently become a big fan of the condition number formalism for floating-point error; it is a simple mental model that explains a lot about floating point. In this blog post I want to use that mental model to investigate "operator fusion": basically, why library functions like log1p , cospi , or hypot improve error. 1 [ 1 Actually, one of the big effects of hypot is to avoid overflow, which…
In Herbie we use e-graphs to do algebraic rewriting of mathematical expressions. For example, in the Rust standard library's acosh function , e-graphs rewrite log(sqrt(x^2 + 1)) … into log(1 + sqrt(x^2 + 1) - 1) into log1p(sqrt(x^2 + 1) - 1) into log1p(x^2 / (sqrt(x^2 + 1) + 1)) into log1p(x / (sqrt(1 + (1/x)^2) + (1/x))) , Still, they're bad at some things, and one that really stands out…
In case you can't tell, I've been following a double - double rabbit-hole recently. Those previous two posts were about performance, but this one is about semantics. Specifically, it's about using double-double arithmetic as an oracle for standard double-precision arithmetic, and a specific issue, absorption , that comes up. Double-double oracles I have a dream of "safe" numerical programming,…
In my last post , I pointed out that FastTwoSum plus a sort is actually faster than normal TwoSum on modern hardware, and suggested that TwoSum is therefore obsolete. This post expands the analysis and tests futher optimizations on the Apple M1 chip. General approach The general FastTwoSum algorithm is the following: s = a + b bb = s - a e = b - bb This assumes that |a| > |b| , or perhaps a…
We all know that floating-point arithmetic is imprecise. When you do s = x + y , the value of s might not exactly be the sum of the values of x and y . Curiously (and importantly, for some applications), there's a way to quantify the imprecision: there's a family of algorithms 1 [ 1 Called "error-free transformations", because they transform x and y into s and e without any error in the sum. ]…
ChatGPT o3 (the full version, not the mini version I tested earlier ) came out just over a week ago . I used up my rate limit that day. It is the real deal, and I am blown away. I have been an LLM skeptic for a while. But this semester of paternity leave I decided that learning to use LLMs would be a goal, and I've been trying to use them more and more. And I'll be honest: I get a lot of value out…
I've been practicing using LLMs (mostly OpenAI o3-mini-high ) for coding. It's good at quick prototypes, and I've recently been thinking about fast set membership operations (specifically related to CSS matching ). So I've had it implement a number of different binary search algorithms. The upshot is that modern CPUs are amazingly fast. Here's the fastest version I ended up with: int sSearch ( int…
I have long been interested in CSS selector matching algorithms . In short: existing selector matching algorithms are \(O(d^2)\) at worst, where \(d\) is the tree depth, and there are better algorithms that are \(O(d)\). But of course the constants matter a lot. I previously described both algorithms, and even showed that the bad cases can occur in practice. Recently I dove into the Stylo CSS…
Alright, I'm back at it : comparing Herbie against LLMs to see who is best at numerical rewriting. If you're new here, Herbie is a research compiler I've been working on for about a decade that helps compile mathematical expressions to fast and accurate floating-point code. More recently, I've been comparing new OpenAI models against Herbie to see who is the top numerical analyst. So far, Herbie's…
This proposal suggests a radically different way Herbie could work, making use of high-quality oracle-free methods of evaluating error. This new method would make Herbie simpler, faster, and possibly better, while (I hope) maintaining all the things we currently like about Herbie. This new Herbie would use egg/egglog much more heavily than today, and the greedy improvement loop would be gone.…
This blog post is a design document, laying out how the platforms feature should work and how it should be organized. First—what is the platforms feature? I think it’s useful to separate out two parts: Users should be able to specify a platform when invoking Herbie. Users should also be able to make new platforms. Let’s consider each in turn, but first—a background on platforms. What is a…
Today I found and fixed a Herbie bug. It had been bothering me for months: even when run with the same seed, Herbie's results are not reproducible. They're almost reproducible! They're close! But a few benchmarks, something like 5 or so, would differ from run to run. The bug was so tricky, so bizarre, that I just had to write about it. The bug I'll keep things short. I first tested a number of…
Floating-point code uses various functions on floating-point numbers, like arithmetic and elementary functions. When I got started working on floating-point error, I thought that was the ontology: arithmetic vs elementary. However, I now realize that it's more complex than that: it's useful to distinguish between floating-point operations based on their exactness. Exact operations (Group 0) These…
This post is the third in a series of me trying to work out batches , a new data structure I am testing for Herbie and more generally for programming with recursive data structures. In my first post I laid out a type theory for batches, and in my second post I discussed how we can check that programs that use batches are safe. But I'm still after a "holy grail": how to making programming with…
A year and a half ago, I wrote a blog post comparing Herbie to the first ChatGPT (which we now call, I think, GPT 3.5). I chose 11 floating-point repair benchmarks, and fed all of them to Herbie and ChatGPT. Herbie is a tool my students and I develop to do exactly this work, and I wanted to know if AI tools had obsoleted it. The conclusion was that Herbie was still much better, winning 6/11 and…
Last time , I talked about batches, my term for an arena-allocated, flattened form of an AST, which I think is going to be a key data structure in Herbie. That post covered basics and sketched out a type theory; in this post I want to dive deeper into computating with batches. Batch Refresher & Index Safety Here's just a quick review from last time. A batch stores a recursive data structure like…
Most of Herbie is spent thinking about expressions: generating them, evaluating them, mutating them, analyzing them, filtering them, and so on. So naturally this has to be as fast as possible. Herbie is a primarily mutational synthesis engine—most expressions it thinks about are generated by changing, in small ways, another expression—so most of its expressions are very similar and…
The Herbie Project has grown and grown over the last—gosh—decade, and in 2024 we now have something like 15 people working on it, including myself and Zach and all of our students PhD, MS, and undergraduate. So for this semester I've chosen to focus my efforts a bit narrower than normal and worked with Zane and Artem on making Herbie faster. It's been a super-productive few months, with Artem and…
I previously posted asking what the algorithmic complexity of selector matching is. I've learned a lot about browsers in the two years since, so this post contains an answer and also further thoughts. Quadratic Selector Matching Selector matching is quadratic when you have \(O(n)\) elements which each need to walk up the node tree \(O(n)\) steps to test whether a selector matches. There are a lot…
Note This is guest post by my student Artem Yadrov, who has been working on the Herbie Core. I recently tried to switch Herbie ’s interval representation from our Rival library to the more-common Arb library. I initially assumed that, with Arb, Herbie would be faster and no less accurate, but it didn’t turn out that way, and we’ve now decided that Herbie will stick with Rival. This blog explains…
In MemBalancer , my student Marisa and I came up with a novel correctness property for garbage collection heap limits, which we called "compositionality", derived compositional heap limits for a basic one-generation garbage collector, and showed that this new heap limit lead to big reductions in memory usage for Chrome's V8 JavaScript runtime. But actually V8 uses a generational GC, and…
I was recently talking to Hans Boehm about floating point rounding modes. They are a mess, aren't they? It's a piece of global application state that very subtly changes the meaning of every floating-point operation in the whole program. It causes bugs in compilers, confusion for programmers, and all sorts of pain for library developers. So what would be better? Can we get rid of rounding modes?…
In research it's common to compare your solution to some simple approach as a baseline, to prove that whatever complex algorithm you've developed is actually worth using. Sometimes, coming up with this baseline is hard. But now we have ChatGPT, so let's plug a hole in my 2015 research paper on floating-point error improvement by comparing my tool, Herbie, with ChatGPT. Methodology I've chosen a…
Now that I have advised a few research projects, I've begun to notice similarities, common errors, and inflection points. For the benefit of my students, here's a quick summary of how I approach projects. Naturally, this is specific to my research, and might not apply to any other advisor. Projects I divide my students' research into "projects". Usually a project begins with some vague idea, like…
This semester, I am teaching Compilers , and I'm quite happy with how I covered parsing this year. Specifically, I taught students to build a top-down LR parser and it seemed to go relatively well. Update : Laurence asks me to note that he's not as much of a parser theorist as this post makes him out to be. Update : There's an ongoing discussion on Hacker News about this post. I learned a lot from…
About two years ago, I wrote about some ideas for using a typed DSL for implementing math libraries. I wanted to give a bit of a status update on that project: MegaLibm. All the work described here was done by the extremely talented Ian Briggs —if you're looking to hire a verification and optimization wizard, email me . Not everything described below currently works, but it's all pretty close. We…
Last week I had a fun experience using Herbie to actually improve the numerical accuracy of real code. Discovering a Rust problem It all started when Finn (an undergraduate from UW) submitted a PR to FPBench to compile FPBench benchmarks to Rust. Besides being great work and a valuable contribution, he also pointed out that our test framework was failing on his FPBench to Rust compiler "due to…
I've been thinking recently about the differences between affine arithmetic and error Taylor series . In both, an expression is represented as 1) the answer, plus 2) a number of error terms. But in my experience, tools based on affine arithmetic are less precise than those based on error Taylor series. What gives? And how are the two analyses related? In affine arithmetic, the true answer is…
Earlier today, I merged one of the biggest improvements to Herbie ever. Let me take a moment to celebrate. Why cost-accuracy trade-offs? About a year ago, the Herbie team, lead by Brett and Oliver , published Combining Precision Tuning and Rewriting at ARITH'21. While ostensibly that paper was about incorporating precision tuning into Herbie, in reality it was about slightly more than that—it was…
I've been tackling a lot of old issues in Herbie this summer, and in the process I found out that Herbie's pruning algorithm is incredibly slow. This is the story of how I sped it up, demonstrating both some good optimization tricks and also some nice tooling that we've built in Herbie. The Backstory Pruning is an essential part of Herbie. At a high level, Herbie has three phases: first, it…
Skia is a fast and widely used 2D graphics library for tasks like rasterization. it's used in Google Chrome and Android, so speeding it up would have large impacts, and I think e-graphs have a lot of potential to drive an interesting research project in that direction. A bit of Skia background I don't know much about Skia, but I learned a lot from Chris Harrelson helping him edit a chapter about…
CSS selectors are part of the CSS language used for styling web pages on the web. CSS stylesheets are made up of rules, where each rule has a selector that defines which elements on the page the rule applies to. When the browser loads a stylesheet, it needs to match those selectors to the elements on the page, to determine which rules apply to which element. Here's my question: what is the…
Error models play a central role in automated numerical analysis. Basically, when you have a floating-point operation x + y , it is usually easier to analyze it in terms of non-deterministic real operations. Epsilon and Delta The most common error model is that an operation x * y (taking * to be addition, subtraction, multiplication, or division, and sometimes square root or fused multiply-add)…
E-graphs are good . They are a powerful, general-purpose mechanism for representing sets of programs and reasoning about those sets of programs via equational rules. My colleagues at the University of Washington who work on the Egg library have been developing a "cookbook" of techniques for common subexpression elimination, synthesis, constant folding, and binding in e-graphs. This post is a new…
As part of Ian and my work on synthesizing math libraries , I've been thinking about synthesizing range reductions. I think we've found a beautiful and efficient way to do this tricky bit of synthesis using e-graphs . This idea is also related to recent Herbie work on detecting symmetric expressions . What is range reduction The core of modern library function implementation is the Remez algorithm…
As maintainer of Racket's math library , I sometimes put my numerical methods knowledge to a practical test. For example, a few days ago, I took a look at Racket's quadratic-solutions function, which returns the roots of a quadratic formula. Humorously, I've used the quadratic formula as an example in dozens of talks and in the Herbie paper . Yet it was more complex than I expected! The quadratic…