Can an A.I. win a medal in the mathematical olympiad?-Benchmarking mechanized mathematics on pre-university problems 1

Takuya Matsuzaki, Hidenao Iwane, Munehiro Kobayashi, Yiyang Zhan, Ryoya Fukasaku, Jumma Kudo, Hirokazu Anai, Noriko H. Arai

研究成果: ジャーナルへの寄稿記事

抄録

This paper introduces a benchmark problem library for mechanized mathematics including computer algebra and automated theorem proving. The library consists of pre-university mathematical problems taken from exercise problem books, university entrance examinations, and the International Mathematical Olympiads. The subject areas include real algebra, geometry, number theory, pre-calculus, calculus, and combinatorics. It thus includes problems in various areas of pre-university mathematics and with a variety of difficulty. Unlike other existing benchmark libraries, this one contains problems that are formalized so that they are obtainable as the result of mechanical translation of the original problems expressed in natural language. In other words, the library is designed to support the integration of the technologies of mechanized mathematics and natural language processing towards the goal of end-To-end automatic mathematical problem solving. The paper also presents preliminary experimental results of our prototype reasoning component of an end-To-end system on the library. The library is publicly available through the Internet.

元の言語英語
ページ(範囲)251-266
ページ数16
ジャーナルAI Communications
31
発行部数3
DOI
出版物ステータス出版済み - 1 1 2018

Fingerprint

Benchmarking
Algebra
Number theory
Theorem proving
Internet
Geometry
Processing

All Science Journal Classification (ASJC) codes

  • Artificial Intelligence

これを引用

Can an A.I. win a medal in the mathematical olympiad?-Benchmarking mechanized mathematics on pre-university problems 1. / Matsuzaki, Takuya; Iwane, Hidenao; Kobayashi, Munehiro; Zhan, Yiyang; Fukasaku, Ryoya; Kudo, Jumma; Anai, Hirokazu; Arai, Noriko H.

:: AI Communications, 巻 31, 番号 3, 01.01.2018, p. 251-266.

研究成果: ジャーナルへの寄稿記事

Matsuzaki, Takuya ; Iwane, Hidenao ; Kobayashi, Munehiro ; Zhan, Yiyang ; Fukasaku, Ryoya ; Kudo, Jumma ; Anai, Hirokazu ; Arai, Noriko H. / Can an A.I. win a medal in the mathematical olympiad?-Benchmarking mechanized mathematics on pre-university problems 1. :: AI Communications. 2018 ; 巻 31, 番号 3. pp. 251-266.
@article{22c36ee7a28746cfaa53ec30b722f8df,
title = "Can an A.I. win a medal in the mathematical olympiad?-Benchmarking mechanized mathematics on pre-university problems 1",
abstract = "This paper introduces a benchmark problem library for mechanized mathematics including computer algebra and automated theorem proving. The library consists of pre-university mathematical problems taken from exercise problem books, university entrance examinations, and the International Mathematical Olympiads. The subject areas include real algebra, geometry, number theory, pre-calculus, calculus, and combinatorics. It thus includes problems in various areas of pre-university mathematics and with a variety of difficulty. Unlike other existing benchmark libraries, this one contains problems that are formalized so that they are obtainable as the result of mechanical translation of the original problems expressed in natural language. In other words, the library is designed to support the integration of the technologies of mechanized mathematics and natural language processing towards the goal of end-To-end automatic mathematical problem solving. The paper also presents preliminary experimental results of our prototype reasoning component of an end-To-end system on the library. The library is publicly available through the Internet.",
author = "Takuya Matsuzaki and Hidenao Iwane and Munehiro Kobayashi and Yiyang Zhan and Ryoya Fukasaku and Jumma Kudo and Hirokazu Anai and Arai, {Noriko H.}",
year = "2018",
month = "1",
day = "1",
doi = "10.3233/AIC-180762",
language = "English",
volume = "31",
pages = "251--266",
journal = "AI Communications",
issn = "0921-7126",
publisher = "IOS Press",
number = "3",

}

TY - JOUR

T1 - Can an A.I. win a medal in the mathematical olympiad?-Benchmarking mechanized mathematics on pre-university problems 1

AU - Matsuzaki, Takuya

AU - Iwane, Hidenao

AU - Kobayashi, Munehiro

AU - Zhan, Yiyang

AU - Fukasaku, Ryoya

AU - Kudo, Jumma

AU - Anai, Hirokazu

AU - Arai, Noriko H.

PY - 2018/1/1

Y1 - 2018/1/1

N2 - This paper introduces a benchmark problem library for mechanized mathematics including computer algebra and automated theorem proving. The library consists of pre-university mathematical problems taken from exercise problem books, university entrance examinations, and the International Mathematical Olympiads. The subject areas include real algebra, geometry, number theory, pre-calculus, calculus, and combinatorics. It thus includes problems in various areas of pre-university mathematics and with a variety of difficulty. Unlike other existing benchmark libraries, this one contains problems that are formalized so that they are obtainable as the result of mechanical translation of the original problems expressed in natural language. In other words, the library is designed to support the integration of the technologies of mechanized mathematics and natural language processing towards the goal of end-To-end automatic mathematical problem solving. The paper also presents preliminary experimental results of our prototype reasoning component of an end-To-end system on the library. The library is publicly available through the Internet.

AB - This paper introduces a benchmark problem library for mechanized mathematics including computer algebra and automated theorem proving. The library consists of pre-university mathematical problems taken from exercise problem books, university entrance examinations, and the International Mathematical Olympiads. The subject areas include real algebra, geometry, number theory, pre-calculus, calculus, and combinatorics. It thus includes problems in various areas of pre-university mathematics and with a variety of difficulty. Unlike other existing benchmark libraries, this one contains problems that are formalized so that they are obtainable as the result of mechanical translation of the original problems expressed in natural language. In other words, the library is designed to support the integration of the technologies of mechanized mathematics and natural language processing towards the goal of end-To-end automatic mathematical problem solving. The paper also presents preliminary experimental results of our prototype reasoning component of an end-To-end system on the library. The library is publicly available through the Internet.

UR - http://www.scopus.com/inward/record.url?scp=85047195529&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85047195529&partnerID=8YFLogxK

U2 - 10.3233/AIC-180762

DO - 10.3233/AIC-180762

M3 - Article

AN - SCOPUS:85047195529

VL - 31

SP - 251

EP - 266

JO - AI Communications

JF - AI Communications

SN - 0921-7126

IS - 3

ER -