Exploration of Neural Machine Translation in Autoformalization of
Mathematics in Mizar

Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar

5 December 2019

Papers citing "Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar"

14 / 14 papers shown

Title
Hierarchical Attention Generates Better Proofs Jianlong Chen Chao Li Yang Yuan Andrew Chi-Chih Yao AIMat LRM 33 0 0 27 Apr 2025
ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data Xiaoyang Liu Kangjie Bao Jiashuo Zhang Yunqi Liu Yu Chen Yu Chen Yang Jiao Tao Luo AIMat 57 0 0 08 Feb 2025
ZIP-FIT: Embedding-Free Data Selection via Compression-Based Alignment Elyas Obbad Iddah Mlauzi Brando Miranda Rylan Schaeffer Kamal Obbad Suhana Bedi Sanmi Koyejo CVBM 65 0 0 23 Oct 2024
Can Transformers Do Enumerative Geometry? Baran Hashemi Roderic G. Corominas Alessandro Giacchetto 49 2 0 27 Aug 2024
Lean-STaR: Learning to Interleave Thinking and Proving Haohan Lin Zhiqing Sun Yiming Yang Sean Welleck ReLM LRM 75 26 0 14 Jul 2024
Using Large Language Models for (De-)Formalization and Natural Argumentation Exercises for Beginner's Students M. Carl LRM 24 1 0 12 Apr 2023
Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs Garett Cunningham Razvan C. Bunescu D. Juedes LRM 23 16 0 05 Jan 2023
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs Albert Q. Jiang Sean Welleck Jin Peng Zhou Wenda Li Jiacheng Liu M. Jamnik Timothée Lacroix Yuhuai Wu Guillaume Lample AIMat 75 160 0 21 Oct 2022
Memorizing Transformers Yuhuai Wu M. Rabe DeLesley S. Hutchins Christian Szegedy RALM 30 173 0 16 Mar 2022
A Survey on Artificial Intelligence for Source Code: A Dialogue Systems Perspective Erfan Al-Hossami Samira Shaikh 32 6 0 10 Feb 2022
Proof Artifact Co-training for Theorem Proving with Language Models Jesse Michael Han Jason M. Rute Yuhuai Wu Edward W. Ayers Stanislas Polu AIMat 30 121 0 11 Feb 2021
LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning Yuhuai Wu M. Rabe Wenda Li Jimmy Ba Roger C. Grosse Christian Szegedy AIMat LRM 82 53 0 15 Jan 2021
IsarStep: a Benchmark for High-level Mathematical Reasoning Wenda Li Lei Yu Yuhuai Wu Lawrence Charles Paulson AIMat LRM 26 10 0 13 Jun 2020
Effective Approaches to Attention-based Neural Machine Translation Thang Luong Hieu H. Pham Christopher D. Manning 220 7,930 0 17 Aug 2015