Achievement Award

Pioneering research on verified numerical computations Shinichi OISHI

Shinichi OISHI

With the development of information and communication technology, digital computers have come into wide use in various sectors of society. In computers, floating-point arithmetic and numbers are used instead of real arithmetic and numbers. In 1985, IEEE 754 was established as the standard for floating-point operations and was revised in 2008.   Since floating-point numbers are represented with limited precision, every floating-point operation may involve a rounding error. The more operations, the more errors. In scientific computing, large-scale problems frequently arise, and a huge number of operations are required. As a result, we cannot know how accurate the computed results are. Verified numerical computations play an important role in such cases. Moreover, in order to solve outstanding mathematical problems, verified numerical computations become essential in some cases. For example, the Kepler conjecture, which concerns the densest sphere packing arrangement in Hilbert's 18th problem, had remained unproven for more than 300 years, and it was only resolved by the use of verified numerical computations. Thus it can be seen that there is an increased need for verified numerical computations in science and engineering.   Prof. Oishi is involved in the study of verified numerical computations from basic theory to applications. In particular, he established and promoted fast verification methods for linear systems, facilitating the practical use of verified numerical computations. In the past, most of the researchers in this area were of the opinion that it was too difficult to figure out numerical errors. Although interval arithmetic already existed, it was not practicable because it is not applicable to large-scale problems, in principle, and the computational cost in terms of time is several hundreds or thousands times greater than ordinary floating-point arithmetic. Moreover, it was difficult to obtain accurate solutions to ill-conditioned problems that are highly susceptible to rounding errors.   In these circumstances, first, Prof. Oishi devised a fast verification method for modestly well-conditioned problems, which is as fast as the standard numerical method. Second, he developed an efficient verification method for ill-conditioned problems. The method incurs a minimal computational cost for obtaining accurate solutions by introducing error-free transformations (EFT) of floating-point computations. Fig.1. Error analysis of higher-precision dot product using vectorized error-free transformations   Since fundamentals of numerical computations come down to reducing problems to be solved using linear systems, the achievements by Prof. Oishi made it possible put verified numerical computations to practical use. In fact, his achievements enable us to verify the accuracy of numerical solutions of linear systems involving millions of dimensions. INTLAB, which was developed by his collaborator Prof. S. M. Rump, has further refined and advanced such achievements. INTLAB has several thousand users in more than 50 countries. Most of the researchers working in the field of verified numerical computations use INTLAB.   As stated above, Prof. Oishi achieved a breakthrough in the research area of numerical computations. He established fast and efficient verified numerical computations, which can prove the existence of solutions to equations, and compute numerical solutions with exceptional accuracy. Such achievements have received high recognition, for example, he has received the Medal with Purple Ribbon in 2012, was awarded the Commendation for Science and Technology by the Minister of MEXT in 2010, and became an IEICE fellow in 2006. Prof. Oishi has made outstanding contributions to science and engineering, and richly deserves the IEICE Achievement Award.

References

（1）A. Takayasu, X. Liu, and S. Oishi, “Remarks on computable a priori error estimates for finite element solutions of elliptic problems,” Nonlinear Theory and Its Applications, IEICE, vol.5, no.1, pp.53-63, Jan. 2014. （2）N. Yamanaka and S. Oishi, “Fast quadruple-double floating point format,” Nonlinear Theory and Its Applications, IEICE, vol.5, no.1, pp.15-34, Jan. 2014. （3）X. Liu and S. Oishi, “Verified eigenvalue evaluation for Laplacian over polygonal domain of arbitrary shape,” SIAM J. Numer. Anal., vol.51, no. 3, pp.1634-1654, May 2013. （4）K. Ozaki, T. Ogita, and S. Oishi, “Tight and efficient enclosure of matrix multiplication by using optimized BLAS,” Numer. Linear Algebra Applications, vol.18, no.2, pp.237-248, Feb. 2011. （5）S. Oishi, T. Ogita, and S. M. Rump, “Iterative refinement for ill-conditioned linear systems,” Japan J. Indust. Appl. Math., vol.26, no.2-3, pp.465-476, Oct. 2009. （6）S. M. Rump, T. Ogita, and S. Oishi, “Accurate floating-point summation part I: Faithful rounding,” SIAM J. Sci. Comput., vol.31, no.1, pp.189-224, Oct. 2008. （7）T. Ogita, S. M. Rump, and S. Oishi, “Accurate sum and dot product,” SIAM J. Sci. Comput., vol.26, no.6, pp.1955-1988, Jul. 2005. （8）S. Oishi and S. M. Rump, “Fast verification of solutions of matrix equations,” Numer. Math., vol. 90, no.4, pp.755-773, Feb. 2002. （9）S. Oishi, “Numerical verification of existence and inclusion of solutions for nonlinear operator equations,” J. Comput. Appl. Math., vol.60, no.1-2, pp.171-185, June 1995. （10）S. Oishi, “Two topics in nonlinear system analysis through fixed point theorems,” IEICE Trans. Fundamentals, vol.E77-A, no.7, pp.1144-1153, July 1994.