ML surrogates matching high-fidelity CFD/physics solvers at a fraction of the cost

A systematic review found 79% (60/76) of ML-for-fluid-PDE papers claiming to beat numerical methods used weak baselines, and reporting biases are widespread. Benchmarks such as ML4CFD score physical fidelity and OOD generalization separately because surrogates that look accurate on average still break conservation laws or fail on unseen geometries. Industry still validates final designs with full CFD.

Source: nature.com

import Mathlib.Data.Real.Basic
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Algebra.Order.Field.Power
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Positivity

/-!
# ML surrogates matching high-fidelity CFD solvers at a fraction of the cost

Concrete here: the **error and speedup metrics**. The held-out set is a finite
family of cases indexed by `Fin n`. For each case the reference solver supplies
an integrated coefficient (e.g. drag) and a sampled field; the surrogate is a
function from the case to the same shapes. Mean absolute relative coefficient
error and mean relative field L2 error are defined explicitly here, as is the
wall-clock speedup ratio, so the acceptance test is arithmetic over the numbers
in the evidence record — not an oracle call.

Opaque oracle (`HeldOut`): the geometries themselves and the reference values,
which come from a converged high-fidelity solver run (AirfRANS- or
DrivAerNet-style), the mesh-convergence claim behind them, the sealed
train/test split, and the two measured wall-clock times on declared hardware.

Who must attest: the benchmark host, publishing the split, the solver settings
and convergence evidence, the reference coefficients and field samples, and both
timings measured on the same declared hardware; plus the statement that the
surrogate's weights were frozen before the held-out geometries were released.

Units: coefficients and relative errors are dimensionless; field samples are in
the field's own units and enter only through a ratio; times in seconds per case.
Denominators are guarded: relative errors require a nonzero reference scale.

Checked with Lean 4.33.0 / Mathlib using:
  lake env lean <absolute-path-to-this-file>
-/

namespace OpenSpur.Problems.CfdSurrogate

/-- Reference data for one held-out case: an integrated coefficient, a sampled
field, and the reference field's L2 norm used as the error denominator. -/
structure Reference (m : ℕ) where
  coefficient : ℝ
  field : Fin m → ℝ
  /-- L2 norm of `field`; the attestation includes it, positivity required. -/
  fieldNorm : ℝ

/-- A surrogate prediction for one case. -/
structure Prediction (m : ℕ) where
  coefficient : ℝ
  field : Fin m → ℝ

/-- The sealed held-out set plus the two timings, all oracle-supplied. -/
structure HeldOut (n m : ℕ) where
  reference : Fin n → Reference m
  /-- Mean solver wall-clock seconds per case. -/
  solverSeconds : ℝ
  /-- Mean surrogate wall-clock seconds per case, same hardware. -/
  surrogateSeconds : ℝ
  splitSealedBeforeSubmission : Prop
  solverMeshConverged : Prop

/-- Absolute relative error of the coefficient on one case. -/
noncomputable def coeffRelError {m : ℕ} (r : Reference m) (p : Prediction m) : ℝ :=
  |p.coefficient - r.coefficient| / |r.coefficient|

/-- Relative L2 field error on one case: ‖p - r‖₂ / ‖r‖₂, with the numerator
written as a squared-sum comparison to avoid a square root. -/
def fieldRelErrorSqBound {m : ℕ} (r : Reference m) (p : Prediction m) (τ : ℝ) : Prop :=
  (∑ j, (p.field j - r.field j) ^ 2) ≤ τ ^ 2 * r.fieldNorm ^ 2

/-- Mean absolute relative coefficient error over the held-out set. -/
noncomputable def meanCoeffRelError {n m : ℕ} (H : HeldOut n m) (S : Fin n → Prediction m) : ℝ :=
  (∑ i, coeffRelError (H.reference i) (S i)) / (n : ℝ)

/-- Wall-clock speedup of the surrogate over the solver. -/
noncomputable def speedup {n m : ℕ} (H : HeldOut n m) : ℝ :=
  H.solverSeconds / H.surrogateSeconds

/-- Accuracy and cost bars. -/
structure Thresholds where
  /-- Mean relative coefficient error allowed, e.g. 0.05. -/
  maxMeanCoeffError : ℝ
  /-- Per-case relative field L2 error allowed, e.g. 0.10. -/
  maxFieldError : ℝ
  /-- Minimum wall-clock speedup, e.g. 100. -/
  minSpeedup : ℝ

/-- Acceptance predicate over a sealed held-out set. -/
def Solved {n m : ℕ} (T : Thresholds) (H : HeldOut n m)
    (S : Fin n → Prediction m) : Prop :=
  H.splitSealedBeforeSubmission ∧
  H.solverMeshConverged ∧
  0 < H.surrogateSeconds ∧
  (∀ i, 0 < (H.reference i).fieldNorm) ∧
  meanCoeffRelError H S ≤ T.maxMeanCoeffError ∧
  (∀ i, fieldRelErrorSqBound (H.reference i) (S i) T.maxFieldError) ∧
  T.minSpeedup ≤ speedup H

/-- Rung `k` halves both error bars and doubles the required speedup. -/
noncomputable def Rung (k : ℕ) : Thresholds where
  maxMeanCoeffError := 0.05 / (2 : ℝ) ^ k
  maxFieldError := 0.10 / (2 : ℝ) ^ k
  minSpeedup := 100 * (2 : ℝ) ^ k

/-- The coefficient-error bar tightens monotonically along the rungs. -/
theorem rung_coeff_antitone {j k : ℕ} (h : j ≤ k) :
    (Rung k).maxMeanCoeffError ≤ (Rung j).maxMeanCoeffError := by
  simp only [Rung]
  have hpow : (2 : ℝ) ^ j ≤ (2 : ℝ) ^ k := by
    exact pow_le_pow_right₀ (by norm_num) h
  have hj : (0 : ℝ) < (2 : ℝ) ^ j := by positivity
  apply div_le_div_of_nonneg_left (by norm_num) hj hpow

/-- The speedup bar tightens monotonically along the rungs. -/
theorem rung_speedup_mono {j k : ℕ} (h : j ≤ k) :
    (Rung j).minSpeedup ≤ (Rung k).minSpeedup := by
  simp only [Rung]
  have hpow : (2 : ℝ) ^ j ≤ (2 : ℝ) ^ k := pow_le_pow_right₀ (by norm_num) h
  linarith

end OpenSpur.Problems.CfdSurrogate

• AirfRANS (2D RANS airfoil dataset, NeurIPS 2022 D&B)
• NeurIPS 2024 ML4CFD competition + results retrospective (LIPS scoring: accuracy, physics compliance, OOD, speed-up)
• DrivAerNet / DrivAerNet++ (8,000 car CFD designs, 39 TB)
• Emmi-Wing dataset (Emmi AI, NeurIPS 2025 ML4PS workshop)
• PhysicsX DINOZAUR (preprocessed public engineering-simulation datasets)
• Neural Concept DrivAerNet++ result (Cd R2 0.978, MAE 2.22e-3)