第１２回 Theorem Proving and Provers ミーティング、プログラム 2016 年 11 月 14 日（月） 10:25 - 10:45 受付 10:45 - 11:15 井上健太（千葉大学） 代数ニューラルネットワークのCoqにおける形式化 11:15 - 11:45 池渕未来（名古屋大学） Coqによる大規模データ処理・機械学習ライブラリの開発 13:30 - 14:00 山田伊織（電気通信大学） CoqからのD言語プログラムの抽出 14:00 - 14:30 才川隆文（名古屋大学） Reed-Solomon符号の形式化 15:00 - 15:30 Jacques Garrigue（名古屋大学） Formalization of graphs for verification of error-correcting codes 15:30 - 16:00 木下修司（神奈川大学） Analysis of Open Systems Dependability Requirements in Agda 16:30 - 17:15 TPPmark 18:00 - 20:00 懇親会 2016 年 11 月 15 日（火） 10:00 - 10:30 坂口和彦（筑波大学） 定理証明器Coqの効率的な有限ドメイン関数ライブラリ 10:30 - 11:00 土橋拓馬（明治大学） 動的幾何学ソフトウェアにおける画像認識入力と、 作図手順の自動推定手法の提案 11:15 - 11:45 松本早貴、山本光晴（千葉大学） ペトリネットにおけるKarp-Miller木構成と 被覆性判定の正当性の形式化 11:45 - 12:15 Fadoua Ghourabi（お茶の水女子大学） Intervals, Nests and Points 概要： - 井上健太 千葉大学 代数ニューラルネットワークのCoqにおける形式化 今日、機械学習の分野で、ニューラルネットワークと呼ばれるグラフを用いて 学習を行う、ディープラーニングと呼ばれる手法が大きな注目を集めている。 しかし、このニューラルネットワークにおいてその学習が行われるメカニズム や、与えられた問題に対し、それを解くのに最適な構造が判明しておらず、ま た学習後のニューラルネットワークの正当性の判定もあいまいである等、ブ ラックボックスとして利用されているのが現状である。本研究の目的はニュー ラルネットワークの構造を数学的な手法で解明することである。 具体的には、ニューラルネットワークを代数を用いて記述し、これのもつ性質 を調べることでニューラルネットワークの構造がもつ性質を解析する。 また、この代数ニューラルネットワークを証明支援系Coqで形式化する。 本発表では、Coqで形式化した代数ニューラルネットワークの定義やいくつか の性質、それらをまとめたライブラリを紹介する。 また、それを用いて符号問題と呼ばれるEXOR問題を一般化した問題の解の存在 性の証明も行い、この結果から階層型ニューラルネットワークを多層化するこ とへの考察を発表する。 - 池渕未来 名古屋大学 Coqによる大規模データ処理・機械学習ライブラリの開発 Nested Vector Language(NVL)はApache Spark、TensorFlow等の大規模データ を処理するシステムのための、現在MIT CSAILで開発されている中間言語であ る。NVLはいくつかの基本的な関数を持ち、それに対して内部で並列化やルー プ最適化等の変換を自動で行う。今回紹介する研究では、NVLの型や関数をCoq のModule Type上で抽象的に定義し、それに対するいくつかのプログラム変換 の正当性の証明を行った。また、Coq上で線型代数・多変数の微積分を扱う証 明付きのライブラリを実装し、その中の演算をNVLによる式への書き換え規則 の証明をした。さらに、それらの線型代数・微積分の演算を用いてニューラル ネットワークとその誤差逆伝播法による教師付き機械学習のプログラムを実装 した。本発表では、研究の全貌とともに、内部で扱っているFiat[1 ]ライブラ リの解説と、線型代数・微積分に関するLtacでの自動証明、証明付きの自動微 分について紹介する。尚、今回の研究はMIT CSAILのAdam Chlipala氏の下で行 われた。 [1] B. Delaware, C. Pit-Claudel, J. Gross, A. Chlipala. Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015. - 山田伊織 電気通信大学 CoqからのD言語プログラムの抽出 定理証明支援系Coqに対して、Cライクな静的型付きプログラミング言語Dへの 抽出機能を追加した。Coq標準の抽出機能は中間言語miniMLに変換する際に型 を削除するため、十分な型推論を持たないD言語では型情報を補完する必要が ある。この補完に用いた2つの手法とその比較結果を中心に、実装の概要を紹 介する。 - 才川隆文 名古屋大学 Reed-Solomon符号の形式化 Reed-Solomon符号のエラー訂正をCoqで形式化した。この形式化は今後BCH符 号, Goppa符号へ拡張する予定である。 - Jacques Garrigue 名古屋大学 Formalization of graphs for verification of error-correcting codes In previous work on linear codes, we have proved properties of the sum-product algorithm under the classical assumption that the graph has no cycle (i.e., this is actually a tree). As this assumption does not hold in practice, we have since then started the analysis of decoding for a computation graph ensemble, as described in [Modern Coding Theory, 2008]. For simplicity, we are now working on the binary erasure channel case. We will present our results, and explain the daunting difficulties of the task. - 木下修司 神奈川大学 Analysis of Open Systems Dependability Requirements in Agda 現在策定中の国際規格ISO/IEC 62853 Open Systems Dependabilityでは、オー プンシステム・ディペンダビリティ達成に必要な要件を4種類62個で定義して いる。しかし、これらの要件達成には何が必要なのか、要件どうしにはどのよ うな依存関係があるのか等は必ずしも明らかではない。本発表では、これらの 要件をAgdaによって型付けし、分析する試みを紹介する。 - 坂口和彦 筑波大学 定理証明器Coqの効率的な有限ドメイン関数ライブラリ 本研究は，対話的定理証明器 Coqの有限型と有限ドメイン関数に関する既存ラ イブラリを改良し，従来のライブラリを用いた証明をほとんど変更することな く，その証明から抽出されるプログラムの効率を大幅に改善したものである． Coq のSSReflect/Mathematical Componentsライブラリは，有限型と有限ドメ イン関数をサポートするライブラリ fintype と finfunを提供し，これらの データに対する証明の手間を大幅に削減することに成功している．しかし，そ の証明からプログラム抽出の手法で作成したプログラムは，多くの場合におい て非常に効率が悪いという問題がある．本研究では，fintype や finfunを改 善したライブラリを実装した．このライブラリを用いて作成した証明から抽出 した OCamlコードは，既存ライブラリの場合と比べて非常に高速である．例と して，行列積の計算では，計算時間をおよそ O(n^5) から O(n^3)へ改善でき たことを示す．また，既存の SSReflect ライブラリを用いた Coqの証明は， ほとんど書き換えることなく本研究のライブラリを用いた証明となる．例とし て，Gonthier らの Feit-Thompson定理の約17万行におよぶ形式証明が，わず か 10行以下の修正で，本研究のライブラリを用いた証明にできたことを示す． - 土橋拓馬 明治大学 動的幾何学ソフトウェアにおける画像認識入力と、作図手順の自動推定手法の提案 動的幾何学ソフトウェアとは、マウス操作で平面幾何の作図を行えるソフト ウェアの総称である。本研究では、動的幾何学ソフトウェアにおいて、画像か らの入力を許容するシステムを提案する。ここで2つの問題がある。1つは与え られた画像から認識された点、直線、円などに後から作図手順を追加すること が可能かという問題、もう1つは認識された点、直線、円などの要素が、どの ような作図手順により得られたかを自動推定できるかという問題である。この 2点について、いくつかの知見が得られたので報告する。 - 松本早貴、山本光晴 千葉大学 ペトリネットにおけるKarp-Miller木構成と被覆性判定の正当性の形式化 ペトリネットは多くのシステムに適用可能なモデル化ツールであり、主に並行 的・非同期的・非決定的動作を記述するのに用いられる。ペトリネットに関す る性質のうち、有界性・被覆性については被覆木(Karp-Miller木)を用いた判 定により決定可能であることが知られている。我々は昨年の発表で、構成的な 停止性証明の技術を用いてCoq関数としてKarp-Miller木構成関数を実装した。 この実装はCoqのProgramライブラリを用いて与えていたのだが、この方法では 関数の展開補題の証明が困難であることが後にわかった。本発表では昨年とは 異なる方法で構成関数を定義し、それを用いた被覆性判定の正当性についての Coq/Ssreflectによる形式的証明を与える。これらの性質の証明においては、 木に対して直接示すのではなくある種の状態遷移系を介在させて間接的に示す ことでより簡潔な証明を与えることが可能となった。 - Fadoua Ghourabi お茶大 Intervals, Nests and Points Points are often taken as primitive objects and from a set of points we build other objects such as intervals. Given only one primitive type for intervals, can we construct points? In this ongoing work, we formalize Allen’s interval calculus in Isabelle/HOL where primitive objects are intervals. We then define points as special sets of intervals, called nests, and show that nests form a linear order.