• 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 2021)
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 Final Research Achievements

In this project we develop several formal tools to deal formally with probability and graphs. We provide a formalization of probability theory and more generally of Lebesgue integration in the Coq proof assistant. We develop theories to reason about tree and graph structures and apply them to the formal verification of programs. We applied the resulting theories to the formalization of the bases of information theory and artificial intelligence. We also develop theories to verify probabilistic programs and provide a generic and extensible framework to verify effectful programs in the Coq proof assistant. Most of our results are available as open access papers and open source software.

Academic Significance and Societal Importance of the Research Achievements

形式検証は一般的には基礎的な研究と見なされる。伝統的な数学分野の定理に対する形式検証実験のほうが注目を集めているからである。一方、IT製品の安全性評価に重要な、産業応用にも不可欠な技術である。例えば自動車のように、人命にかかわるシステムに人工知能を搭載するためには、その品質保証の技術が欠かせない。しかし、研究者の注目が薄い分野となっている。本研究では、確率的プログラミングでは初めて、正しさが証明されたソフトウェア実装とその形式化に必要な数学ライブラリが得られる。よって、人工知能の安全性・機械学習の形式検証・信頼性を保証するための基盤技術になりうる。

Report

(4 results)
  • 2021 Final Research Report ( PDF )
  • 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

    • ISBN
      9783030510534, 9783030510541
    • 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

    • ISBN
      9783030535179, 9783030535186
    • 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 Issue: 6 Pages: 1123-1164

    • 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

      Lecture Note in Computer Science

      Volume: 11601 Pages: 235-247

    • DOI

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

    • ISBN
      9783030236786, 9783030236793
    • 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

      International Symposium on Information Theory and Its Applications, Singapore, October 28--31, 2018, IEICE/IEEE Xplore

      Volume: 1 Pages: 665-669

    • 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: 2023-01-30  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi