### 抄録

This paper introduces a benchmark problem library for mechanized math technologies including computer algebra and automated theorem proving. The library consists of pre-university math problems taken from exercise problem books, university entrance exams, and the International Mathematical Olympiads. It thus includes problems in various areas of pre-university math 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 math and natural language processing towards the goal of end-to-end automatic math 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.

元の言語 | 英語 |
---|---|

ホスト出版物のタイトル | Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings |

編集者 | Nicola Olivetti, Ashish Tiwari |

出版者 | Springer Verlag |

ページ | 213-227 |

ページ数 | 15 |

ISBN（印刷物） | 9783319402284 |

DOI | |

出版物ステータス | 出版済み - 1 1 2016 |

外部発表 | Yes |

イベント | 8th International Joint Conference on Automated Reasoning, IJCAR 2016 - Coimbra, ポルトガル 継続期間: 6 27 2016 → 7 2 2016 |

### 出版物シリーズ

名前 | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

巻 | 9706 |

ISSN（印刷物） | 0302-9743 |

ISSN（電子版） | 1611-3349 |

### 会議

会議 | 8th International Joint Conference on Automated Reasoning, IJCAR 2016 |
---|---|

国 | ポルトガル |

市 | Coimbra |

期間 | 6/27/16 → 7/2/16 |

### Fingerprint

### All Science Journal Classification (ASJC) codes

- Theoretical Computer Science
- Computer Science(all)

### これを引用

*Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings*(pp. 213-227). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻数 9706). Springer Verlag. https://doi.org/10.1007/978-3-319-40229-1_15

**Race against the teens – Benchmarking mechanized math on pre-university problems.** / Matsuzaki, Takuya; Iwane, Hidenao; Kobayashi, Munehiro; Zhan, Yiyang; Fukasaku, Ryoya; Kudo, Jumma; Anai, Hirokazu; Arai, Noriko H.

研究成果: 著書/レポートタイプへの貢献 › 会議での発言

*Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings.*Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 巻. 9706, Springer Verlag, pp. 213-227, 8th International Joint Conference on Automated Reasoning, IJCAR 2016, Coimbra, ポルトガル, 6/27/16. https://doi.org/10.1007/978-3-319-40229-1_15

}

TY - GEN

T1 - Race against the teens – Benchmarking mechanized math on pre-university problems

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 - 2016/1/1

Y1 - 2016/1/1

N2 - This paper introduces a benchmark problem library for mechanized math technologies including computer algebra and automated theorem proving. The library consists of pre-university math problems taken from exercise problem books, university entrance exams, and the International Mathematical Olympiads. It thus includes problems in various areas of pre-university math 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 math and natural language processing towards the goal of end-to-end automatic math 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 math technologies including computer algebra and automated theorem proving. The library consists of pre-university math problems taken from exercise problem books, university entrance exams, and the International Mathematical Olympiads. It thus includes problems in various areas of pre-university math 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 math and natural language processing towards the goal of end-to-end automatic math 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=84976638591&partnerID=8YFLogxK

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

U2 - 10.1007/978-3-319-40229-1_15

DO - 10.1007/978-3-319-40229-1_15

M3 - Conference contribution

AN - SCOPUS:84976638591

SN - 9783319402284

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 213

EP - 227

BT - Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings

A2 - Olivetti, Nicola

A2 - Tiwari, Ashish

PB - Springer Verlag

ER -