4 0 0 0 数学の自動化を推進するための機械学習を用いた定理自動証明手法
数学における証明のを計算機を用いて一部自動化することを目指します.本申請課題は,この最終目標に対する探索研究として,自然数に関する命題の証明の一部自動化を目指します.本申請課題では,証明が二者ゲームとして定式化でき,したがってゲーム AI の学習手法を証明ゲームに適用することで有能な自動証明アルゴリズムを錬成できるのではないか,というアイデアに基づいて研究を進めます.自動証明は様々なシステムが意図通りに動作することを保証するための要素技術として用いられており,その点で将来的に産業的なインパクト・貢献の可能性が期待できると考えています.
1 0 0 0 機械学習技術による高速な演繹的推論エンジンの開発
本研究では,近年著しい発展を遂げている機械学習技術を数理論理学的な問題に応用して,高効率な演繹的推論エンジンを構成することを目指す.機械学習技術は画像認識やゲームAIを含む様々な分野で著しい成功を遂げているが,証明などの演繹的推論が関わる分野には未だに古典的な演繹的推論技術が機械学習技術に優位である問題が多い.これまでの研究では解きたい問題を直接解く機械学習モデルを作る End-to-End の方法が主流であったが,本研究では解きたい問題ではなく機械学習に適した問題を学習させて,学習結果を演繹的推論エンジンで活用する.
1 0 0 0 OA AI時代を見据えたプログラム検証技術
プログラム検証とは、プログラムが正しく振る舞うかどうかを実行前に網羅的に検証する技術であり、ソフトウェアの信頼性向上のために欠かせないものである。本研究課題では、近年の機械学習技術の台頭とそれに伴うコンピュータによって制御されたシステムの社会への普及を踏まえ、(1)代表者らがこれまで研究を進めてきた高階モデル検査などの自動プログラム検証技術や理論をさらに発展させるとともに、(2)プログラム検証技術のさらなる飛躍のために機械学習技術を活用し、さらに(3)機械学習技術の台頭に伴うソフトウェアの質と量の変化に対応するための、新たなプログラム検証技術の確立を目指す。
- 著者
- 関山 太 山県 弘忠
- 出版者
- 日本育種学会
- 雑誌
- 育種学雑誌 (ISSN:05363683)
- 巻号頁・発行日
- vol.26, no.2, pp.p146-151, 1976-06
水稲パーオキシダーゼザイモグラムの器官特異性を検出する目的で,4種類のポリアクリルアミドゲル電気泳動法を比較検討した。このうち垂直カラムによる焦点電気泳動法が優れていたが,市販の泳動分析装置てばアイソエンザイムの分離が不十分であった。そこで著者らは新しくユニット式ポリアクリルアミドゲルカラム電気泳動装置(U-タイプ)を作製した。U-タイプは6本のゲルカラム用ガラス管,これらガラス管を支える上下2枚の支持板,上部および下部電極,支持板と上部電極を支える左右2本の支持棒,および泳動距離の調節装置などから成り,外径10mm以下,長さ50〜200m?のガラス管を泳動目的に合わせて選定できること,泳動途中でゲルカラム毎に通電の中断あるいは開始ができること(ユニット配列),さらに泳動に必要な電極液の量が陽極0.25〜0.6ml(カラム直径3〜5mmの場合),陰極20mlと少量でよいことなどの利点を有する。水稲品種銀坊主の第1.3葉令期(第2葉がその全長の約3分の1まで伸長した時期)の植物体を供試し,U-タイプにより直径3mm,長さ150mmのゲルカラムを用いて泳動し,多数の明瞭なバンドから成る安定なザイモグラムを得た。これら36種の泳動条件を比較した結果,最適泳動条件は電圧が10V/cm,泳動時間が16〜18時間,電極液濃度が0.8%V/V(P)〜2.2%V/V(T)あるいは1.2%V/V(P)〜3.3%V/V(T)であった。