A Promising Path Towards Autoformalization and General Artificial Intelligence

By Christian Szegedy. 2020

88 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Information Systems, Natural Language Processing, Prompting & Reasoning

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

1. Yejin Choi
2. Percy Liang
3. Hannaneh Hajishirzi
4. Luke S. Zettlemoyer
5. Mohit Bansal
6. Sean Welleck
7. Jianfeng Gao
8. Dawn Song

In Information Systems

1. Wenda Li
2. Sean Welleck
3. Yuhuai Wu
4. Albert Qiaochu Jiang
5. Lawrence Charles Paulson
6. Lei Yu
7. Zhangir Azerbayev
8. Jiacheng Liu

In Natural Language Processing

1. Yejin Choi
2. Hannaneh Hajishirzi
3. Sean Welleck
4. Ximing Lu
5. Luke S. Zettlemoyer
6. Mohit Bansal
7. Markus Norman Rabe
8. Dragomir R. Radev

In Prompting & Reasoning

1. Sean Welleck
2. Yuhuai Wu
3. Wenda Li
4. Markus Norman Rabe
5. Hannaneh Hajishirzi
6. Edward W. Ayers
7. Jiacheng Liu
8. Lawrence Charles Paulson

Citations in the corpus

• Measuring Mathematical Problem Solving With the MATH Dataset (2021, background): “We address Szegedy (2020)’s concern by creating a dataset to test understanding of mathematics written in natural language and commonplace mathematical notation.”
• Autoformalization with Large Language Models (2022, background): “Autoformalization refers to the task of automatically translating from natural language mathematics to a formal language [46, 42].”
• Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs (2022, background): “Autoformalization In a position paper, Szegedy (2020) argued for attaining formal mathematical data from informal sources with neural networks.”
• ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics (2023, background): “…, the task of automatically formalizing mathematics, seeks to build a bridge be-tween informal and formal mathematical reasoning [Wang et al., 2018, Szegedy, 2020, Wu et al., 2022a], with the potential of extracting a training signal from vast corpora of natural language mathematics data while…”
• NaturalProver: Grounded Mathematical Proof Generation with Language Models (2022, background): “From Point is Open iff it is not Dense-in-itself , it follows that { x } is not dense-in-itself.”
• IsarStep: a Benchmark for High-level Mathematical Reasoning (2021, methodology): “, 2020a), proof method recommendations (Nagashima, 2020; Nagashima & He, 2018), and autoformalisation of mathematics (Wang et al., 2020; Szegedy, 2020).”