• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Formal verification of probabilistic graphical models and its application to artificial intelligence

Research Project

Project/Area Number 18H03204
Research Category

Grant-in-Aid for Scientific Research (B)

Allocation TypeSingle-year Grants
Section一般
Review Section Basic Section 60010:Theory of informatics-related
Research InstitutionNational Institute of Advanced Industrial Science and Technology

Principal Investigator

Affeldt Reynald  国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (40415641)

Co-Investigator(Kenkyū-buntansha) 勝股 審也  国立情報学研究所, アーキテクチャ科学研究系, 特任研究員 (30378963)
中野 圭介  東北大学, 電気通信研究所, 教授 (30505839)
J Garrigue  名古屋大学, 多元数理科学研究科, 教授 (80273530)
Project Period (FY) 2018-04-01 – 2021-03-31
Project Status Completed (Fiscal Year 2020)
Budget Amount *help
¥8,840,000 (Direct Cost: ¥6,800,000、Indirect Cost: ¥2,040,000)
Fiscal Year 2020: ¥2,990,000 (Direct Cost: ¥2,300,000、Indirect Cost: ¥690,000)
Fiscal Year 2019: ¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000)
Fiscal Year 2018: ¥2,730,000 (Direct Cost: ¥2,100,000、Indirect Cost: ¥630,000)
Keywords形式検証 / 確率プログラミング / 測度論 / ルベーグ積分 / 確率論 / モナド / Coq / 条件付き独立 / 情報理論 / graphoid
Outline of Annual Research Achievements

本プロジェクトの目的は、AIソフトウェアの厳密な品質評価ができるように、確率やグラフィカルモデルなどの数学的基盤を形式化することである。令和2年度、確率論に必要な実解析とモナドに基づくプログラミングに関する形式的検証の研究を行った。
昨年度行ったconvexとconical spacesの研究に基づいて、圏論の形式化を含む非決定性・確率プログラミングの検証基盤を完成させた。その成果は国際雑誌に掲載されている。一般的なモナドのプログラムをサポートするように、その検証基盤をモナドトランスフォーマとアレーモナドでモジュラーに拡張し、その成果を国際会議の会議録と国内学会で発表した。また、確率的なリーゾニングのため、モナド上のダイバージェンスを用いて関係プログラム論理を定式化し、その成果も国内学会で発表した。
昨年度開始した実解析の形式化に基づいて、測度論と積分をCoqで形式化し、国際ワークショップと国内学会で発表した。その形式化に基づいて、一般的な確率論の形式化を開始した。確率の因子分解の定理のファーストステップとして、昨年度開始したベイジアンネットワークの形式化を確率変数ベクトルを扱えるように拡張した。また、グラフィカルモデルに対する応用として、モジュラーなリーゾニングができるように、量子回路のゲートを線形変換として形式化した。そのゲートをノードとするグラフであり、 その意味論は確率分布上の関数として与えられる。
以上の成果は二つのソフトウェアとして配布している。 以上の研究のために、才川隆文(名古屋大学)、斉藤歩夢(東京工業大学)の協力を得た。

Research Progress Status

令和2年度が最終年度であるため、記入しない。

Strategy for Future Research Activity

令和2年度が最終年度であるため、記入しない。

Report

(3 results)
  • 2020 Annual Research Report
  • 2019 Annual Research Report
  • 2018 Annual Research Report

Research Products

(48 results)

All 2022 2021 2020 2019 2018 Other

All Journal Article (18 results) (of which Int'l Joint Research: 9 results,  Peer Reviewed: 18 results,  Open Access: 14 results) Presentation (19 results) (of which Int'l Joint Research: 8 results) Remarks (11 results)

  • [Journal Article] Practical Aspects of Monadic Equational Reasoning in Coq2022

    • Author(s)
      Ayumu Saito, Reynald Affeldt
    • Journal Title

      第24回プログラミングおよびプログラミング言語ワークショップ (PPL 2022)

      Volume: -

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed
  • [Journal Article] 関係プログラム論理のためのモナド上のダイバージェンス2022

    • Author(s)
      佐藤 哲也, 勝股 審也
    • Journal Title

      第24回プログラミングおよびプログラミング言語ワークショップ (PPL 2022)

      Volume: -

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed
  • [Journal Article] A trustful monad for axiomatic reasoning with probability and nondeterminism2021

    • Author(s)
      AFFELDT REYNALD、GARRIGUE JACQUES、NOWAK DAVID、SAIKAWA TAKAFUMI
    • Journal Title

      Journal of Functional Programming

      Volume: 31

    • DOI

      10.1017/s0956796821000137

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Extending equational monadic reasoning with monad transformers2021

    • Author(s)
      Reynald Affeldt, David Nowak
    • Journal Title

      26th International Conference on Types for Proofs and Programs (TYPES 2020), Leibniz International Proceedings in Informatics (LIPIcs)

      Volume: 188

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Formalization of the Lebesgue measure in MathComp-Analysis2021

    • Author(s)
      Reynald Affeldt, Cyril Cohen
    • Journal Title

      The Coq Workshop 2021, July 2, 2021, Jul 2021

      Volume: -

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Porting the Mathematical Components library to Hierarchy Builder2021

    • Author(s)
      Reynald Affeldt, Xavier Allamigeon, Yves Bertot, Quentin Canu, Cyril Cohen, Pierre Roux, Kazuhiko Sakaguchi, Enrico Tassi, Laurent Thery, Anton Trunov
    • Journal Title

      The Coq Workshop 2021, July 2, 2021, Jul 2021

      Volume: -

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis2020

    • Author(s)
      Affeldt Reynald、Cohen Cyril、Kerjean Marie、Mahboubi Assia、Rouhling Damien、Sakaguchi Kazuhiko
    • Journal Title

      10th International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France, June 29--July 6, 2020, Lecture Notes in Artificial Intelligence

      Volume: 12167 Pages: 3-20

    • DOI

      10.1007/978-3-030-51054-1_1

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Reasoning with Conditional Probabilities and Joint Distributions in Coq2020

    • Author(s)
      Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
    • Journal Title

      Computer Software

      Volume: 37(3) Pages: 79-95

    • NAID

      130007906562

    • Related Report
      2020 Annual Research Report 2019 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Formal Adventures in Convex and Conical Spaces2020

    • Author(s)
      Affeldt Reynald、Garrigue Jacques、Saikawa Takafumi
    • Journal Title

      13th Conference on Intelligent Computer Mathematics (CICM 2020), Bertinoro, Forli, Italy, July 26--31, 2020, Lecture Notes in Artificial Intelligence

      Volume: 12236 Pages: 23-38

    • DOI

      10.1007/978-3-030-53518-6_2

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] A Library for Formalization of Linear Error-Correcting Codes2020

    • Author(s)
      Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
    • Journal Title

      Journal of Automated Reasoning

      Volume: TBD

    • DOI

      10.1007/s10817-019-09538-8

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Competing inheritance paths in dependent type theory: a case study in functional analysis2020

    • Author(s)
      Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi
    • Journal Title

      10th International Joint Conference on Automated Reasoning (IJCAR 2020) LNAI

      Volume: 12167

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Vers la formalisation en Coq des transformateurs de monades modulaires2020

    • Author(s)
      Celestine Sauvage, Reynald Affeldt, David Nowak
    • Journal Title

      31st Journees Francophones des Langages Applicatifs (JFLA 2020)

      Volume: 1 Pages: 23-30

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Formal Adventures in Convex and Conical Spaces2020

    • Author(s)
      Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
    • Journal Title

      13th Conference on Intelligent Computer Mathematics (CICM 2020) LNCS

      Volume: TBD

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Streaming Ranked-Tree-to-String Transducers2019

    • Author(s)
      Takahashi Yuta、Asada Kazuyuki、Nakano Keisuke
    • Journal Title

      24th International Conference on Implementation and Application of Automata (CIAA 2019) LNCS

      Volume: 11601 Pages: 235-247

    • DOI

      10.1007/978-3-030-23679-3_19

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Proving Tree Algorithms for Succinct Data Structures2019

    • Author(s)
      Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka
    • Journal Title

      10th International Conference on Interactive Theorem Proving (ITP 2019)

      Volume: N.A.

    • NAID

      40022501257

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Reasoning with conditional probabilities and joint distributions in Coq2019

    • Author(s)
      Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa
    • Journal Title

      21st Workshop on Programming and Programming Languages (PPL2019), Iwate-ken, Hanamaki-shi, March 6--8, 2019, JSSST

      Volume: 1 Pages: 1-16

    • NAID

      130007906562

    • Related Report
      2018 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Examples of formal proofs about data compression2018

    • Author(s)
      Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa
    • Journal Title

      Proceedings of ISITA

      Volume: 1 Pages: 633-637

    • DOI

      10.23919/isita.2018.8664276

    • Related Report
      2018 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] ComplCoq: Rewrite Hint Construction with Completion Procedures2018

    • Author(s)
      Mirai Ikebuchi and Keisuke Nakano
    • Journal Title

      Proc. of the Coq Workshop 2018

      Volume: 1 Pages: 1-2

    • Related Report
      2018 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Presentation] Practical Aspects of Monadic Equational Reasoning in Coq2021

    • Author(s)
      Ayumu Saito, Reynald Affeldt
    • Organizer
      第24回プログラミングおよびプログラミング言語ワークショッ(PPL 2022)
    • Related Report
      2020 Annual Research Report
  • [Presentation] 関係プログラム論理のためのモナド上のダイバージェンス2021

    • Author(s)
      佐藤 哲也, 勝股 審也
    • Organizer
      第24回プログラミングおよびプログラミング言語ワークショッ(PPL 2022)
    • Related Report
      2020 Annual Research Report
  • [Presentation] Formalization of the Lebesgue measure in MathComp-Analysis2021

    • Author(s)
      Reynald Affeldt, Cyril Cohen
    • Organizer
      The Coq Workshop 2021, online, July 2, 2021, Jul 2021
    • Related Report
      2020 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Porting the Mathematical Components library to Hierarchy Builder2021

    • Author(s)
      Reynald Affeldt, Xavier Allamigeon, Yves Bertot, Quentin Canu, Cyril Cohen, Pierre Roux, Kazuhiko Sakaguchi, Enrico Tassi, Laurent Thery, Anton Trunov
    • Organizer
      The Coq Workshop 2021, online, July 2, 2021, Jul 2021
    • Related Report
      2020 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Progress report on the formalization of the Lebesgue integral in MathComp-Analysis2021

    • Author(s)
      Reynald Affeldt, Cyril Cohen
    • Organizer
      17th Theorem Proving and Provers Meeting (TPP2021), 2021/11/21-22
    • Related Report
      2020 Annual Research Report
  • [Presentation] Extending Monae to formalize quicksort using monads in Coq2021

    • Author(s)
      Ayumu Saito, Reynald Affeldt
    • Organizer
      17th Theorem Proving and Provers Meeting (TPP2021), 2021/11/21-22
    • Related Report
      2020 Annual Research Report
  • [Presentation] Formalization of integration theory in Coq2021

    • Author(s)
      Reynald Affeldt, Cyril Cohen
    • Organizer
      第24回プログラミングおよびプログラミング言語ワークショップ (PPL 2022)
    • Related Report
      2020 Annual Research Report
  • [Presentation] Formalizing quantum circuits with MathComp/Ssreflect2021

    • Author(s)
      才川 隆文
    • Organizer
      17th Theorem Proving and Provers Meeting (TPP2021), 2021/11/21-22
    • Related Report
      2020 Annual Research Report
  • [Presentation] Formalization of measure theory in Coq2020

    • Author(s)
      Reynald Affeldt, Cyril Cohen
    • Organizer
      第23回プログラミングおよびプログラミング言語ワークショッ(PPL 2021)
    • Related Report
      2020 Annual Research Report
  • [Presentation] Competing inheritance paths in dependent type theory: a case study in functional analysis2020

    • Author(s)
      Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi
    • Organizer
      10th International Joint Conference on Automated Reasoning (IJCAR 2020)
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Formal Adventures in Convex and Conical Spaces2020

    • Author(s)
      Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
    • Organizer
      13th Conference on Intelligent Computer Mathematics (CICM 2020)
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Streaming Ranked-Tree-to-String Transducers2019

    • Author(s)
      Yuta Takahashi, Kazuyuki Asada, Keisuke Nakano
    • Organizer
      24th International Conference on Implementation and Application of Automata (CIAA 2019)
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Proving Tree Algorithms for Succinct Data Structures2019

    • Author(s)
      Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka
    • Organizer
      10th International Conference on Interactive Theorem Proving (ITP 2019)
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Vers la formalisation en Coq des transformateurs de monades modulaires2019

    • Author(s)
      Celestine Sauvage, Reynald Affeldt, David Nowak
    • Organizer
      31st Journees Francophones des Langages Applicatifs (JFLA 2020)
    • Related Report
      2019 Annual Research Report
  • [Presentation] Reasoning with conditional probabilities and joint distributions in Coq2019

    • Author(s)
      Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa
    • Organizer
      21st Workshop on Programming and Programming Languages (PPL2019), Iwate-ken, Hanamaki-shi, March 6--8, 2019, JSSST
    • Related Report
      2018 Annual Research Report
  • [Presentation] Examples of formal proofs about data compression2018

    • Author(s)
      Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa
    • Organizer
      International Symposium on Information Theory and Its Applications, Singapore, October 28--31, 2018, IEICE/IEEE Xplore
    • Related Report
      2018 Annual Research Report
    • Int'l Joint Research
  • [Presentation] ComplCoq: Rewrite Hint Construction with Completion Procedures2018

    • Author(s)
      Mirai Ikebuchi and Keisuke Nakano
    • Organizer
      The Coq Workshop 2018
    • Related Report
      2018 Annual Research Report
    • Int'l Joint Research
  • [Presentation] 定理証明支援系Coqにおける余帰納的証明のガード条件の漸進的検査2018

    • Author(s)
      小澤 祐也, 中野 圭介
    • Organizer
      第121回プログラミング研究発表会
    • Related Report
      2018 Annual Research Report
  • [Presentation] 定理証明支援系Coqにおける余帰納的証明のガード条件の漸進的検査2018

    • Author(s)
      小澤 祐也, 中野 圭介
    • Organizer
      The 14th Theorem Proving and Provers meeting (TPP 2018)
    • Related Report
      2018 Annual Research Report
  • [Remarks] A trustful monad for axiomatic... (preprint)

    • URL

      https://arxiv.org/abs/2003.09993

    • Related Report
      2020 Annual Research Report
  • [Remarks] Extending equational monadic... (preprint)

    • URL

      https://arxiv.org/abs/2011.03463

    • Related Report
      2020 Annual Research Report
  • [Remarks] A Coq formalization of information... (preprint)

    • URL

      https://github.com/affeldt-aist/infotheo

    • Related Report
      2020 Annual Research Report
  • [Remarks] Monadic effects and equational reasonig in Coq

    • URL

      https://github.com/affeldt-aist/monae

    • Related Report
      2020 Annual Research Report 2019 Annual Research Report
  • [Remarks] Math. Comp. compliant Analysis Library

    • URL

      https://github.com/math-comp/analysis

    • Related Report
      2020 Annual Research Report
  • [Remarks] A Coq formalization of information theory

    • URL

      https://github.com/affeldt-aist/infotheo

    • Related Report
      2019 Annual Research Report
  • [Remarks] Manuscript

    • URL

      https://hal.inria.fr/hal-02463336v2

    • Related Report
      2019 Annual Research Report
  • [Remarks] Preprint

    • URL

      https://arxiv.org/abs/2003.09993

    • Related Report
      2019 Annual Research Report
  • [Remarks] Preprint

    • URL

      https://arxiv.org/abs/2004.12713

    • Related Report
      2019 Annual Research Report
  • [Remarks] infotheo

    • URL

      https://github.com/affeldt-aist/infotheo

    • Related Report
      2018 Annual Research Report
  • [Remarks] Monadic equational reasoning in Coq

    • URL

      https://github.com/affeldt-aist/monae

    • Related Report
      2018 Annual Research Report

URL: 

Published: 2018-04-23   Modified: 2022-12-28  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi