一句话：在构造类型论与可计算实数下建立全局优化与回归的联系，并给出收敛准则及 Agda 机器化证明。
论文研究连续函数的确定性、完备且一般的全局优化与广义回归之间的联系。作者以构造类型论和可计算实数为理论基础，将全局优化视为回归的一种推广，并利用全局优化的收敛性质导出新的回归收敛准则。由于采用可计算实数而非浮点数，该方法能在精度和终止性方面给出强理论保证。全部理论已在证明助手 Agda 的安全模式下形式化；作者还用 Java 的现成构造性实数库实现示例，表明该途径在算法上具有前景。
We draw new connections between deterministic, complete, and general global optimisation of continuous functions and a generalised notion of regression, using constructive type theory and computable real numbers. Using this foundation we formulate novel convergence criteria for regression, derived from the convergence properties of global optimisations. We see this as possibly having an impact on optimisation-based computational sciences, which include much of machine learning. Using computable reals, as opposed to floating-point representations, we can give strong theoretical guarantees in terms of both precision and termination. The theory is fully formalised using the safe mode of the proof assistant AGDA. Some examples implemented using an off-the-shelf constructive reals library in JAVA indicate that the approach is algorithmically promising.