2023 Fiscal Year Annual Research Report
正しさと効率の形式的証明を備えたスケルトン並列プログラミング環境に関する研究
| Project/Area Number |
19K11903
|
|---|
| Research Institution | Kyushu Institute of Technology |
|---|
Principal Investigator |
江本 健斗 九州工業大学, 大学院情報工学研究院, 准教授 (00587470)
|
|---|
| Project Period (FY) |
2019-04-01 – 2024-03-31
|
| Keywords | 定理証明支援系 / 深層学習 |
|---|
| Outline of Annual Research Achievements |
今年度は、昨年度までに発見された新たな課題について、その解決に向けたアプローチの開発・評価を行った。具体的には、定理証明支援系による証明構築の困難さの解消に向けて、その一部を深層学習的なアプローチにより自動化する手法の試作・評価を行った。定理証明支援系での形式証明の構築の完全自動化は、理想的ではあるものの、既存研究の結果から（少なくとも現状では）現実的とはいえないと考えられる。この理想を一段現実的にした手法として、「人間が証明の道筋を用意し、それに沿っての証明を自動化する」という方法が考えられる。人間が証明全体の構築を行う際にもこの道筋の用意は必須であり、証明における最も創造性を必要とする部分である。よって、その部分については人間の能力を用いることとし、それより下の部分を自動化しようという考えである。その具体的な実現として「証明の中間状態の大雑把な形を与え、その形に至るまでの証明を自動で構築する」というシステムを、深層学習モデルを用いて構築し、その性能や使い勝手を評価した。結果として、まだまだモデルの改良が必要なものの、アプローチとしては有用であるとの結論が得られた。今後は新たな研究課題としてこの手法の完成を目指す。
研究期間全体を通じては、定理証明支援系での形式証明を経た正しい（並列）プログラムの構築に対し、その支援技術の開発や具体的なモデル・言語機構の形式化を行った。形式化については、計算量を含めた低層並列計算モデル、並列計算のための負荷分散等を実現できる言語機能、並列プログラムの構成パーツ等の定式化の基礎となる recursion schemes の定理証明支援系での形式化に取り組んだ。支援技術については、これらの証明を簡単化するためのライブラリやシステムの構築に取り組んだ。これらの取り組みで得られた成果は、国際会議や国内雑誌、国内大会・研究会等で発表した。
|
