| 研究課題/領域番号 |
25330034
|
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
汪 金芳 千葉大学, 理学(系)研究科(研究院), 教授 (10270414)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2017-03-31
|
| キーワード | Big Math Data / Conditional Independence / Cain Algebra / 自動証明 / Coq/SSReflect / Causal Inference / Sensitivity / Specificity |
|---|
| 研究実績の概要 |
ヨーロッパやアメリカを中心として、数学の様々な理論が形式化されつつある。数学の定理や証明も統計的に分析できる時代に入りつつある。統計学者に数学の理論の統計分析という新たなフロンティアへの挑戦には様々な可能性と困難があり、今年度は数学理論という新たなビッグデータの統計解析に関連したいくつかの問題に取り組んだ。より具体的には、Coq/SSReflectで形式化された数学の定理と証明に着目し、これらの定理および証明を数値化し、パタン認識の問題について研究を行った。
確率関数や確率密度関数の代数的性質を抽出し、条件付き独立性を操作するための枠組みとしてCain代数が提案されている。Cain代数学では、条件付き独立性に関する全ての条件と結論が方程式の形で記述されている。今年度では、定理証明支援言語Coq/SSReflectを用いて、Cain代数の基本形であるCainoidの形式化を行った。条件付き独立性の自動証明を視野に入れて、この研究を更に進展させていくつもりである。
画像診断法の有効性の統計的研究は様々な視点で行われているが、本研究では複数の読影者（multiple raters ）によるクラスターデータ（clustered data）が得られることを前提に、２つの画像診断法の有効性の比較法を提案した。また、複数の読影者が存在することを想定し、読影者間の相関と感度特異度間の相関を考慮した、変量効果モデルに基づいた、感度と特異度の信頼区間の構築法を提案した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本研究はおおむね順調に進展しているが、研究成果をより精緻なものにするため、当初計画にはなかった条件付独立性の形式化に取り組んだ。想定した以上に束論やケーインの形式化に時間を要したため、補助事業期間を延長し、平成28年度においても引き続き研究を行う予定である。
|
| 今後の研究の推進方策 |
定理証明支援言語 SSReflect の library である finset.v を積極的に利用し、有限集合の場合に焦点を当て、ケーインの形式化の完成を目指す。
|
| 次年度使用額が生じた理由 |
研究成果をより精緻なものにするため、当初計画にはなかった条件付独立性の形式化に取り組んだ。想定した以上に束論やケーインの形式化に時間を要したため、補助事業期間を延長し、平成28年度においても引き続き研究を行う予定である。
|
| 次年度使用額の使用計画 |
得られた研究成果の発表などのため、主に旅費として使用する予定である。
|
| 備考 |
このサイトにはケーイン代数やその形式化に関する情報を掲載しています。
|
