| Project/Area Number |
24K20735
|
|---|
| 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 |
|---|
Principal Investigator |
THIES HOLGER 京都大学, 人間・環境学研究科, 特定講師 (50839107)
|
|---|
| Project Period (FY) |
2024-04-01 – 2029-03-31
|
| Project Status |
Granted (Fiscal Year 2024)
|
| Budget Amount *help |
¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Fiscal Year 2028: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2027: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2026: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2025: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2024: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
|
|---|
| Keywords | Formal Verification / Computable Analysis / Coq / Exact Real Computation / 計算可能解析学 / 微分方程式 / 精度保証付き数値計算 / 計算機援用証明 |
|---|
| Outline of Research at the Start |
he main purpose of the project is to apply and extend ideas from computable analysis to verified and efficient exact computation over uncountable mathematical structures based on strong theoretical foundations and its formal verification using proof assistants.
The project not only aims for theoretical correctness results but also for efficiency in terms of resource usage and for usability in practical applications. Additionally to empiric evaluation of algorithms by experiments, efficiency is also studied systematically in form of complexity theory.
|
| Outline of Annual Research Achievements |
During this fiscal year, significant progress was made on extending the Coq formalization library cAERN for formalizing exact real computation. The library was expanded to include solution operators for simple polynomial ordinary differential equations (ODEs). From these formal proofs, programs that compute ODE trajectories with arbitrary precision can be automatically extracted. Experimental results confirmed that these extracted programs perform efficiently in practice. The results were presented at the ITP 2024 international conference.
Building on this, the approach was further generalized to cover ODEs with analytic right-hand sides for any finite dimension. This generalization no longer depends on the cAERN library and can be used more broadly within the Coq ecosystem, improving accessibility and integration and allows to compute solutions directly in the proogf assistant additionally to extracting programs. A paper summarizing these results is currently being prepared.
In another direction, we extended our previous formalization of subsets and continuity from Euclidean spaces to general Polish spaces, which are important in analysis and probability theory. We showed the equivalence of several representations of subsets in this setting, and all results were fully formalized in Coq.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
The research project has proceeded according to the planned schedule without major obstacles. Key milestones outlined in the original research plan were successfully achieved during the fiscal year, including the extension of the Coq library cAERN to support polynomial ODEs and the development of a more general formalization for analytic ODEs. These results were presented at major international conferences and form the basis of an upcoming publications. In addition, further progress was made in the formalization of foundational concepts in analysis, exceeding the original scope. While some technical challenges were encountered, they were resolved within expected timeframes. Overall, the project is on track and developing steadily toward its goals.
|
| Strategy for Future Research Activity |
Building on the formal foundations developed so far, the research will proceed in two main directions. First, the generalized solution method for analytic ordinary differential equations will be further refined and extended to cover a broader class of initial value problems. In particular, it is planned to integrate the results better with some existing libraries in the Coq ecosystem, such as mathcomp-analysis. To this end, it is planned to also formalize some results from classical analysis addtionally to the constructive theorems developed so far. This is also expected to enable further generalization of the approach to selected classes of partial differential equations.
At the same time, efforts will be made to improve the efficiency and practical applicability of the formalized theory. To this end, experimental evaluations will be conducted, including applications to concrete problems arising in fields such as physics.
|
