2015 Fiscal Year Research-status Report
擬似尤度に基づく情報量基準の構築と過分散を持つ離散データの解析への応用
| Project/Area Number |
25330034
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
汪 金芳 千葉大学, 理学(系)研究科(研究院), 教授 (10270414)
|
|---|
| Project Period (FY) |
2013-04-01 – 2017-03-31
|
| Keywords | Big Math Data / Conditional Independence / Cain Algebra / 自動証明 / Coq/SSReflect / Causal Inference / Sensitivity / Specificity |
|---|
| Outline of Annual Research Achievements |
ヨーロッパやアメリカを中心として、数学の様々な理論が形式化されつつある。数学の定理や証明も統計的に分析できる時代に入りつつある。統計学者に数学の理論の統計分析という新たなフロンティアへの挑戦には様々な可能性と困難があり、今年度は数学理論という新たなビッグデータの統計解析に関連したいくつかの問題に取り組んだ。より具体的には、Coq/SSReflectで形式化された数学の定理と証明に着目し、これらの定理および証明を数値化し、パタン認識の問題について研究を行った。
確率関数や確率密度関数の代数的性質を抽出し、条件付き独立性を操作するための枠組みとしてCain代数が提案されている。Cain代数学では、条件付き独立性に関する全ての条件と結論が方程式の形で記述されている。今年度では、定理証明支援言語Coq/SSReflectを用いて、Cain代数の基本形であるCainoidの形式化を行った。条件付き独立性の自動証明を視野に入れて、この研究を更に進展させていくつもりである。
画像診断法の有効性の統計的研究は様々な視点で行われているが、本研究では複数の読影者（multiple raters ）によるクラスターデータ（clustered data）が得られることを前提に、２つの画像診断法の有効性の比較法を提案した。また、複数の読影者が存在することを想定し、読影者間の相関と感度特異度間の相関を考慮した、変量効果モデルに基づいた、感度と特異度の信頼区間の構築法を提案した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究はおおむね順調に進展しているが、研究成果をより精緻なものにするため、当初計画にはなかった条件付独立性の形式化に取り組んだ。想定した以上に束論やケーインの形式化に時間を要したため、補助事業期間を延長し、平成28年度においても引き続き研究を行う予定である。
|
| Strategy for Future Research Activity |
定理証明支援言語 SSReflect の library である finset.v を積極的に利用し、有限集合の場合に焦点を当て、ケーインの形式化の完成を目指す。
|
| Causes of Carryover |
研究成果をより精緻なものにするため、当初計画にはなかった条件付独立性の形式化に取り組んだ。想定した以上に束論やケーインの形式化に時間を要したため、補助事業期間を延長し、平成28年度においても引き続き研究を行う予定である。
|
| Expenditure Plan for Carryover Budget |
得られた研究成果の発表などのため、主に旅費として使用する予定である。
|
| Remarks |
このサイトにはケーイン代数やその形式化に関する情報を掲載しています。
|
