2015工学部研究紹介|信州大学
58/76

製品設計や仕様書の正しさをチェックする(ものづくりへの応用)証明問題のインタラククティブ教材(教育への応用)(数学以外への形式化数学の応用例) 情報⼯学科師⽟研究室研究から広がる未来卒業後の未来像形式化数学記述言語によって、現行数学の全ての定理とその証明をライブラリ化するという壮大な目標をもった国際共同研究プロジェクトに参加しながら、形式化数学と計算機ソフトウエア開発の融合を目指しています。人手による解析や、全ての場合を尽くせるとは限らないテストデータによる試行に頼ることなく、その動作の正しさが数学的に裏付けされたプログラムを開発できる手法の構築を目指しています。先生は、論理的思考能力、数理的思考能力を身に付けた情報工学技術者となるように学生たちに指導しているそうです。師玉康成教授工学博士(慶応義塾大学)1987年防衛大学校理工学研究科研究員、1990年信州大学助手、助教授を経て1995年より同大学教授形式化数学記述言語とそれを用いた計算機検証の研究に従事。主に•数学基礎一般の形式化と検証・ライブラリ編纂•アルゴリズムの動作検証•形式化数学記述言語を用いた論理思考訓練教材の構築に取り組む。師玉研究室では数学定理と証明を計算機のプログラムのような形式化言語で書いてその論理的・数学的正しさを計算機で検査する研究をしています。この検査で正しいことが確かめられた定理と証明を辞書のようにライブラリにする国際共同研究プロジェクトに海外の研究者達とともに参加しています。例えばインターネットのデータ通信に使われる暗号は高度な代数学を用います。現代の科学・工学技術は数学なしには成り立ちません。株式の売買その他、経済活動も高度な数学を利用したコンピュータシステムが主役になっています。数学の研究成果の正しさを、誤りを犯しやすい人手によらず、計算機によって、厳密に、瞬時に検査できる手段は大変重要です。その使い道は定理の正しさを検査するだけではなく、将棋やチェスのルールのように複数の規則に従って、様々な要素や手続き、機能を論理的に組み合わせて作られる工学的なシステムの開発やその動作の検査にも応用できます。例えば計算機のプログラムは入力データから出力データを作る論理的な手続きを形式的な言語で表現したものであり、その動作は数学的な命題として表すことができます。これにより、今までのように、多くのテストデータを入力して処理結果を検査したり、誤りを犯しやすい人手によって動作を一行一行解析したりといった、不完全な方法ではなく計算機によって数学的に厳密に検査することができるようになります。それが正しいと確認されれば、その形式的な記述をそのまま、計算機プログラムに変換して使えば、その動作の正しさが数学的に裏付けされたプログラムを作ることができます。形式化数学記述⾔語と計算機検証ぬいぐるみ(くま)人(赤ちゃん、笑う、遊ぶ)画像からの情報の取り出し情報⼯学科⼭崎研究室研究から広がる未来卒業後の未来像画像というのは人間で考えると目から入る情報になります。画像処理技術は様々な場面で利用されていますが、CGや3D、バーチャルリアリティなどが注目されています。これらの技術は人間の目に入れるための情報をどのように作成するかに注目した分野になります。一方、人間は目から取り込んだ情報から人物や物の判定やそれらがどのような状態であるかを判断しています。このような技術には、自動販売機の人物が成人であるかの判定やカメラのシャッターの機能の人が笑っているかどうかを判定するといった技術があります。山崎研究室では、コンピュータで人間が行うような画像の判定や解析を行うことを研究しています。応用の一つとして、ハードディスクなどコンピュータデバイス製造過程での傷検出・認識処理の研究を行なっています。現在は人間のほうが正確に判断できるので、製造過程の多くの段階で人間が関わっています。人手・視認によらない品質管理、不良検出の自動化、ロボットによる部品の組み立てなど、物作り日本の産業基盤の根底、底力を支える広汎な技術です。同研究室では、それの数学的な手法を研究しています。デジタル画像処理を扱うための数学としては集合論、格子理論、位相幾何学、確率論などを基礎にした幾何的構造の解析や処理を行う数学数理形態学という分野の研究になります。山﨑浩助教博士(工学)1997年より同大学助教。形式化数学記述言語とそれを用いた画像処理手法検証の研究に従事。主に•数学基礎一般の形式化と検証・ライブラリ編纂•画像処理•e-learning:インターネットを利用した教育に取り組む。数理形態学の応用研究を通して、省力化、製造産業技術の高度化、高品質化、に参加し、世界一を誇る日本の物づくりの維持、活性化に貢献していきます。人件費の高騰や労働力不足に対応して行くためには自動化、ロボット化は必須であり、数理形態学の応用はその中で重要です。論理的思考能力,数理的思考能力を身につけたうえでシステムが理解できる卒業生はどんな職場・環境でも問題を解決できます。さらにそのような人は人を動かせる人物となっています。画像の数学的理解56

元のページ 

10秒後に元のページに移動します

※このページを正しく表示するにはFlashPlayer10.2以上が必要です