| Project/Area Number |
20K19744
|
|---|
| Research Category |
Grant-in-Aid for Early-Career Scientists
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | Kyoto University (2021-2023)
Kyushu University (2020) |
|---|
Principal Investigator |
THIES HOLGER 京都大学, 人間・環境学研究科, 特定講師 (50839107)
|
|---|
| Project Period (FY) |
2020-04-01 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2023: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2022: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2021: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2020: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
|
|---|
| Keywords | Computable Analysis / Exact Real Computation / Formal Proofs / Type Theory / ODEs / Program Extraction / Spaces of subsets / Proof Assistants / 計算可能解析学 / 計算量 / 計算機援用証明 / 実数計算 / Computable analysis / Differential equations / Verification / Formal proofs / Complexity Theory |
|---|
| Outline of Research at the Start |
The research project aims to get insights into the computational complexity of problems in the physical world and to provide efficient and formally verified algorithms for computations that involve real numbers. Such algorithms lead to better, more reliable and reusable software.
|
| Outline of Annual Research Achievements |
This year's main focus was on the implementation of exact real computation in the Coq proof assistant. Previous results on the computation on subsets have been extended and new efficient representations for dealing with subsets have been devised and compared. The results were summarized for presentation at the 48th International Symposium on Mathematical Foundations of Computer Science and an extended journal version is currently in progress.
Further, during a research visit by Pieter Collins (Maastricht University) possible applications to his work on verified numerics were discussed.
Large progress was also made toward one of the main goals stated in the research proposal, that is, toward a verified solver for ordinary differential equations in exact real computation. In joint work with Sewon Park (Kyoto University) a simple solver for polynomial ordinary differential equations was implemented in the Coq proof assistant. For this, it was also necessary to formalize a theory of classical functions in our system, and results from classical mathematics concering e.g. differentiabilty. From proofs in our formal system, we can extract Haskell programs for such a solvers.The programs can be used to solve polynomial ODEs on some interval and print out approximations of the result up to any desired output precision.
Lastly, some applications to particle physics could be discovered. Simulation of particle dynamics turns out to be a good case study for exact real computation, as it often requires a very high precision that can not be achieved by classical numerical methods.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
Large advancements toward the original goal of verified ODE solving could be made during the last AY. First, the PI together with his collaborators could extend the previous formalization to a theory of classical functions, which e.g. could be used to formalize statements about continuity and differentiabilty, which are in turn needed to define solution operators for ODEs. Further, on top of this theory a simple solver for ODEs was implemented and verified to be correct. This solver can be extracted as a Haskell program which has shown to perform rather efficiently.
Also, some practical applications of the work in particle physics could be discovered.
The PI could present several of these new results on international conferences and workshops.
On the other hand, the solver currently only works for 1-dimensional polynomial ODEs and is thus not very generic. There is still some work left to generalize the solver to higher dimension and more generic types of functions.
|
| Strategy for Future Research Activity |
First, it is planned to summarize the results obtained in the previous AY in a publication at an international conference. The main task in this AY is then to extend the results further. Currently the ODE solver only works for 1-dimensional polynomial ODEs. As a first step, it is planned to extend the results to higher-dimensions. This is quite challenging, as it also requires the formalization of some classical results, that we currently only formalized for 1 dimension. Nonetheless, the algorithm itself generalizes nicely to higher dimension, and thus an implementation should be possible.
The PI plans to present these results at international conferences and workshops, in particular the CCA and CCC conferences.
Further, the applications of the work in particle physics will be explored more deeply, in collaboration with experts from physics.
Regarding changes to the research plan, while in previous years also the comparison to other proof assistants, and in particular the system IFP, was a central topic, it is planned to focus mostly on the Coq formalization in the coming AY, as more progress toward the initial goal of verified ODE solving could be done in Coq. Still it is planned to consider how some of the results could be formalized in a logic based system like IFP.
|
