| 研究課題/領域番号 |
24K20735
|
|---|
| 研究種目 |
若手研究
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
小区分60010:情報学基礎論関連
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
THIES HOLGER 京都大学, 人間・環境学研究科, 特定講師 (50839107)
|
|---|
| 研究期間 (年度) |
2024-04-01 – 2029-03-31
|
| 研究課題ステータス |
交付 (2024年度)
|
| 配分額 *注記 |
4,680千円 (直接経費: 3,600千円、間接経費: 1,080千円)
2028年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2027年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2026年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2025年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2024年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
|
|---|
| キーワード | Formal Verification / Computable Analysis / Coq / Exact Real Computation / 計算可能解析学 / 微分方程式 / 精度保証付き数値計算 / 計算機援用証明 |
|---|
| 研究開始時の研究の概要 |
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.
|
| 研究実績の概要 |
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.
|
| 現在までの達成度 |
現在までの達成度
2: おおむね順調に進展している
理由
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.
|
| 今後の研究の推進方策 |
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.
|
