Projects

Develop a communication path characteristic collateral technology that guarantees the route characteristics of communication inside the system, detects unintended degrading, etc., and alarms and deterrences in a hybrid cloud system that connects multiple cloud infrastructures and internal networks with wide-area communication between data centers and bases.

We will carry out AI safety standard creation and research and development as an integrated initiative. The research and development items are as follows.

1. Data, learning model, AI system safety evaluation and management infrastructure technology
2. AI safety evaluation and implementation technology for AI products and services in the "living area"
3. AI safety guidelines, implementation explanations, and international standardization

Formal verification methods have been studied as a method to mathematically verify whether the system works as expected, and have been used to verify various systems. This study aims to establish a formal verification method to mathematically and strictly verify whether the risk response of the machine learning utilization system can be implemented. In particular, we will build a technology that automatically verifies the inadequacy of the risk response of the machine learning use system, and aim to improve the quality of products and services based on machine learning.

Today, computer programs, in addition to the manipulation of digital information and their networks, interact with the outside world, for program verification, not only formal logic and discrete mathematics, but also real analysis, probability theory, geometry, etc. Learning is necessary, and it is difficult to rigorously verify the various side effects of the program. To reduce its complexity, both a fundamental study of the semantics of the program and an integrated study that gives a consistent formal expression to advanced mathematics are necessary. In this study, on the theorem proof support system Rocq, real analysis, continuous probability, rigid geometry are formalized, and based on monad and equation reasoning, the formal foundation is constructed and evaluated.