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.
Benchmark risk, compute budgets, and uncertainty records
Definition
Fix measurable spaces and , a metric target space with its Borel sigma-algebra , and a nonempty truth class with inherited sigma-algebra . Let and be measurable target and forward maps. The admissible state set is a declared nonempty -measurable subset . The observation model is a specified probability kernel from to ; in an additive-noise model, when has a measurable addition operation, it is the law of for a declared noise law of , while nonadditive or model-dependent observation noise is encoded directly by .
The forward solver, when a numerical evaluation is used, is the specified procedure for evaluating this model, including its discretization, tolerances, finite call budget, and any model-specific admissibility test; exact evaluation is the special case with no numerical-solver error. A failed admissibility test or solver call is recorded with its failure status and is not silently omitted from the benchmark results.
A benchmark specification also declares a training law on a named measurable space for all random variables used to fit a method or select its hyperparameters; those variables may be paired or unpaired. It declares a test law on for evaluation pairs , and any separate validation law used for tuning. The training and test laws need not agree. Each candidate method is identified by its fitting procedure and by its deployed measurable deterministic reconstruction rule or randomized reconstruction kernel from to . Its population test risk is the risk under as defined by the inverse-risk functional; a reported finite-sample score must additionally name its test sample and empirical aggregation rule. No risk transfer or generalization bound follows from the benchmark specification.
Before comparison, the specification fixes a nonnegative product-measurable loss , an uncertainty diagnostic, and a finite compute-budget vector. An uncertainty diagnostic is a declared measurable statistic of the method outputs and, when applicable, target labels, together with its target quantity; for example, if a reported set-valued estimate has a product-measurable membership event , its test coverage is . The budget vector records the applicable maximum counts of forward-model queries, adjoint queries, gradient evaluations, ODE right-hand-side evaluations, solver or sampling steps, and elapsed runtime; inapplicable counts are marked as not applicable, not zero. It also records the hardware, numerical precision, software/model versions, random seeds, tuning data, and stopping tolerances needed to interpret those counts. Each method's result records its metric values, uncertainty diagnostic, realized compute counts, solver status, and failed runs. A comparison is tied to the declared test law, test sample, loss, solver, admissibility rules, and tuning protocol; when budgets or other conditions differ, those differences are reported as part of the comparison. The specification defines an evaluation protocol, not a theorem ranking algorithms.
The arrows label declared information flow into fitting, observation generation, and evaluation. The diagram asserts no equality between and and no risk-transfer result.
Definition references
Risk under a specified joint evaluation law
Point reconstruction rules and randomized posterior kernels
Separate forward operators, observation laws, and prior support
A model-specific finite solver/admissibility contract
Bal, Introduction to Inverse Problems, §1.1 and §§8.2–8.3, full lecture notes
Zheng et al., InverseBench, ICLR 2025, full paper and appendices
Depends on
Used by
- A solver-invalid FWI iterate Example
- Black-hole VLBI benchmark Example
- First-Born optical scattering benchmark Example
- Full waveform inversion benchmark Example
- Multi-coil MRI benchmark Example
- Prior-matched and out-of-distribution cases Example
- Two-dimensional Navier–Stokes benchmark Example
- Scope of InverseBench findings Remark
Dependency tree · two levels
27 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
- Guillaume Bal, Introduction to Inverse Problems, E6901 Lecture Notes for 2011 course, full 132-page PDF (standard reference, not scraped)
- Hongkai Zheng et al., InverseBench: Benchmarking Plug-and-Play Diffusion Priors for Inverse Problems in Physical Sciences, ICLR 2025, full 29-page paper and appendices (standard reference, not scraped)