• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2023 年度 実施状況報告書

Computational complexity and practice of verified and efficient algorithms for dynamical systems

研究課題

研究課題/領域番号 20K19744
研究機関京都大学

研究代表者

THIES HOLGER  京都大学, 人間・環境学研究科, 特定講師 (50839107)

研究期間 (年度) 2020-04-01 – 2025-03-31
キーワードComputable Analysis / Exact Real Computation / Formal Proofs / Type Theory / ODEs
研究実績の概要

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.

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

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.

今後の研究の推進方策

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.

次年度使用額が生じた理由

Due to the pandemic, in the first years of the project international cooperation was difficult and less money than previously planned was allocated for travel expenses. This also slowed down the progress of the project in the first years. As international collaboration is very important for the progress of the project, the funds are planned to be used for visiting conferences and joint research with experts from other universities.

  • 研究成果

    (9件)

すべて 2024 2023 その他

すべて 雑誌論文 (1件) 学会発表 (6件) (うち国際学会 3件、 招待講演 1件) 備考 (2件)

  • [雑誌論文] Formalizing Hyperspaces for Extracting Efficient Exact Real Computation2023

    • 著者名/発表者名
      Michal Konecny, Sewon Park, Holger Thies
    • 雑誌名

      Leibniz International Proceedings in Informatics (LIPIcs)

      巻: 272 ページ: 59:1-59:16

    • DOI

      10.4230/LIPIcs.MFCS.2023.59

  • [学会発表] Applications of Exact Real Computation in Particle Physics2024

    • 著者名/発表者名
      Svetlana Selivanova, Holger Thies
    • 学会等名
      17th International Conference on Computability, Complexity and Randomness
    • 国際学会
  • [学会発表] Extending cAERN to spaces of subsets2023

    • 著者名/発表者名
      Michal Konecny, Sewon Park, Holger Thies
    • 学会等名
      29th International Conference on Types for Proofs and Programs
    • 国際学会
  • [学会発表] Advances in verified set and function calculi in Coq2023

    • 著者名/発表者名
      Pieter Collins, Sewon Park, Holger Thies
    • 学会等名
      Continuity, Computability, Constructivity 2023
  • [学会発表] Formal verification and program extraction for efficient computations over real numbers and hyperspaces2023

    • 著者名/発表者名
      Holger Thies
    • 学会等名
      Fifth Workshop on Digitalization and Computable Models
    • 招待講演
  • [学会発表] 計算可能解析学とCoq2023

    • 著者名/発表者名
      Holger Thies
    • 学会等名
      The 19th Theorem Proving and Provers meeting
  • [学会発表] Towards verified implementation of iterative and interactive real-RAM2023

    • 著者名/発表者名
      Sewon Park, Holger Thies
    • 学会等名
      Twentieth International Conference on Computability and Complexity in Analysis
    • 国際学会
  • [備考] Personal Website

    • URL

      http://www.holgerthies.com

  • [備考] cAERN project

    • URL

      https://github.com/holgerthies/coq-aern

URL: 

公開日: 2024-12-25  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi