Elamur Research⌕
☰
home / papers / 2024 / Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency

Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency

Paper · 2024 · Zenan Li, Yifan Wu, Zhaoyu Li et al.

Summary

The paper addresses a weakness in LLM-based autoformalization, the task of turning natural-language math statements into formal theorems (here, Isabelle/HOL). A single sampled translation is often wrong, but among ten samples a correct one is frequently present. For GPT-4, the gap between pass@1 and pass@10 on MATH and miniF2F is about 20–27 points. The authors aim to pick the right candidate without training or test cases.

Their framework scores each of k candidates in two ways. Symbolic equivalence uses automated provers (Sledgehammer, Z3, CVC5) to group candidates that are logically equivalent despite different variable names. Semantic consistency back-translates each formal statement into natural language and compares its embedding with the original problem. Three schemes merge the two scores, and a log-based combination (log-comb) works best.

Across five LLMs, the method consistently improves top-1 selection, with relative gains of 0.22–1.35x over baselines. It also reduces the human effort needed to verify formalizations. This makes LLM output more reliable for building formal math corpora.

Key points

  • Pass@k gap: GPT-4's pass@1 vs. pass@10 gap on MATH and miniF2F ranges from 19.5% to 26.5%. This motivates training-free selection among candidates.
  • Models tested: Mistral-7B, Llemma-34B, DeepSeek-v2, Codex and GPT-4. With GPT-4, the combined method gains up to 7.8% (MATH) and 10.7% (miniF2F) over baselines. For Mistral-7B, log-comb adds 22.6% (MATH) and 10.5% (miniF2F) in 1@k accuracy over symbolic equivalence alone.
  • Labeling cost: Measured against the baseline, relative labeling efficiency reaches 8.4–21.9%. Log-comb gives 17.7–21.6% on MATH and 21.9% on miniF2F with GPT-4, outperforming Naïve and Cluster selection.
  • Difficulty and prover strength: Accuracy falls sharply for MATH difficulty levels 4–5. Restricting the prover to only auto and simp barely changes results, suggesting stronger ATPs add little.
  • Code and future work: Code and data are released at github.com/Miracle-Messi/Isa-AutoFormal. Proposed next steps include Lean 4 support, specialized models (ProofGPT, MMA) and synthesizing aligned informal–formal data.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang and Xiaoxing Ma. 2024. Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency. arXiv:2410.20936.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2410.20936 · arXiv 2410.20936

@misc{li2024autoformalize,
  title = {{Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency}},
  author = {Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang and Xiaoxing Ma},
  year = {2024},
  doi = {10.48550/arxiv.2410.20936},
  eprint = {2410.20936},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2410.20936}
}

References

74 references, 30 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. J Mc Carty and PJ Hayes. Some philosophical problems from the standpoint of artificial intelligence. d. michie (ed), machine intelligence 4, 1969. find
  2. Donald Simon. Checking natural language proofs. In International Conference on Automated Deduction, pages 141–150. Springer, 1988. find
  3. Cezary Kaliszyk, Josef Urban, Jiří Vyskočil, and Herman Geuvers. Developing corpus-based translation methods between informal and formal mathematics: Project description. In International Conference on Intelligent Computer Mathematics, 2014. find
  4. Cezary Kaliszyk, Josef Urban, and Jiří Vyskočil. Learning to parse on aligned corpora (rough diamond). In 6th International Conference on Interactive Theorem Proving, 2015. find
  5. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, et al. sel4: Formal verification of an os kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, pages 207–… find
  6. Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. Compcert-a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, 2016. find
  7. Georges Gonthier. The four colour theorem: Engineering of a formal proof. In Computer Mathematics: 8th Asian Symposium, ASCM 2007, Singapore, December 15-17, 2007. Revised and Invited Papers, pages 333–333. Springer, 2008. find
  8. Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al. A formal proof of the kepler conjecture. In Forum of mathematics, Pi, volume 5, page e2. Cambridge University Press, 2017.
  9. Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings 13, pages 3–20. Springer, 2020. find
  10. Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations, 2022.
  11. Jin Peng Zhou, Charles Staats, Wenda Li, Christian Szegedy, Kilian Q Weinberger, and Yuhuai Wu. Don’t trust: Verify–grounding llm quantitative reasoning with autoformalization. arXiv preprint arXiv:2403.18120, 2024.
  12. Emily First. Automating the formal verification of software. 2023. find
  13. Christopher Wang, Candace Ross, Yen-Ling Kuo, Boris Katz, and Andrei Barbu. Learning a natural-language to ltl executable semantic parser for grounded robotics. In Conference on Robot Learning, pages 1706–1718. PMLR, 2021. find
  14. Roma Patel, Roma Pavlick, and Stefanie Tellex. Learning to ground language to temporal logical form. In Conference of the North American Chapter of the Association for Computational Linguistics (NAACL), 2019. find
  15. Martin D. Fraser, Kuldeep Kumar, and Vijay K. Vaishnavi. Informal and formal requirements specification languages: bridging the gap. IEEE transactions on Software Engineering, 17(5): 454, 1991. find
  16. Alessandro Fantechi, Stefania Gnesi, Gioia Ristori, Michele Carenini, Massimo Vanocchi, and Paolo Moreschini. Assisting requirement formalization by means of natural language translation. Formal Methods in System Design, 4:243–263, 1994. find
  17. Claire Grover, Alexander Holt, Ewan Klein, and Marc Moens. Designing a controlled language for interactive model checking. In Proceedings of the third international workshop on controlled language applications, pages 29–30. Citeseer, 2000. find
  18. Tobias Kuhn. A survey and classification of controlled natural languages. Computational linguistics, 40(1):121–170, 2014. find
  19. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. Advances in Neural Information Processing Systems, 35:32353–32368, 2022.
  20. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433, 2023.
  21. Albert Q Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization. arXiv preprint arXiv:2311.03755, 2023.
  22. Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al. Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374, 2021.
  23. Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. In Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 2), 2021.
  24. Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. GPT-4 technical report. arXiv preprint arXiv:2303.08774, 2023.
  25. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations, 2021.
  26. Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc V Le, Ed H Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. Self-consistency improves chain of thought reasoning in language models. In The Eleventh International Conference on Learning Representations, 2022.
  27. Bei Chen, Fengji Zhang, Anh Nguyen, Daoguang Zan, Zeqi Lin, Jian-Guang Lou, and Weizhu Chen. Codet: Code generation with generated tests. arXiv preprint arXiv:2207.10397, 2022. find
  28. Sascha Böhme and Tobias Nipkow. Sledgehammer: judgement day. In Automated Reasoning: 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings 5, pages 107–121. Springer, 2010. find
  29. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340. Springer, 2008. find
  30. Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, et al. cvc5: A versatile and industrial-strength smt solver. In International Conference on Tools and Algorithms for the Construction and Analysi…
  31. Sergey Edunov, Myle Ott, Michael Auli, and David Grangier. Understanding back-translation at scale. arXiv preprint arXiv:1808.09381, 2018. find
  32. Lawrence C Paulson. Isabelle: A generic theorem prover. Springer, 1994. find
  33. Yves Bertot and Pierre Castéran. Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Springer Science & Business Media, 2013. find
  34. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pages 378–388. Springer, 2015. find
  35. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, et al. A machine-checked proof of the odd order theorem. In International conference on interactive theorem proving, pages 163–179. Spring… find
  36. Kevin Buzzard, Johan Commelin, and Patrick Massot. Formalising perfectoid spaces. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 299–312, 2020.
  37. Peter Scholze. Liquid tensor experiment. Experimental Mathematics, 31(2):349–354, 2022. find
  38. Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey on deep learning for theorem proving. arXiv preprint arXiv:2404.09939, 2024.
  39. Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan, and Anand Tadipatri. Towards a mathematics formalisation assistant using large language models. arXiv preprint arXiv:2211.07524, 2022.
  40. Siddhartha Gadgil, Anand Rao Tadipatri, Ayush Agrawal, Ashvni Narayanan, and Navin Goyal. Towards automating formalisation of theorem statements using large language models. In 36th Conference on Neural Information Processing Systems Workshop on MATH-AI, 2022. find
  41. Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, et al. Fimo: A challenge formal dataset for automated theorem proving. arXiv preprint arXiv:2309.04295, 2023.
  42. Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. SATLM: Satisfiability-aided language models using declarative prompting. In Proceedings of the 37th International Conference on Neural Information Processing Systems, 2023.
  43. Xueliang Zhao, Wenda Li, and Lingpeng Kong. Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving. arXiv preprint arXiv:2305.16366, 2023.
  44. Chuanyang Zheng, Haiming Wang, Enze Xie, Zhengying Liu, Jiankai Sun, Huajian Xin, Jianhao Shen, Zhenguo Li, and Yu Li. Lyra: Orchestrating dual correction in automated theorem proving. arXiv preprint arXiv:2309.15806, 2023.
  45. Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics. arXiv preprint arXiv:2310.10631, 2023.
  46. Huajian Xin, Haiming Wang, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, et al. LEGO-prover: Neural theorem proving with growing libraries. In The Twelfth International Conference on Learning Representations, 2024.
  47. Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Mingchuan Zhang, YK Li, Y Wu, and Daya Guo. DeepSeekMath: Pushing the limits of mathematical reasoning in open language models. arXiv preprint arXiv:2402.03300, 2024.
  48. Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, et al. InternLM-Math: Open math large language models toward verifiable reasoning. arXiv preprint arXiv:2402.06332, 2024.
  49. Xinyun Chen, Renat Aksitov, Uri Alon, Jie Ren, Kefan Xiao, Pengcheng Yin, Sushant Prakash, Charles Sutton, Xuezhi Wang, and Denny Zhou. Universal self-consistency for large language model generation. arXiv preprint arXiv:2311.17311, 2023.
  50. Denny Zhou, Nathanael Schärli, Le Hou, Jason Wei, Nathan Scales, Xuezhi Wang, Dale Schuurmans, Claire Cui, Olivier Bousquet, Quoc Le, et al. Least-to-most prompting enables complex reasoning in large language models. arXiv preprint arXiv:2205.10625, 2022.
  51. Angelica Chen, Jason Phang, Alicia Parrish, Vishakh Padmakumar, Chen Zhao, Samuel R Bowman, and Kyunghyun Cho. Two failures of self-consistency in the multi-step reasoning of llms. arXiv preprint arXiv:2305.14279, 2023.
  52. Furui Cheng, Vilém Zouhar, Simran Arora, Mrinmaya Sachan, Hendrik Strobelt, and Mennatallah El-Assady. Relic: Investigating large language model responses using self-consistency. In Proceedings of the CHI Conference on Human Factors in Computing Systems, pages 1–18, 2024. find
  53. Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, et al. Training verifiers to solve math word problems. arXiv preprint arXiv:2110.14168, 2021.
  54. Romal Thoppilan, Daniel De Freitas, Jamie Hall, Noam Shazeer, Apoorv Kulshreshtha, Heng-Tze Cheng, Alicia Jin, Taylor Bos, Leslie Baker, Yu Du, et al. Lamda: Language models for dialog applications. arXiv preprint arXiv:2201.08239, 2022.
  55. Shen Zheng, Yuyu Zhang, Yijie Zhu, Chenguang Xi, Pengyang Gao, Xun Zhou, and Kevin Chen-Chuan Chang. Gpt-fathom: Benchmarking large language models to decipher the evolutionary path towards gpt-4 and beyond. arXiv preprint arXiv:2309.16583, 2023. find
  56. Baizhou Huang, Shuai Lu, Weizhu Chen, Xiaojun Wan, and Nan Duan. Enhancing large language models in coding through multi-perspective self-consistency. arXiv preprint arXiv:2309.17272, 2023. find
  57. Marcus J Min, Yangruibo Ding, Luca Buratti, Saurabh Pujar, Gail Kaiser, Suman Jana, and Baishakhi Ray. Beyond accuracy: Evaluating self-consistency of code llms. In The Twelfth International Conference on Learning Representations, 2023. find
  58. Kexun Zhang, Danqing Wang, Jingtao Xia, William Yang Wang, and Lei Li. Algo: Synthesizing algorithmic programs with generated oracle verifiers. Advances in Neural Information Processing Systems, 36, 2024. find
  59. Harold Neil Gabow. Implementation of algorithms for maximum matching on nonbipartite graphs. Stanford University, 1974. find
  60. Yanyan Jiang and Chang Xu. Needle: Detecting code plagiarism on student submissions. In Proceedings of ACM Turing Celebration Conference-China, pages 27–32, 2018. find
  61. Li Yujian and Liu Bo. A normalized levenshtein distance metric. IEEE transactions on pattern analysis and machine intelligence, 29(6):1091–1095, 2007. find
  62. Gonzalo Navarro. A guided tour to approximate string matching. ACM computing surveys (CSUR), 33(1):31–88, 2001. find
  63. Tom Kenter and Maarten De Rijke. Short text similarity with word embeddings. In Proceedings of the 24th ACM international on conference on information and knowledge management, pages 1411–1420, 2015. find
  64. Omid Shahmirzadi, Adam Lugowski, and Kenneth Younge. Text similarity in vector space models: a comparative study. In 2019 18th IEEE international conference on machine learning and applications (ICMLA), pages 659–666. IEEE, 2019. find
  65. Felix Hill, Kyunghyun Cho, Sebastien Jean, Coline Devin, and Yoshua Bengio. Embedding word similarity with neural machine translation. arXiv preprint arXiv:1412.6448, 2014. find
  66. Raj Dabre, Chenhui Chu, and Anoop Kunchukuttan. A survey of multilingual neural machine translation. ACM Computing Surveys (CSUR), 53(5):1–38, 2020. find
  67. Felix Stahlberg. Neural machine translation: A review. Journal of Artificial Intelligence Research, 69:343–418, 2020. find
  68. Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. Bert: Pre-training of deep bidirectional transformers for language understanding. arXiv preprint arXiv:1810.04805, 2018.
  69. Albert Q Jiang, Alexandre Sablayrolles, Arthur Mensch, Chris Bamford, Devendra Singh Chaplot, Diego de las Casas, Florian Bressand, Gianna Lengyel, Guillaume Lample, Lucile Saulnier, et al. Mistral 7b. arXiv preprint arXiv:2310.06825, 2023. find
  70. DeepSeek-AI. Deepseek-v2: A strong, economical, and efficient mixture-of-experts language model, 2024. find
  71. Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. Gpt-4 technical report. arXiv preprint arXiv:2303.08774, 2023.
  72. Sanjiv K Bhatia et al. Adaptive k-means clustering. In FLAIRS, pages 695–699, 2004. find
  73. Dominique Unruh. Scala/Isabelle: A library for accessing Isabelle from Scala. https://github.com/dominique-unruh/scala-isabelle, 2023. Accessed: 2024-01-30. ↗
  74. Jasmin Christian Blanchette and Lawrence C Paulson. Hammering away. A User’s Guide to Sledgehammer for Isabelle/HOL. url: http://isabelle.in. tum. de/dist/Isabelle2013-2/doc/sledgehammer. pdf, 2013. ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/li-2024-autoformalize-mathematical-statements-symbolic-equivalence/