مجله‌ی وزین New Scientist در شماره آوریل سال ۲۰۱۹ مقاله جالبی منتشر کرده از پروژه ۱۰ ساله آقای Christian Szegedy و تیمشون برای آموزش حل تئوری‌های ریاضی به هوش مصنوعی گوگل. در زمان چاپ مقاله، حدود ۶۰٪ از تئوری‌های تست توسط این الگوریتم با منطق درست حل شده و تعدادی هم هنوز حل نشده است.

ظاهرا به علت رقابت سخت بین فیس‌بوک و گوگل در این زمینه با تاخیر زیادی در خصوص این پروژه‌ها اطلاعات منتشر می‌شود. نکته‌ی جالب در مورد این یادگیری، توسعه‌ی سیستم‌های شبه‌مغز برای این سیستم هوش مصنوعی است.

HOList: An Environment for Machine Learning of Higher-Order Theorem Proving

We present an environment, benchmark, and deep learning driven automated theorem prover for higher-order logic. Higher-order interactive theorem provers enable the formalization of arbitrary mathematical theories and thereby present an interesting, open-ended challenge for deep learning. We provide an open-source framework based on the HOL Light theorem prover that can be used as a reinforcement learning environment. HOL Light comes with a broad coverage of basic mathematical theorems on calculus and the formal proof of the Kepler conjecture, from which we derive a challenging benchmark for automated reasoning. We also present a deep reinforcement learning driven automated theorem prover, DeepHOL, with strong initial results on this benchmark.

این مصاحبه‌ی کریستین سزگدی رو اگر علاقه دارید ببینید.