科目名 Course Title

知能ソフトウェア特論 [Intelligent Software]

責任教員 Instructor

栗原 正仁 [Masahito KURIHARA] (大学院情報科学研究科)

担当教員 Other Instructors

小山 聡(情報科学研究科), 佐藤 晴彦(情報科学研究科)

科目種別 Course Type

情報科学研究科専門科目

開講年度 Year2014

時間割番号 Course Number046140

開講学期 Semester

１学期

単位数 Number of Credits

2

授業形態 Type of Class講義

対象年次 Year of Eligible Students

1～1

言語コード・言語 Language Code, Language Type0 日本語で行う授業

キーワード Key Words
プログラムの正当性，モデル検査，項書換え系，階層型ニューラルネットワーク，カーネル法，サポートベクターマシン
correctness of programs, model checking, term rewriting system, hierarchical neural networks, kernel methods, support vector machines

授業の目標 Course Objectives
ソフトウェア開発のための知能的な方法，及び知能的な振る舞いをするソフトウェアの要素について，理論と技術の理解を深めることを目標とする。具体的には，まずソフトウェア工学の基礎である逐次プログラム，並行システム，および関数型プログラムの理論などに基づき，プログラムの自動検証と知能的な開発技術について学ぶ。続いて，人工知能学の基礎である機械学習の理論などに基づき，ニューラルネットワーク，サポートベクターマシン，及び情報の組織化などの知能的なソフトウェアの要素技術について学ぶ。
The objective of this course is to deepen the understandings of the theory and technologies for (1) the intelligent methods for softwaredevelopment and (2) the elements of intelligent software. More precisely, we first study the methods for automated verification of computer
programs and intelligent software development, based on the theories of sequential programs, concurrent systems, and functional programs
developed in the field of software engineering. Then we study the elements of intelligent software such as neural networks, support vector
machines, and information organization, based on the theories of machine learning and other technologies developed in the field of artificialintelligence.
到達目標 Course Goals
1)逐次プログラムの正当性の概念を述べ，その関連技術を説明できる。
Students will be able to describe the general concepts of the correctness of sequential programs and explain the related techniques.
2)並行システムのモデル検査の概念を述べ，その関連技術を説明できる。
Students will be able to describe the general concepts of the model checking for concurrent programs and explain the related techniques.
3)関数型プログラムのための項書換え系の概念を述べ，その関連技術を説明できる。
Students will be able to describe the general concepts of the term rewriting system for functional programs and explain the related techniques.
4)階層型ニューラルネットワークの概念を述べ，その関連技術を説明できる。
Students will be able to describe the general concepts of hierarchical neural networks and explain the related techniques.
5)カーネル法とサポートベクターマシンの概念を述べ，その関連技術を説明できる。
Students will be able to describe the general concepts of support vector machines and explain the related techniques.
6)機械学習を用いて簡単なタスクを行うことができ，その結果を評価できる。
Students will be able to use machine learning for simple tasks and evaluate the results.
授業計画 Course Schedule
1)ガイダンス：知能ソフトウェアとはGuidance: What is the intelligent software?
2)逐次プログラムの正当性(1) 正当性証明の基本原理
Correctness of sequential programs (1) Principles of correctness proof
3)逐次プログラムの正当性(2) ホーア論理
Correctness of sequential programs (2) Hoare logic4)モデル検査(1) 並行システムとモデル検査
Model checking (1) Concurrent systems and model checking5)モデル検査(2) 時相論理
Model checking (2) Temporal logic

6)項書換え系(1) 代数的仕様と項書換え
Term rewriting systems (1) Algebraic specification and term rewriting
7)項書換え系(2) 停止性
Term rewriting systems (2) Termination
8)項書換え系(3) 合流性
Term rewriting systems (3) Confluence9)機械学習の基礎：汎化と正則化
Introduction to machine learning: generalization and regularization10)階層型ニューラルネットワーク(1) ネットワーク構造と推論
Hierarchical neural networks (1) network structure and inference11)階層型ニューラルネットワーク(2) 誤差逆伝搬学習
Hierarchical neural networks (2) backpropagation learning12)カーネル法
Kernel methods
13)サポートベクターマシン
Support vector machines
14)情報の組織化と機械学習
Information organization and machine learning15)情報検索と機械学習
Information retrieval and machine learning
準備学習（予習・復習）等の内容と分量 Homework
事前配付資料に基づき予習を行い，与えられた課題の解決を通して復習を行うこと。１回の講義あたり，４時間程度の予習・復習が必要である。
Students are required to study pre-distributed materials and solve the given problems before and after the classes, respectively. On average,
about four hours will be needed for each class.
成績評価の基準と方法 Grading System
レポート，定期試験，講義への参加状況などを総合して達成度を評価する。
Evaluation is based on the reports, the final examination, and the attendance.
テキスト・教科書 Textbooks
講義資料を配布する。授業の前半（ソフトウェアの検証）の回では，さらに興味があれば，以下の講義指定図書 1),2)を参考にされたい。後半（機械学習）の回では，以下の講義指定図書 3),4),5)を参照する。
Original materials will be distributed in the classes. Students wishing to study more about program verification are adivsed to read the books 1) and2) in the Reading List below. Machine learning sections refer to the books 3), 4) and 5) in the Reading List.
講義指定図書 Reading List
1) Rigorous Software Development: An Introduction to Program Verification／Jose Bacelar Almeida, et al.：Springer，2011
2) Term Rewriting and All That／Franz Baader, et al.：Cambridge University Press，1998
3) パターン認識と機械学習 上 - ベイズ理論による統計的予測／C. M. ビショップ：丸善出版，2007
4) パターン認識と機械学習 下 - ベイズ理論による統計的予測／C. M. ビショップ：丸善出版，2008
5) Pattern Recognition and Machine Learning／C. M. Bishop：Springer，2006
参照ホームページ Websites
研究室のホームページ Website of Laboratory
http://kussharo.complex.ist.hokudai.ac.jp/

備考 Additional Information
プログラミング，論理，線形代数，確率および統計に関する講義を学部において履修していることを前提としている。
Basic knowledge on programming, logic, linear algebra, probability, and statistics is needed.