Mathematics and computation

Random matrix experiments

Large matrices filled with random numbers, diagonalised repeatedly to study the statistics of their eigenvalues.

Question it answers: What pattern do the eigenvalues of a random matrix settle into, and does it match other areas of mathematics and physics?

Leaves out: Only ever samples a tiny corner of an infinite space of possible matrices.

Runs on: about 10¹² FLOPS rough a university cluster generating and diagonalising many large matricesSince: 1955 Wigner's early work on random matrix eigenvalue statistics

Random graph experiments

Graphs generated by a random rule, node by node or edge by edge, to see which properties, such as connectivity or clustering, appear typically.

Question it answers: What does a 'typical' network look like under this rule for adding nodes and edges?

Leaves out: Real-world networks are rarely as clean as the rule that generates the model.

Runs on: about 10¹⁰ FLOPS rough runs on a desktop for graphs up to millions of nodesSince: 1959 Erdos and Renyi's random graph model

Percolation simulation

A lattice or network with sites or bonds opened at random, watched for the point at which a connected path suddenly spans the whole system.

Question it answers: At what density does a random network suddenly become connected end to end?

Leaves out: Idealised lattices behave more cleanly than any real porous material or network.

Runs on: about 10¹⁰ FLOPS rough a desktop machine for large lattice sweepsSince: 1957 Broadbent and Hammersley's introduction of percolation theory

Experimental mathematics searches

Brute-force numerical search for patterns, counterexamples or exact relationships among numbers, run far beyond what could be checked by hand.

Question it answers: Is this conjecture true for every case anyone can afford to check, and does a pattern emerge?

Leaves out: No amount of checked cases is a proof, however many are found to hold.

Runs on: about 10¹¹ FLOPS rough a university cluster running for days on one searchSince: 1963 by 1963, computer searches for integer relations and prime patterns

Monte Carlo estimation of constants

Random sampling used to estimate a mathematical constant or integral, such as scattering points to estimate an area, as an exercise rather than for a physical model.

Question it answers: How accurately can blind random sampling alone pin down an exact mathematical quantity?

Leaves out: Converges far more slowly than almost any more sophisticated numerical method.

Runs on: about 10⁹ FLOPS rough runs on a laptop in seconds to minutesSince: 1946 Ulam’s idea of 1946; von Neumann proposed an electronic-computer version in March 1947, and the method was first published in 1949 sourceIn the simulations tree: Monte Carlo method

Run the interactive model

Computational number theory searches

Large numbers tested for primality, factored, or searched for special properties such as perfect numbers, using algorithms run at scale rather than by hand.

Question it answers: Does this huge number have the property we are looking for, and how far can the search push the record?

Leaves out: Record-breaking searches say little about numbers nobody has thought to check yet.

Runs on: about 10¹³ FLOPS rough a distributed volunteer computing project across many donated machinesSince: 1951 Lucas's hand test for Mersenne primes, first run by computer in 1951

Chaotic-attractor numerics

A small set of nonlinear equations integrated step by step to reveal sensitive dependence on initial conditions and a fractal attractor.

Question it answers: Why does a simple deterministic system become unpredictable?

Leaves out: Numerical rounding means a long trajectory is not a true orbit, only one that stays close to one.

Runs on: about 10³ FLOPS rough a few equations, seconds on a laptop.Since: 1963 Lorenz's deterministic nonperiodic flow, a convection model run on a computer. sourceIn the simulations tree: Lorenz’s chaotic convection

Nonlinear lattice experiments

A chain of masses with nonlinear springs started in one mode and followed to see whether the energy spreads evenly, as thermodynamics would suggest.

Question it answers: Does a nonlinear chain share its energy evenly among all its motions?

Leaves out: Results depend on the chosen chain and initial state.

Runs on: about 10³ FLOPS rough tiny by modern standards; the original used a few dozen masses.Since: 1955 Fermi, Pasta and Ulam's studies of nonlinear problems on an early digital computer. source

Soliton numerical experiments

A nonlinear wave equation solved on a grid to watch pulses pass through each other and keep their shape, which linear waves do not.

Question it answers: Why do some nonlinear waves pass through each other unchanged?

Leaves out: It shows one family of equations, not the general behaviour of nonlinear waves.

Runs on: about 10⁴ FLOPS rough a one-dimensional grid, trivial today.Since: 1965 Zabusky and Kruskal's interaction of solitons in a collisionless plasma and the recurrence of initial states. source

Fractal-set rendering

A simple iterated formula tested at each location in the complex plane to see whether it escapes, drawing the boundary of the set of stable points.

Question it answers: What is the shape of the set where a simple iteration stays bounded?

Leaves out: Escape tests only suggest membership, and the picture is a finite-resolution sampling of an infinitely detailed set.

Runs on: about 10⁹ FLOPS rough deep zooms need extended-precision iteration at millions of points.Since: 1980 Mandelbrot's fractal aspects of the iteration of z to lambda z(1-z), first computer images of the Mandelbrot set. source

Sandpile self-organised criticality

Grains dropped on a grid that topple when too steep, giving avalanches of every size without tuning, as a model of how systems reach a critical state.

Question it answers: Why do avalanches of every size appear without any tuning?

Leaves out: Whether real systems share the same scaling is contested.

Runs on: about 10⁹ FLOPS rough long runs on large grids to see scaling.Since: 1987 Bak, Tang and Wiesenfeld's self-organised criticality: an explanation of 1/f noise. source

Riemann zeta zero computation

The values of the zeta function along its critical line are calculated to locate and count its zeros, checking they lie where the hypothesis says.

Question it answers: Do all the non-trivial zeros of the zeta function lie on one line?

Leaves out: A finite check, however long, cannot prove that no zero off the line exists beyond it.

Runs on: about 10¹⁸ FLOPS rough decades of CPU time at the largest searches.Since: 1953 Turing's calculations of the Riemann zeta function. source

Digits of pi by computer

Series for pi are summed to enormous numbers of digits with exact arithmetic, testing both the number and the machine.

Question it answers: Do the digits of pi look random, and can the machine be trusted at this scale?

Leaves out: The digits do not answer any open question, and checks catch hardware errors only if the method is independent.

Runs on: about 10¹⁷ FLOPS rough months on a server for hundreds of trillions of digits.Since: 1950 Reitwiesner's ENIAC determination of pi and e to more than 2000 decimal places (published 1950, reprinted in Pi: A Source Book). source

AI-guided conjecture discovery

Machine learning on large tables of mathematical objects finds which properties are linked, to suggest a conjecture that mathematicians then try to prove.

Question it answers: Which unseen relationship between these mathematical quantities is worth proving?

Leaves out: It only suggests patterns and proves nothing itself, and some regularities in the data may be artefacts of how the data were made.

Runs on: about 10¹⁵ FLOPS rough days on a few GPUs per dataset.Since: 2021 Davies and colleagues' advancing mathematics by guiding human intuition with AI. source

Learned algorithm and construction search

A game-playing or language-model system searches for new procedures or mathematical objects, with a computer checking each candidate for correctness.

Question it answers: Can a program discover a faster algorithm or a larger example than people have found?

Leaves out: Each result is a single new example, and the search covers only the kinds of objects its designers framed as a game.

Runs on: about 10¹⁷ FLOPS rough days to weeks on accelerator clusters.Since: 2022 Fawzi and colleagues' AlphaTensor, discovering faster matrix multiplication algorithms with reinforcement learning. source

Model checking

Every reachable state of a finite system, such as a protocol or a circuit design, enumerated by computer to check that a property holds in all of them.

Question it answers: Is there any reachable state where this design breaks its own rules?

Leaves out: State spaces explode past what can be checked, so real designs are simplified first.

Runs on: about 10¹² FLOPS rough a university cluster exhausting a large but bounded state spaceSince: 1981 Clarke and Emerson's introduction of model checking

Automated theorem proving search

A search through chains of logical inference, computer-generated step by step, looking for a proof or disproof of a mathematical statement.

Question it answers: Does a valid chain of logical steps exist from the axioms to this statement?

Leaves out: Finds proofs no human would choose, and sometimes none at all within reach.

Runs on: about 10¹¹ FLOPS rough a university cluster searching for hours to daysSince: 1956 the Logic Theorist, an early automated proof search program

SAT and constraint solving

Millions of combinations of true or false values searched systematically to satisfy a large set of logical constraints, used to schedule, route or verify designs.

Question it answers: Is there any assignment of values that satisfies every one of these constraints at once?

Leaves out: Some instances are hard enough that no solver, however good, finishes in time.

Runs on: about 10¹¹ FLOPS rough a workstation to a cluster, depending on problem sizeSince: 1962 the Davis-Putnam procedure for satisfiability search

Cryptographic attack modelling

A code or key-exchange scheme attacked millions of times in simulation, by brute force, statistical bias or a modelled weakness, to measure how much effort breaking it really takes.

Question it answers: How many operations would it actually take to break this, and is that number still safely large?

Leaves out: Only tests the attacks the analyst thought to model, not the one nobody has found yet.

Runs on: about 10¹⁴ FLOPS rough a distributed cluster of many machines running attack trialsSince: 1976 by 1976, computational analysis of cipher and key-exchange strength

Side-channel leakage simulation

The power draw, timing or electromagnetic emission of a device modelled while it runs a cryptographic operation, to see what a listener outside could learn from it.

Question it answers: How much of the secret key leaks out through the physical behaviour of the device, not the maths?

Leaves out: Lab conditions catch cleaner signals than a noisy real device usually gives away.

Runs on: about 10¹⁰ FLOPS rough a workstation modelling one device's power or timing traceSince: 1996 Kocher's demonstration of timing attacks on cryptographic implementations

Security protocol verification

Every message an attacker could send, replay or forge in a communication protocol, enumerated by computer to check whether a secret or an identity can be forced out of it.

Question it answers: Can any sequence of messages trick this protocol into leaking a secret or accepting a fake identity?

Leaves out: Verifies the protocol as specified, not the shortcuts a real implementation takes.

Runs on: about 10¹¹ FLOPS rough a workstation to a cluster checking one protocol's message spaceSince: 1989 the Dolev-Yao model, a foundational basis for protocol verification

Computer-assisted proof by exhaustive case checking

A theorem reduced to a finite list of cases, each verified by program, because no human could check them all.

Question it answers: Can a proof be completed by a machine checking every case?

Leaves out: Trust moves to the program, the hardware and the case-reduction argument.

Runs on: about 10⁹ FLOPS rough about a thousand hours on a mainframe for the original; far less now.Since: 1977 Appel and Haken's proof that every planar map is four-colourable, using computer-checked reducibility. source

Validated numerics

Computations carried out with guaranteed bounds, so a numerical result proves a mathematical statement, such as the existence of a chaotic attractor.

Question it answers: Can a computed answer be proved correct, not just probably accurate?

Leaves out: Bounds can blow up over long times, limiting proofs to short or well-behaved problems.

Runs on: about 10⁹ FLOPS rough interval arithmetic multiplies cost by a modest factor.Since: 2002 Tucker's rigorous ODE solver and Smale's 14th problem, proving the Lorenz attractor exists. source

Turing-machine enumeration

Every small program of a minimal machine run to see which halt and which run forever, to find the longest-running halting one of each size.

Question it answers: How long can a tiny program run before it stops?

Leaves out: Undecidability means some machines can never be classified, no matter how long they run.

Runs on: about 10¹⁵ FLOPS rough billions of machines, with proofs for the non-halting ones.Since: 1965 Lin and Rado's computer studies of Turing-machine problems. source

Statistical model checking

A system with random behaviour simulated many times to estimate with confidence how likely it is to violate a property.

Question it answers: How likely is a random system to break a safety rule?

Leaves out: Statistical runs give a probability with a confidence level, not a proof, and rare failures need importance sampling.

Runs on: about 10⁹ FLOPS rough thousands to millions of sampled executions.Since: 2002 Younes and Simmons's probabilistic verification of discrete event systems using acceptance sampling. source

Fuzz testing

A program is fed huge numbers of random or mutated inputs to find those that make it crash, in effect simulating a hostile or careless world.

Question it answers: What input will make this software fail?

Leaves out: It finds only failures that random inputs reach, and a program can pass for years while hiding a bug behind a rare case.

Runs on: about 10¹⁴ FLOPS rough machine-years of CPU time for a major code base.Since: 1990 Miller, Fredriksen and So's empirical study of the reliability of UNIX utilities. source

Symbolic execution

A program is run with unknown inputs written as symbols, collecting the conditions on each path, then a solver finds values that take each branch.

Question it answers: Which inputs make each path of this program run, and does any reach a bug?

Leaves out: The number of paths grows exponentially with program size, so large ones are covered only in part.

Runs on: about 10¹² FLOPS rough hours of solver time per program, growing steeply with path count.Since: 1976 King's symbolic execution and program testing. source

Abstract interpretation

A program is run on sets of possible values, such as ranges, instead of single values, to prove properties that hold for every input.

Question it answers: Can this program ever divide by zero or overflow, for any input?

Leaves out: Safe approximation raises false alarms, so people must still check each warning.

Runs on: about 10¹¹ FLOPS rough hours on a workstation for a large avionics code base.Since: 1977 Cousot and Cousot's abstract interpretation, a unified lattice model for static analysis of programs. source

Bounded model checking

The behaviour of a design up to a fixed number of steps is written as a logic formula and handed to a satisfiability solver to find any short path to a bug.

Question it answers: Can this circuit or program reach an error state within a given number of steps?

Leaves out: It proves nothing beyond the step bound unless a separate argument shows it is enough.

Runs on: about 10¹³ FLOPS rough hours on a server per property.Since: 1999 Biere, Cimatti, Clarke and Zhu's symbolic model checking without BDDs. source

Property-based random testing

A rule that should always hold is stated, and the computer generates many random cases and shrinks any failure to a small counterexample.

Question it answers: Does this code obey its own specification on a wide range of inputs?

Leaves out: Random cases may never reach a rare condition, and the property written down may not be the one that matters.

Runs on: about 10⁹ FLOPS rough minutes on a laptop for thousands of cases.Since: 2000 Claessen and Hughes' QuickCheck, a lightweight tool for random testing of Haskell programs. source

Neural network verification

Constraint solvers prove that for every input in a region, a neural network's output stays within bounds, instead of testing samples.

Question it answers: Can a small change to an input ever make the network give a wrong answer?

Leaves out: Proofs scale only to small networks, and the set of perturbations that can be checked is narrow.

Runs on: about 10¹³ FLOPS rough hours to days on a server for a small network.Since: 2017 Katz and colleagues' Reluplex, an SMT solver for verifying deep neural networks. source

Computer architecture simulation

A proposed processor's pipeline, caches and branch predictor modelled instruction by instruction, to estimate the speed of a chip before it is built.

Question it answers: How fast would this processor design run real programs, before any silicon is cut?

Leaves out: Simplifies enough of the real chip that final silicon always differs a little from the model.

Runs on: about 10¹¹ FLOPS rough a university cluster running benchmark programs through the modelSince: 1990 by 1990, cycle-accurate processor simulators for architecture research

Distributed systems and consensus simulation

Many computers modelled sending messages to each other with delays, drops and failures, to test whether a distributed algorithm still agrees on the right answer.

Question it answers: Does this algorithm still reach the correct agreement when messages are lost, delayed or nodes crash?

Leaves out: Injected failures are those the designer anticipated, not those that arise unexpectedly in production.

Runs on: about 10¹⁰ FLOPS rough a cluster simulating hundreds of virtual nodesSince: 1978 Lamport's early work on ordering and failure in distributed systems

Storage systems simulation

Disks, drives and file systems modelled for how they lay out data, fail and recover, to test a storage design before real drives are bought and filled.

Question it answers: How does this storage design perform and survive failure, at a scale too expensive to test for real first?

Leaves out: Real drives fail in messier, more correlated ways than the model's random failure rate.

Runs on: about 10¹⁰ FLOPS rough a workstation to a small cluster modelling a storage arraySince: 1988 by 1988, simulation models of disk array reliability

Operating system scheduler simulation

A stream of computing tasks modelled arriving and competing for a processor, run against different scheduling rules to see which one is fairest or fastest.

Question it answers: Which way of ordering the queue of tasks gets the most work done, or is fairest to every task?

Leaves out: Synthetic workloads rarely match the irregular mix of tasks a real machine encounters.

Runs on: about 10⁹ FLOPS rough runs on a laptop or workstation in seconds to minutesSince: 1968 by 1968, simulation studies of processor scheduling policies

Compiler and program optimisation search

Enormous numbers of small variations of a piece of code tried and measured, searching for the fastest or shortest version that still does the same job.

Question it answers: Out of every equivalent way to write this small piece of code, which one is actually fastest?

Leaves out: Programs found are sometimes so unusual that no explanation of why they work is available.

Runs on: about 10¹⁰ FLOPS rough a cluster searching a large space of code variantsSince: 2006 by 2006, superoptimisation search over short instruction sequences

Empirical algorithm performance testing

An algorithm run thousands of times over randomly generated or real-world inputs of increasing size, measuring how its running time actually grows rather than proving it on paper.

Question it answers: How does this algorithm's running time actually grow in practice, on the inputs it will really see?

Leaves out: A worst case absent from the test inputs remains undetected until it occurs.

Runs on: about 10⁹ FLOPS rough runs on a workstation across many generated test inputsSince: 1970 by 1970, systematic empirical testing of algorithm running times

Language-model program execution

A language model writes out step-by-step intermediate states as it traces what a program would compute.

Question it answers: Can a language model emulate running code?

Leaves out: Output is not guaranteed correct, and long programs fail.

Runs on: about 10¹⁴ FLOPS rough Per-query inferenceSince: 2021 Show your work: scratchpads for intermediate computation with language models (2021) source

Blockchain consensus simulation

A network of nodes producing and sharing blocks under delays, to test how block size, timing and attackers affect security and throughput.

Question it answers: How secure and fast is a blockchain under network delay and attack?

Leaves out: Real node behaviour and network topologies are only partly measured.

Runs on: about 10⁸ FLOPS rough event-driven runs of thousands of nodes.Since: 2016 Gervais and colleagues' security and performance analysis of proof-of-work blockchains with a simulator. source

Parallel discrete-event simulation

A simulation of events in time is split across many processors that each advance their own clock and roll back if one arrives late.

Question it answers: How can a huge event-driven simulation, such as a network or battlefield, run fast on many machines?

Leaves out: Rollbacks can cascade, and the speed-up depends heavily on how tightly the events are coupled.

Runs on: about 10¹⁴ FLOPS rough hours on a supercomputer for billions of events.Since: 1985 Jefferson's virtual time, the Time Warp mechanism for optimistic synchronisation. source

Graphics processor architecture simulation

A graphics processor's cores, warps and memory are modelled cycle by cycle, running real programs to evaluate a design before building it.

Question it answers: How would a design change affect the speed of parallel programs on a graphics chip?

Leaves out: Details of real chips are secret or unknown, so the model matches the numbers of existing designs only roughly.

Runs on: about 10¹² FLOPS rough hours to days of host time per second of simulated execution.Since: 2009 Bakhoda and colleagues' analysis of CUDA workloads using a detailed GPU simulator. source

FPGA-accelerated system simulation

A chip design is loaded onto many reconfigurable circuits that run it cycle-exactly at megahertz speeds, simulating whole servers and networks of them.

Question it answers: How will this processor and its cluster behave running real software, before it is made?

Leaves out: It is far slower than the real chip, and a design that does not fit on the circuits cannot be run.

Runs on: about 10¹⁵ FLOPS rough days on a cloud of hundreds of reconfigurable circuits.Since: 2018 Karandikar and colleagues' FireSim, FPGA-accelerated cycle-exact scale-out system simulation in the public cloud. source

Full-system simulation

An entire computer, with processors, memory, disks and network cards, is simulated well enough to boot an unmodified operating system and run its programs.

Question it answers: How does real software behave on a machine that does not yet exist, or can be paused and replayed at will?

Leaves out: Timing is approximated for speed, so it cannot give exact performance, only the functional behaviour.

Runs on: about 10¹¹ FLOPS rough near real time on a server per simulated machine.Since: 2002 Magnusson and colleagues' Simics, a full-system simulation platform. source

Lightweight network emulation

Dozens or hundreds of virtual hosts and switches run real network software on one laptop, linked by emulated cables with set speed and delay.

Question it answers: Will this network control program work on a whole topology before it is deployed?

Leaves out: The host's own processor is shared by all the virtual nodes, so fast links get slowed down.

Runs on: about 10¹⁰ FLOPS rough real time on one workstation.Since: 2010 Lantz, Heller and McKeown's 'A network in a laptop', rapid prototyping for software-defined networks. source

Simulated annealing

A computer cools a model of atoms or a design slowly, accepting worse arrangements sometimes, to find a good solution to a hard optimisation problem.

Question it answers: What is a near-best layout or schedule among astronomically many possibilities?

Leaves out: It gives no guarantee of the best answer, and results depend on the cooling schedule.

Runs on: about 10¹² FLOPS rough hours on a workstation for a chip placement.Since: 1983 Kirkpatrick, Gelatt and Vecchi's optimisation by simulated annealing. source

Approximate Bayesian computation

A simulator is run with many trial parameter values, and those that produce data close to the observed data are kept, giving a picture of which values are plausible.

Question it answers: Which settings of a complicated model could have produced the data we observe?

Leaves out: The result depends on which summaries of the data are used and how close a match must be to count.

Runs on: about 10¹³ FLOPS rough millions of simulator runs on a cluster.Since: 1997 Tavaré and colleagues' inference of coalescence times from DNA sequence data using simulation. source