A Promising Path Towards Autoformalization and General Artificial Intelligence
Integrity signals
Registry
Cites
Statistics
Claims the paper makes
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
There are multiple existing proof-of-concept solutions for various components of this reinforcement learning system, which suggests that a full solution may be realizable in the coming years.
“there are multiple existing proof-of-concept solutions for various components of this reinforcement learning system (Szegedy, 2020), which suggests that a full solution may be realizable in the coming years.”
From Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems (2024) · cites this paper as Szegedy, 2020
Cites
Deep Residual Learning for Image Recognition
He, K., Zhang, X., Ren, S., & Sun, J. (2016) · 2016 IEEE Conference on Computer Vision and Pattern Recognition (CVPR) · doi:10.1109/cvpr.2016.90 · Cited by 235,474 · see citing works
BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding
Devlin, J., Chang, M.-W., Lee, K., & Toutanova, K. (2019) · Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume 1 (Long and Short Papers) · doi:10.18653/v1/n19-1423 · Cited by 48,293 · see citing works
Deep Contextualized Word Representations
Peters, M., Neumann, M., Iyyer, M., Gardner, M., Clark, C., Lee, K., & Zettlemoyer, L. (2018) · Proceedings of the 2018 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume 1 (Long Papers) · doi:10.18653/v1/n18-1202 · Cited by 11,983 · see citing works
A general reinforcement learning algorithm that masters chess, shogi, and Go through self-play
Silver, D., Hubert, T., Schrittwieser, J., Antonoglou, I., Lai, M., Guez, A., Lanctot, M., Sifre, L., Kumaran, D., Graepel, T., et al. (2018) · Science · doi:10.1126/science.aar6404 · Cited by 3,562 · see citing works
Flagged first, then by citations
Cited by
Sorted by citations
Measuring Mathematical Problem Solving With the MATH Dataset
Hendrycks, D., Burns, C., Kadavath, S., Arora, A., Basart, S., Tang, E., Song, D., & Steinhardt, J. (2021) · arXiv · doi:10.48550/arxiv.2103.03874 · Cited by 306 · see citing works
Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems
Dalrymple, D. "., Skalse, J., Bengio, Y., Russell, S., Tegmark, M., Seshia, S., Omohundro, S., Szegedy, C., Goldhaber, B., Ammann, N., et al. (2024) · arXiv · doi:10.48550/arxiv.2405.06624 · Cited by 12 · see citing works
Self-citationProvably safe systems: the only path to controllable AGI
Tegmark, M., & Omohundro, S. (2023) · arXiv · doi:10.48550/arxiv.2309.01933 · Cited by 10 · see citing works
“Another reason to be bullish on ML for theorem proving is that autoformalization [89] and synthetically generated examples are likely to soon produce massive training datasets.”
BackgroundTowards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs
Cunningham, G., Bunescu, R. C., & Juedes, D. (2023) · arXiv · doi:10.48550/arxiv.2301.02195 · Cited by 10 · see citing works
- Authors
- Szegedy, C.
- Affiliations
- Google (United States) (US)
- Corresponding author
- Szegedy, Christian
- ORCID
- Szegedy, Christian
- Venue
- Lecture Notes in Computer Science
- Publisher
- Springer International Publishing
- Published
- 2020
- Pages
- 3-20
- ISSN
- 0302-9743 (ISSN-L)
- 1611-3349
- OpenAlex
- W3042499904
- Cited by
- 29
- References
- 4
- Citations by year
- 2026: 6 · 2025: 6 · 2024: 5 · 2023: 6 · 2022: 2 · 2021: 3 · 2020: 1
- FWCI
- 1.14
- Type
- conference paper
- Language
- en
- Open access
- closed
- Locations
- Lecture notes in computer science (publishedVersion)
- Topics
- Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Mathematics, Computing, and Information Processing
- Physical Sciences › Computer Science › Artificial Intelligence › Natural Language Processing Techniques
- Keywords
- autoformalization, formal verification, machine-checked proofs, automated reasoning, software synthesis, mathematical reasoning
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
