Model Discovery and Verification With Symbolic, Hybrid Symbolic-Numeric and Parallel Computation

摘要：自然（如人的心跳）或人为过程（如无线信号的无线电波）的数学模型是对系统参数（如时间点）的评估产生模型值（如波的振幅）的数学表达式或算法。模型是通过理解过程创建的，这暗示了表达的形式，并通过观察和测量一个实际的过程。根据这些数据点，通过计算拟合出最佳模型。Erich Kaltofen既研究如何拟合特定的数据模型，比如稀疏多项式的分数，又研究如何证明计算产生了最好的模型。创建最佳拟合和随后的最优性认证的算法可能是计算密集型的，需要多处理器计算环境。Erich Kaltofen和他的学生和合作者将为符号模型设计算法，如稀疏多变分函数和具有非常大甚至参数指数的公式。我们的算法可以处理精确和近似数据，后者通过混合符号/数字技术。当应用随机化时，浮点标量的计算需要一种新的概率分析，我们将利用最近在估计随机矩阵的谱和条件数方面的结果。这种随机化的一个应用是高度欠定和过定的密集线性系统的有效解。误差分析的一种新的替代方法是精确验证我们的近似解的全局最优性的符号计算。半定规划和牛顿精算用于计算数值平方和表示，它被转换为近似有理数下界的精确有理数恒等式。由于确切的证书不容置疑，因此不需要对数字启发式进行充分分析。我们将寻找可以验证非常大的平方和并因此适用于大输入的合理化。我们将为出现的符号和混合符号-数值计算任务开发并行和分布式计算工具。

ABSTRACT:A mathematical model for a natural (e.g., the heart beat of ahuman) or man-made process (e.g., the radio wave of a wirelesssignal) is a mathematical expression or an algorithm that onevaluation of system parameters (such as a point in time) yieldsa model value (e.g., the amplitude of a wave). Models arecreated by understanding the process, which suggests the formof the expression, and by observing and measuring an actualprocess. From those data points the best model is fitted bya computation. Erich Kaltofen studies both how to fit to datacertain models, such as fractions of sparse polynomials, andthen how to certify that the computation has produced the bestpossible model. The algorithms for creation of best fits andsubsequent certification of optimality can be compute-intensiveand require multi-processor computing environments.Erich Kaltofen and his students and collaborators will designalgorithms for symbolic models such as sparse multivariaterational functions and formulas with very large and evenparametric exponents. Our algorithms can work with both exactand approximate data, the latter by hybrid symbolic/numerictechniques. Computation with floating point scalars requiresa new kind of probabilistic analysis when randomization isapplied, and we will make use of recent results on estimatingthe spectra and condition numbers of random matrices. Oneapplication of such randomization is the efficient solutionof highly under- and overdetermined dense linear systems.A new alternative to error analysis is the exact validation viasymbolic computation of the global optimality of our approximatesolutions. Semidefinite programming and Newton refinementare used to compute a numerical sum-of-squares representation,which is converted to an exact rational identity for a nearbyrational lower bound. Since the exact certificates leave nodoubt, the numeric heuristics need not be fully analyzed.We will search for rationalizations that can validate verylarge sums-of-squares and hence apply to large inputs. We willdevelop parallel and distribute computing tools for the arisingsymbolic and hybrid symbolic-numeric computation tasks.