著者
末永 幸平 塚田 武志 関山 太朗
出版者
京都大学
雑誌
挑戦的研究(萌芽)
巻号頁・発行日
2019-06-28

数学における証明のを計算機を用いて一部自動化することを目指します.本申請課題は,この最終目標に対する探索研究として,自然数に関する命題の証明の一部自動化を目指します.本申請課題では,証明が二者ゲームとして定式化でき,したがってゲーム AI の学習手法を証明ゲームに適用することで有能な自動証明アルゴリズムを錬成できるのではないか,というアイデアに基づいて研究を進めます.自動証明は様々なシステムが意図通りに動作することを保証するための要素技術として用いられており,その点で将来的に産業的なインパクト・貢献の可能性が期待できると考えています.

言及状況

Twitter (4 users, 4 posts, 11 favorites)

もしかするとネタにマジレスかもしれませんが、機械学習を定理証明に援用する研究としては、例えばこの辺りの研究があります。たまにこれ系の話題が Twitter で流れてくるのを見ます。 https://t.co/FWSn5tCBmi https://t.co/FMRuRWjmig

収集済み URL リスト