| 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-2024)
Kyushu University (2020) |
|---|
Principal Investigator |
THIES HOLGER 京都大学, 人間・環境学研究科, 特定講師 (50839107)
|
|---|
| Project Period (FY) |
2020-04-01 – 2025-03-31
|
| Project Status |
Completed (Fiscal Year 2024)
|
| 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 / Formal Verification / Real Number Complexity / ODEs / Proof Assistants / Coq / Computational Complexity / Exact Real Computation / Complexity Theory / Formal Proofs / Type Theory / Program Extraction / Spaces of subsets / 計算可能解析学 / 計算量 / 計算機援用証明 / 実数計算 / Computable analysis / Differential equations / Verification / Formal proofs |
|---|
| 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 Final Research Achievements |
The project focused on the development of formally verified algorithms for the accurate and efficient solution of ordinary differential equations (ODEs). Based on ideas from real-number complexity theory, the algorithms were proven correct using the Coq proof assistant.
In particular, Taylor expansion methods were formalized in Coq, and program extraction techniques were applied to automatically generate certified programs that compute solution trajectories of ODEs. These programs guarantee mathematical correctness while remaining computationally practical. The results, including both theoretical advances and verified implementations, were published in peer-reviewed journals and presented at leading international conferences.
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究は、常微分方程式の解を高精度かつ誤りなく計算できるアルゴリズムを、数学的に正しさを保証しながら構築・実装した点に意義があります。これにより、物理・生物・工学など多くの分野で使われるシミュレーション結果の信頼性が向上し、安全性が求められる制御システムなどへの応用が期待されます。さらに、証明とプログラムが一体となった形で成果を共有することにより、ソフトウェアの透明性や長期的な保守性の向上にもつながります。
|
