Proof Mining in Convex Optimization and related areas

凸优化及相关领域的证明挖掘

• 批准号: 400007828
• 负责人: Professor Dr. Ulrich Kohlenbach
• 金额: --
• 依托单位: Department of Computer Science
• 依托单位国家: 德国
• 项目类别: Research Grants
• 资助国家: 德国
• 项目状态: 未结题
• 来源: https://gepris.dfg.de/gepris/projekt/400007828?language=en
• 关键词: Proof; Mining; Convex; Optimization; related

In this Project we aim at using proof-theoretic methods from logic for the extraction of new data (such as effective bounds, "proof mining") from prima facie noneffective proofs in convex optimization and related areas.In the course of this logic-based methodology, suitable forms of so-called proof interpretations have been developed by the applicant during the past decades and successfully applied in nonlinear analysis. In the previous 3 years of funding we applied this at large scale to problems in the area of convex optimization and - additionally - also carried out new case studies in neighbouring areas such as ergodic theory, approximation theory and Tauberian theory.During the next 3 years we will extend this approach to further problems in convex optimization including those which have a connection to current work in the area of machine learning. Here we will focus on proofs which make use of generalizations of the concept of "monotonicity" for set-valued operators which have recently been studied in convex optimization and are used in the context of machine learning. We also intend to analyze proofs which study abstract Cauchy problems given by accretive operators.The main goal of this project is the extraction of rates of asymptotic regularity, metastability (in the sense of T. Tao) and convergence of central iterative procedures whose convergence is shown using such generalized monotonicity or accretivity properties of set-valued operators but also the generalization of such results from the setting of Hilbert spaces to metric structures, such as CAT(0)-spaces, and more general Banach spaces.

在这个项目中，我们的目标是使用逻辑证明理论方法从凸优化和相关领域的表面无效证明中提取新数据（例如有效范围，“证明挖掘”）。在这种基于逻辑的方法的过程中，申请人在过去几十年中开发了所谓的证明解释的合适形式，并成功应用于非线性分析。在过去 3 年的资助中，我们大规模地将这种方法应用于凸优化领域的问题，此外，还在遍历理论、逼近理论和陶伯理论等邻近领域进行了新的案例研究。在接下来的 3 年中，我们将把这种方法扩展到凸优化中的其他问题，包括那些与机器学习领域当前工作相关的问题。在这里，我们将重点关注利用集值算子的“单调性”概念的推广的证明，这些算子最近在凸优化中进行了研究，并在机器学习的背景下使用。我们还打算分析研究由累加算子给出的抽象柯西问题的证明。该项目的主要目标是提取渐近正则性、亚稳态（在 T.Tao 意义上）的速率和中心迭代过程的收敛性，其收敛性使用集值算子的广义单调性或累加性属性来显示，而且还将这些结果从希尔伯特空间的设置推广到度量 结构，例如 CAT(0) 空间，以及更一般的 Banach 空间。