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.
Benchmarks, prior shift, and solver admissibility
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Banach-Space Differential Calculus and Banach Manifolds
- Bayesian models, priors, and posterior laws
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Linear Operators and Quotient Spaces
- Compactness in Metric Spaces
- Complete Metrizability, Čech-Completeness, and Baire Category
- Completeness, Completion, and Uniform Continuity
- Complex Norms and Realification
- Complexification, Realification and Real Structures
- Conditional Distributions and Regular Conditional Probability
- Conditional Expectation
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Convex and Semicontinuous Functions on Rⁿ
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Countability Axioms and Cardinal Functions
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Domination and Likelihood Ratios
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Estimators and Randomized Procedures
- Finite Counting, Factorials and Binomial Coefficients
- Finite-element meshes and interpolation
- Foundations of the Real Numbers for Analysis
- Function-space priors and sample regularity
- Hilbert Space Geometry and Riesz Representation
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Infinite Product Measures and Kolmogorov Extension
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Inverse maps, identifiability, and stability
- Learned reconstruction targets and risk
- Lebesgue-Stieltjes Measures and Distribution Functions
- Likelihood potentials and posterior propriety
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Loss, Risk and Decision Theory
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Measurable Functions and Simple Approximation
- Measures and Their Basic Properties
- Metric Spaces
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Nonlinear maps and tangential cone control
- Nonlinear Tikhonov existence and stability
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- Order, Zorn's Lemma, and the Axiom of Choice
- Outer Measure and the Caratheodory Extension Theorem
- PDE-constrained inversion and adjoint error control
- Polynomial Rings, the Division Algorithm and Roots
- Posterior propriety and dominated Bayes formula
- Power Series and Real-Analytic Functions
- Probability Spaces Random Variables and Expectation
- Product Measures and the Fubini Tonelli Theorems
- Properties of the Integral and the Working FTC
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Score and diffusion methods for inverse data
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Sigma Algebras and Borel Sets
- Signed and Complex Measures Hahn and Jordan
- Simple Field Extensions and the Construction of the Complex Numbers
- Standard-Borel Real Codings and Determining Classes
- Statistical Experiments, Models and Identifiability
- Subspaces, Products, and Quotients
- Suprema and Infima
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Derivative and the Mean Value Theorems
- The Exponential Function
- The Lebesgue Integral and the Convergence Theorems
- The Radon Nikodym Theorem and Lebesgue Decomposition
- The Riemann Integral: Definition and Integrability
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Unknown operators, model mismatch, and robustness limits
- Vector Spaces, Linear Subspaces, Span and Direct Sums
- Weak Convergence Tightness and Representation
2 · Logical flowchart
3 · Definitions, theorems and proofs
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
Scope of InverseBench findings
Remark
Zheng et al.'s InverseBench reports 14 plug-and-play diffusion-prior algorithms and domain-specific baselines on five selected cases: first-Born optical scattering, raw multi-coil knee MRI, black-hole very-long-baseline interferometry, full waveform inversion, and two-dimensional vorticity-form Navier–Stokes inversion. For these experiments, the authors report that diffusion-prior methods often outperform conventional baselines when the training data are suitable, while a classical full-waveform-inversion optimizer initialized from a smoothed ground truth outperforms the tested diffusion-prior methods. In cases with closed-form forward models, methods using more forward-gradient queries can be more accurate and more expensive; the paper reports that this trend fails for its numerical PDE cases. Its Navier–Stokes split has one validation case and ten test cases. The paper reports step-size/Courant–Friedrichs–Lewy (CFL) failures in its PDE experiments. Its Figure 5 out-of-distribution diagnostics feed digit images to a black-hole prior trained on simulated black-hole images, and nine-cell scattering sources to a prior trained on one-to-six-cell sources; for the black-hole case, the authors report outputs with the prior's characteristic ring feature. These are empirical observations for the named data, solvers, methods, tuning protocol, and hardware; they establish no universal ranking, stability bound, posterior exactness, risk-transfer bound, or robustness theorem.
There is a first-Born notation discrepancy between the paper and its released implementation. Appendix B.1 defines a contrast-dependent total field and then displays a sensor equation with that field multiplied by the contrast, which does not itself exhibit a fixed linear map. The pinned implementation instead passes the fixed incident field into the sensor-propagation routine and constructs its cached linear matrix from that fixed field. This page therefore identifies the implemented benchmark as the first-Born linear case and does not infer linearity from the printed contrast-dependent expression.
Remark references
Benchmark specification and reporting protocol
Risk under a named joint evaluation law
Learned estimators, score fields, and posterior samplers carry no automatic guarantee
Operator and prior mismatch are distinct and imply no automatic robustness bound
Solver admissibility and CFL thresholds are model-specific
Exact diffusion scores versus learned or plug-in approximations
Zheng et al., InverseBench, ICLR 2025, full paper and appendices
InverseBench implementation, pinned inverse_scatter.py source
4 · Examples, counterexamples and false statements
None yet.
Sources
- Guillaume Bal, Introduction to Inverse Problems, E6901 Lecture Notes for 2011 course, full 132-page PDF
- 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
- InverseBench source implementation, pinned revision 1db5932bc2995504491663d1e2c498e7317c5404, inverse_problems/inverse_scatter.py