How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Full waveform inversion benchmark
Example
In the InverseBench full-waveform-inversion (FWI) case, the unknown is the compressional-wave velocity on a two-dimensional physical domain ; its discretization is a velocity map . For each source signal , the pressure field starts with zero initial pressure and velocity, and on , and solves
and the observation is the receiver restriction , where samples the wavefield at the selected receivers. The benchmark uses a domain, horizontal and vertical grid spacings of and , a time step chosen to satisfy the numerical solver's Courant–Friedrichs–Lewy stability condition, a Ricker source wavelet, and of simulated time. Its top boundary has the natural free-surface condition, while the other boundaries have absorbing conditions of width grid points. It uses sources at depth and receivers evenly placed near the free surface at depth . The reported observation noise is zero. The CurveFaultB velocity-map split has training maps, one validation map, and ten test maps, resized to . These counts and solver settings define this empirical benchmark instance; they are not existence or convergence claims for full waveform inversion.
Example references
Facts & Assumptions
Given: A positive velocity map, the acoustic pressure-wave equation and source signal with zero initial pressure and velocity, the receiver sampling operator, a free-surface top and absorbing other boundaries of width grid points, sources at depth , receivers at depth , the stated discrete solver and mesh, and the finite CurveFaultB split.
Benchmark risk, compute budgets, and uncertainty records: a benchmark instance includes its forward solver, admissible inputs, noise, compute protocol, and test population.
Scope of InverseBench findings: the reported FWI outcomes concern this selected solver, tuning procedure, and test set only.
For an explicit conditional finite-data benchmark, supply the actual nonempty training, validation, and test lists of the stated sizes, including realized observations, target images, operator metadata, and valid discrete forward values. Let be the finite set of labelled cases, with its full power-set sigma-algebra; labels distinguish repeated images. Let with Euclidean distance and Borel sets, and let be the finite-dimensional observation-and-operator-metadata space with Borel sets. For case , set (its target image), (its discrete noiseless forward data), and (its recorded data, with the same metadata). Thus describes replay conditional on these realized lists, not a population of newly sampled velocity fields. Require because this case is noise-free; the forward values are outputs of the specified discrete solver on admissible inputs, with its actual settings recorded. Set , where is the test index set and ; use the analogous uniform empirical validation law. Take to be the point mass at the entire supplied fitting record, including training/tuning lists and seeds. This conditional specialization supplies laws, not just sample counts, and is not a reconstruction of the paper's full evaluation protocol.
Supply each candidate's complete fitting/tuning procedure and deployed measurable rule , with all seeds fixed. Fix the loss and a radius before testing. The uncertainty diagnostic is empirical coverage , targeting coverage of the balls of radius centered at under . Evaluate every test case once and average its loss. Before fitting or evaluation, supply finite upper bounds for every applicable forward, adjoint, gradient, ODE-evaluation, iteration/sampling, and runtime count, marking inapplicable entries as not applicable, together with hardware, precision, software/model versions, seeds, tuning data, and stopping tolerances. A procedure must return within these bounds or record failure; its deployed rule returns the zero image on failure. Retain that case in both aggregates and report every status and realized count. These supplied procedures and budget records are parameters of this mathematical specialization; the coverage statistic is not a reported InverseBench calibration result.
Verification
With the zero initial data and the stated source, boundary conditions, and solver, the forward call produces the acoustic wavefield; applying the receiver restriction gives the stated observation, with the velocity map as the parameter being inferred.
On the finite labelled truth space of [A1], and are measurable. Since , the replay kernel is the noise-free observation kernel for this supplied finite numerical model; its dependence on is measurable. The empirical test/validation laws and point-mass fitting law specify the population fields of [F1]. The counts fix their list sizes, while the actual supplied lists fix their atoms.
The squared loss and radius-ball membership event in [A2] are product-measurable, so the loss and coverage under the empirical test law equal the declared finite averages. With the supplied procedures, finite budgets, solver settings, metadata, and retained failure records, this gives the remaining fields of [F1]. The source experiment remains scoped as in [F2]; this finite-data specialization proves no continuum PDE existence, numerical convergence, population generalization, or posterior-calibration theorem.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
7 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Hongkai Zheng et al., InverseBench: Benchmarking Plug-and-Play Diffusion Priors for Inverse Problems in Physical Sciences, ICLR 2025, full paper and appendices (standard reference, not scraped)
- InverseBench source implementation, pinned revision 1db5932bc2995504491663d1e2c498e7317c5404, inverse_problems/acoustic.py (standard reference, not scraped)
- Devito v4.8.12 source, examples/seismic/acoustic/wavesolver.py (standard reference, not scraped)
- Devito v4.8.12 source, devito/types/dense.py (standard reference, not scraped)