トポロジーの形式化における深層学習の適用の研究

深度学习在拓扑形式化中的应用研究

基本信息

批准号：
20K20340
负责人：
久我健一
金额：
$ 13.31万
依托单位：
Chiba University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Challenging Research (Pioneering)
财政年份：
2020
资助国家：
日本
起止时间：
2020-04-01 至 2024-03-31
项目状态：
已结题

项目摘要

証明支援系を用いた数学の形式化は一般に非常に困難であるので、この研究では位相幾何学を起点とする数学の形式化において、深層学習を適用することを目標においている。そのために、自然言語処理の深層学習アーキテクチャーであるtransformerを利用するための研究を行なった。研究開始当初は当時主流であったRNN特にLSTMの利用を計画していたが、2018年以降、BERTやGPT等のtransformerベースの学習が自然言語処理において高い性能をあげることが報告されたので、この研究ではtransformerベースの汎用モデルとも考えられるT5(Text To Text Transfer Transformer)を用いて証明支援系Coqによる定理証明の形式化を効率化・自動化することを目指した。まず技術的な課題として、CoqがOCamlで記述されており、他方でC++等で作成されPython等で使用されることが想定されているPyTorch、TensorFlow等の深層学習フレームワークとの連携が直接的には取れない点がある。これについては、当研究で開発したpicoqをHuggingFace社のTransformersと連携が取れるように調整した。これによって、既存の数学形式化coqライブラリについてはほぼ完全に学習データが作成できる状態になった。また学習データ作成における課題として、通常の自然言語学習のGPT等のようにビッグデータを収集するのみでは、数学的及び論理的に複雑な内容を学習できないと考えられる点、および、数学の形式化データ自身が少なく、受動的な学習では効果がないと考えられる点でがあげられる。そこで我々はcoqからのインターラクティブなレスポンスから学習データを作成するプログラムを作成した。これによって様々な数学形式化coqライブラリからT5学習データを作成することができた。

由于使用证明支持系统来形式化数学通常非常困难，因此本研究旨在从拓扑开始将深度学习应用于数学形式化。为此，我们对使用 Transformer 进行了研究，Transformer 是用于自然语言处理的深度学习架构。研究之初，我们计划使用RNN，尤其是当时主流的LSTM，但从2018年开始，有报道称BERT和GPT等基于Transformer的学习在自然语言处理中具有较高的性能。在这项研究中，我们的目标是使用 T5（文本到文本传输转换器）的证明支持系统 Coq 来简化和自动化定理证明的形式化，T5 可以被认为是基于通用转换器的模型。首先，作为技术问题，Coq 是用 OCaml 编写的，另一方面，它无法直接与 PyTorch 和 TensorFlow 等深度学习框架链接，这些框架是用 C++ 等创建的，预计将用于Python等。有一些点不能采取。对此，我们对本研究中开发的picoq进行了调整，使其能够与HuggingFace的Transformers配合。因此，现在可以为现有的数学形式化 COQ 库创建几乎完整的训练数据。此外，作为创建学习数据的挑战，人们认为仅仅通过收集正常自然语言学习的 GPT 等大数据是不可能学习数学和逻辑上复杂的内容的，而且数学的形式化也是问题。数据本身很小，被动学习被认为是无效的。因此，我们创建了一个程序，根据 COQ 的交互式响应创建训练数据。这使我们能够从各种数学形式化 COQ 库创建 T5 训练数据。

项目成果

期刊论文数量（7）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Some experiments of formalizing finite/projective geometry using Monte Carlo tree search

使用蒙特卡罗树搜索形式化有限/射影几何的一些实验

DOI：
发表时间：
2019
期刊：
影响因子：
0
作者：
Ken'ichi Kuga
通讯作者：
Ken'ichi Kuga

Let Models Speak Ciphers: Multiagent Debate through Embeddings

让模型说出密码：通过嵌入进行多智能体辩论

DOI：
10.48550/arxiv.2310.06272
发表时间：
2023-10-10
期刊：
ArXiv
影响因子：
0
作者：
Chau Pham;Boyi Liu;Yingxiang Yang;Zhengyu Chen;Tianyi Liu;Jianbo Yuan;Bryan A. Plummer;Zhaoran Wang;Hongxia Yang
通讯作者：
Hongxia Yang

Training Transformers to formalize Topology in Coq

训练 Transformers 以在 Coq 中形式化拓扑