Elamur Research⌕
☰
home / papers / 2024 / FormalAlign: Automated Alignment Evaluation for Autoformalization

FormalAlign: Automated Alignment Evaluation for Autoformalization

Paper · 2024 · Jianqiao Lu, Yingjia Wan, Yinya Huang et al.

Summary

Autoformalization uses models to turn informal mathematical statements into formal code such as Lean 4. A key weakness is evaluation. Compilers only confirm that the output is valid code, and BLEU or BERTscore only measure surface or embedding similarity. Neither checks whether the formal statement actually means the same thing as the original, so researchers still verify alignment by hand. The authors present FormalAlign, which they describe as the first framework for scoring informal–formal alignment automatically. An LLM is fine-tuned on two objectives at once. A cross-entropy loss trains it to generate the formalization. A contrastive loss on final-position hidden states pulls matching informal–formal pairs together and pushes mismatched pairs apart. At inference, the alignment score averages a certainty term and a similarity term. For testing, the authors built four benchmarks from MiniF2F and FormL4, adding deliberately misaligned formal statements. FormalAlign beats GPT-4 on these benchmarks and catches subtle errors that pass the compiler. This could substantially reduce manual checking in formal-math pipelines.

Key points

  • On FormL4-Basic, FormalAlign scores 99.21% Alignment-Selection versus 88.91% for GPT-4 and 93.65% precision versus 26.33%. On MiniF2F-Valid, its Alignment-Selection score is 66.39% versus 64.34%.
  • Training combines an autoformalization cross-entropy loss with a temperature-scaled contrastive loss (InfoNCE-style) computed over in-batch pairs.
  • The authors ran a human study on 80 sampled MiniF2F test items. Lean 4 experts averaged 79.58% correctness, FormalAlign reached 65.00%, and GPT-4o reached 47.50%. Inter-expert agreement was only moderate (Fleiss' κ = 0.49).
  • Each expert needed about 3 hours for the 80 items, while FormalAlign took under 2 minutes.
  • In a case study, the misaligned statements compiled without errors in Lean 4 and received high BLEU and BERTscore values. FormalAlign scored them all below a 0.7 threshold. The error types were missing conditions, wrong constants, variable type mismatches, equality changes and unpaired statements.
  • Code and data are available at github.com/rookie-joe/FormalAlign.

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

 Institutions

🎓University of CambridgeCambridge · United Kingdom243 works · 121,396 citations🏢Huawei TechnologiesShenzhen · China75 works · 12,975 citations🎓University of Hong KongPok Fu Lam · China89 works · 11,774 citations🎓City University of Hong KongHong Kong · China45 works · 3,014 citations

 Fields, topics and concepts

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 16,667 worksArtificial Intelligence · 16,194 worksArts and Humanities · 16,039 worksLanguage and Linguistics · 15,891 worksComputational Theory and Mathematics · 252 works

Cite

Cite as Jianqiao Lu, Yingjia Wan, Yinya Huang, Jing Xiong, Zhengying Liu and Zhijiang Guo. 2024. FormalAlign: Automated Alignment Evaluation for Autoformalization. arXiv:2410.10135.

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

@misc{lu2024formalalign,
  title = {{FormalAlign: Automated Alignment Evaluation for Autoformalization}},
  author = {Jianqiao Lu, Yingjia Wan, Yinya Huang, Jing Xiong, Zhengying Liu and Zhijiang Guo},
  year = {2024},
  doi = {10.48550/arxiv.2410.10135},
  eprint = {2410.10135},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2410.10135}
}

References

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

  1. 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.
  2. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. CoRR, abs/2302.12433, 2023a. doi: 10.48550/ARXIV.2302.12433. URL https://doi.org/10. 48550/arXiv.2302.12433.
  3. 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. CoRR, abs/2310.10631, 2023b. doi: 10.48550/ARXIV.2310.10631. URL https://doi.org/10.48550/arXiv.2310.… ↗
  4. Kshitij Bansal and Christian Szegedy. Learning alignment between formal & informal mathematics. In 5th Conference on Artificial Intelligence and Theorem Proving, 2020. find
  5. Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, Gérard P. Huet, César A. Muñoz, Chetan R. Murthy, Catherine Parent, Christine Paulin-Mohring, Amokrane Saïbi, and Benjamin Werner. The coq proof assistant : reference manual, ve… find
  6. Andrej Bauer, Matej Petkovic, and Ljupco Todorovski. MLFMF: data sets for machine learning for mathematical formalization. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine (eds.), Advances in Neural Information Processing Systems 36: Annual Conference on Neu… find
  7. Chi-Min Chan, Weize Chen, Yusheng Su, Jianxuan Yu, Wei Xue, Shanghang Zhang, Jie Fu, and Zhiyuan Liu. Chateval: Towards better llm-based evaluators through multi-agent debate. CoRR, abs/2308.07201, 2023. doi: 10.48550/ARXIV.2308.07201. URL https://doi.org/10.48550/ arXiv.2308.07201.
  8. Jiaqi Chen, Tong Li, Jinghui Qin, Pan Lu, Liang Lin, Chongyu Chen, and Xiaodan Liang. Unigeo: Unifying geometry logical reasoning via reformulating mathematical expression. In Yoav Goldberg, Zornitsa Kozareva, and Yue Zhang (eds.), Proceedings of the 2022 Conference on Empirical Methods in Natural L…
  9. Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Pondé de Oliveira Pinto, Jared Kaplan, Harrison Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder, Mik… — Evaluating Large Language Models Trained on Code
  10. Xinlei Chen, Hao Fang, Tsung-Yi Lin, Ramakrishna Vedantam, Saurabh Gupta, Piotr Dollár, and C. Lawrence Zitnick. Microsoft COCO captions: Data collection and evaluation server. CoRR, abs/1504.00325, 2015. URL http://arxiv.org/abs/1504.00325. ↗
  11. Aakanksha Chowdhery, Sharan Narang, Jacob Devlin, Maarten Bosma, Gaurav Mishra, Adam Roberts, Paul Barham, Hyung Won Chung, Charles Sutton, Sebastian Gehrmann, Parker Schuh, Kensen Shi, Sasha Tsvyashchenko, Joshua Maynez, Abhishek Rao, Parker Barnes, Yi Tay, Noam Shazeer, Vinodkumar Prabhakaran, Emi… — PaLM: Scaling Language Modeling with Pathways
  12. Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe (eds.), Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes…
  13. Springer, 2021. doi: 10.1007/ 978-3-030-79876-5\\_37. URL https://doi.org/10.1007/978-3-030-79876-5_37. — [doi:10.1007/978-3-030-79876-5_37](https://doi.org/10.1007/978-3-030-79876-5_37) ↗
  14. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp (eds.), Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7,… find
  15. Springer, 2015. doi: 10.1007/978-3-319-21401-6\\_26. URL https://doi.org/10.1007/978-3-319-21401-6_26. — [doi:10.1007/978-3-319-21401-6\\_26](https://doi.org/10.1007/978-3-319-21401-6_26) ↗
  16. Zorik Gekhman, Jonathan Herzig, Roee Aharoni, Chen Elkind, and Idan Szpektor. Trueteacher: Learning factual consistency evaluation with large language models. In Houda Bouamor, Juan Pino, and Kalika Bali (eds.), Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing,…
  17. John Harrison. HOL Light: A tutorial introduction. In Mandayam K. Srivas and Albert John Camilleri (eds.), Formal Methods in Computer-Aided Design, First International Conference, FMCAD ’96, Palo Alto, California, USA, November 6-8, 1996, Proceedings, volume 1166 of Lecture Notes in Computer Science… find
  18. Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin, Haiming Wang, Zhenguo Li, Linqi Song, and Xiaodan Liang. MUSTARD: Mastering uniform synthesis of theorem and proof data. In The Twelfth International Conference on Learning Representations, 2024. URL https://openreview.net/forum?id=… ↗
  19. Mojan Javaheripi, Sébastien Bubeck, Marah Abdin, Jyoti Aneja, Sebastien Bubeck, Caio César Teodoro Mendes, Weizhu Chen, Allie Del Giorno, Ronen Eldan, Sivakanth Gopi, et al. Phi-2: The surprising power of small language models. Microsoft Research Blog, 2023. find
  20. Albert Q. Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization. CoRR, abs/2311.03755, 2023a. doi: 10.48550/ARXIV.2311.03755. URL https://doi.org/10.48550/ arXiv.2311.03755. find
  21. Albert Q. Jiang, Alexandre Sablayrolles, Arthur Mensch, Chris Bamford, Devendra Singh Chaplot, Diego de Las Casas, Florian Bressand, Gianna Lengyel, Guillaume Lample, Lucile Saulnier, Lélio Renard Lavaud, Marie-Anne Lachaux, Pierre Stock, Teven Le Scao, Thibaut Lavril, Thomas Wang, Timothée Lacroix,… find
  22. Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothée 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, ICLR 2023,…
  23. OpenReview.net, 2023c. URL https://openreview.net/pdf?id=SMa9EAovKMC. ↗
  24. Cezary Kaliszyk, Josef Urban, Jirí Vyskocil, and Herman Geuvers. Developing corpus-based translation methods between informal and formal mathematics: Project description. CoRR, abs/1405.3451, 2014. URL http://arxiv.org/abs/1405.3451. — [arXiv:1405.3451](https://arxiv.org/abs/1405.3451) ↗
  25. Cezary Kaliszyk, Josef Urban, and Jirí Vyskocil. Automating formalization by statistical and semantic parsing of mathematics. In Mauricio Ayala-Rincón and César A. Muñoz (eds.), Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings… find
  26. Springer, 2017. doi: 10.1007/978-3-319-66107-0\\_2. URL https://doi.org/10.1007/978-3-319-66107-0_2. — [doi:10.1007/978-3-319-66107-0\\_2](https://doi.org/10.1007/978-3-319-66107-0_2) ↗
  27. Pei Ke, Bosi Wen, Zhuoer Feng, Xiao Liu, Xuanyu Lei, Jiale Cheng, Shengyuan Wang, Aohan Zeng, Yuxiao Dong, Hongning Wang, Jie Tang, and Minlie Huang. Critiquellm: Scaling llm-as-critic for effective and explainable evaluation of large language model generation. CoRR, abs/2311.18702, 2023. doi: 10.48…
  28. Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay V. Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. Solving quantitative reasoning problems with language models. In Sanmi Koyejo, S.…
  29. 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. CoRR, abs/2404.09939, 2024. doi: 10.48550/ARXIV.2404.09939. URL https://doi.org/10.48550/arXiv.2404.09939. ↗
  30. Chin-Yew Lin. ROUGE: A package for automatic evaluation of summaries. In Text Summarization Branches Out, pp. 74–81, Barcelona, Spain, July 2004. Association for Computational Linguistics. URL https://aclanthology.org/W04-1013. ↗
  31. Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, Ming Zhang, and Qun Liu. FIMO: A challenge formal dataset for automated theorem proving. CoRR, abs/2309.04295, 2023a. doi: 10.48550/ARXIV. 2309.04295. URL https://doi.org/10.485… find
  32. Minqian Liu, Ying Shen, Zhiyang Xu, Yixin Cao, Eunah Cho, Vaibhav Kumar, Reza Ghanadan, and Lifu Huang. X-eval: Generalizable multi-aspect text evaluation via augmented instruction tuning with auxiliary evaluation aspects. CoRR, abs/2311.08788, 2023b. doi: 10.48550/ARXIV.2311. 08788. URL https://doi… find
  33. Yang Liu, Dan Iter, Yichong Xu, Shuohang Wang, Ruochen Xu, and Chenguang Zhu. Gpteval: Nlg evaluation using gpt-4 with better human alignment. arXiv preprint arXiv:2303.16634, 2023c.
  34. Yinhong Liu, Han Zhou, Zhijiang Guo, Ehsan Shareghi, Ivan Vulic, Anna Korhonen, and Nigel Collier. Aligning with human judgement: The role of pairwise preference in large language model evaluators. CoRR, abs/2403.16950, 2024. doi: 10.48550/ARXIV.2403.16950. URL https://doi.org/10.48550/arXiv.2403.16… ↗
  35. Jianqiao Lu, Zhiyang Dou, Hongru Wang, Zeyu Cao, Jianbo Dai, Yingjia Wan, Yinya Huang, and Zhijiang Guo. Autocv: Empowering reasoning with automated process labeling via confidence variation. CoRR, abs/2405.16802, 2024a. doi: 10.48550/ARXIV.2405.16802. URL https://doi.org/10.48550/arXiv.2405.16802. ↗
  36. Jianqiao Lu, Zhengying Liu, Yingjia Wan, Yinya Huang, Haiming Wang, Zhicheng Yang, Jing Tang, and Zhijiang Guo. Process-driven autoformalization in lean 4. CoRR, abs/2406.01940, 2024b. doi: 10.48550/ARXIV.2406.01940. URL https://doi.org/10.48550/arXiv.2406.01940. ↗
  37. Jianqiao Lu, Wanjun Zhong, Yufei Wang, Zhijiang Guo, Qi Zhu, Wenyong Huang, Yanlin Wang, Fei Mi, Baojun Wang, Yasheng Wang, Lifeng Shang, Xin Jiang, and Qun Liu. YODA: teacher-student progressive learning for language models. CoRR, abs/2401.15670, 2024c. doi: 10.48550/ARXIV. 2401.15670. URL https://… — [doi:10.48550/arxiv](https://doi.org/10.48550/arxiv) find
  38. Shashi Narayan, Shay B. Cohen, and Mirella Lapata. Don’t give me the details, just the summary! topic-aware convolutional neural networks for extreme summarization. In Ellen Riloff, David Chiang, Julia Hockenmaier, and Jun’ichi Tsujii (eds.), Proceedings of the 2018 Conference on Empirical Methods i…
  39. OpenAI. GPT-3.5 Turbo, 2023. URL https://platform.openai.com/docs/models/gpt-3-5. ↗
  40. Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu. Bleu: a method for automatic evaluation of machine translation. In Proceedings of the 40th Annual Meeting of the Association for Computational Linguistics, July 6-12, 2002, Philadelphia, PA, USA, pp. 311–318.
  41. ACL, 2002. doi: 10.3115/1073083.1073135. URL https://aclanthology.org/P02-1040/. ↗
  42. Yiwei Qin, Weizhe Yuan, Graham Neubig, and Pengfei Liu. T5score: Discriminative fine-tuning of generative evaluation metrics. In Houda Bouamor, Juan Pino, and Kalika Bali (eds.), Findings of the Association for Computational Linguistics: EMNLP 2023, Singapore, December 6-10, 2023, pp. 15185–15202. A… find
  43. Piotr Rudnicki. An overview of the mizar project. 1992. URL https://api.semanticscholar.org/CorpusID:14378994. ↗
  44. Abigail See, Peter J. Liu, and Christopher D. Manning. Get to the point: Summarization with pointer-generator networks. In Regina Barzilay and Min-Yen Kan (eds.), Proceedings of the 55th Annual Meeting of the Association for Computational Linguistics, ACL 2017, Vancouver, Canada, July 30 - August 4,… find
  45. Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Mingchuan Zhang, Y. K. Li, Y. Wu, and Daya Guo. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. CoRR, abs/2402.03300, 2024a. doi: 10.48550/ARXIV.2402.03300. URL https://doi.org/10.48550/arXiv.2402.03300… ↗
  46. Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Mingchuan Zhang, Y. K. Li, Y. Wu, and Daya Guo. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. CoRR, abs/2402.03300, 2024b. doi: 10.48550/ARXIV.2402.03300. URL https://doi.org/10.48550/arXiv.2402.03300… ↗
  47. Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. In Christoph Benzmüller and Bruce R. Miller (eds.), Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings, volume 12236 of Lecture… find
  48. Springer, 2020. doi: 10.1007/978-3-030-53518-6\\_1. URL https://doi.org/10.1007/978-3-030-53518-6_1. — [doi:10.1007/978-3-030-53518-6\\_1](https://doi.org/10.1007/978-3-030-53518-6_1) ↗
  49. Haochen Tan, Zhijiang Guo, Zhan Shi, Lu Xu, Zhili Liu, Yunlong Feng, Xiaoguang Li, Yasheng Wang, Lifeng Shang, Qun Liu, and Linqi Song. Proxyqa: An alternative framework for evaluating long-form text generation with large language models. In Lun-Wei Ku, Andre Martins, and Vivek Srikumar (eds.), Proc…
  50. Hugo Touvron, Louis Martin, Kevin Stone, Peter Albert, Amjad Almahairi, Yasmine Babaei, Nikolay Bashlykov, Soumya Batra, Prajjwal Bhargava, Shruti Bhosale, Dan Bikel, Lukas Blecher, Cristian Canton-Ferrer, Moya Chen, Guillem Cucurull, David Esiobu, Jude Fernandes, Jeremy Fu, Wenyin Fu, Brian Fuller,… — Llama 2: Open Foundation and Fine-Tuned Chat Models
  51. Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. First experiments with neural translation of informal to formal mathematics. In Florian Rabe, William M. Farmer, Grant O. Passmore, and Abdou Youssef (eds.), Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Aust… find
  52. Springer, 2018. doi: 10.1007/978-3-319-96812-4\\_22. URL https://doi.org/10.1007/978-3-319-96812-4_22. — [doi:10.1007/978-3-319-96812-4\\_22](https://doi.org/10.1007/978-3-319-96812-4_22) ↗
  53. Yidong Wang, Zhuohao Yu, Zhengran Zeng, Linyi Yang, Cunxiang Wang, Hao Chen, Chaoya Jiang, Rui Xie, Jindong Wang, Xing Xie, Wei Ye, Shikun Zhang, and Yue Zhang. Pandalm: An automatic evaluation benchmark for LLM instruction tuning optimization. CoRR, abs/2306.05087, 2023. doi: 10.48550/ARXIV.2306.05…
  54. Tianwen Wei, Liang Zhao, Lichang Zhang, Bo Zhu, Lijie Wang, Haihua Yang, Biye Li, Cheng Cheng, Weiwei Lü, Rui Hu, Chenxia Li, Liu Yang, Xilin Luo, Xuejie Wu, Lunan Liu, Wenjun Cheng, Peng Cheng, Jianhao Zhang, Xiaoyu Zhang, Lei Lin, Xiaokun Wang, Yutuan Ma, Chuanhai Dong, Yanqi Sun, Yifu Chen, Yongy… — Skywork: A More Open Bilingual Foundation Model
  55. Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow. The isabelle framework. In Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar (eds.), Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, volume 5170 of Lect… find
  56. Springer, 2008. doi: 10.1007/978-3-540-71067-7\\_7. URL https://doi.org/10.1007/978-3-540-71067-7_7. — [doi:10.1007/978-3-540-71067-7\\_7](https://doi.org/10.1007/978-3-540-71067-7_7) ↗
  57. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh (eds.), Advances in Neural Information Processing Systems 35: A…
  58. Jing Xiong, Jianhao Shen, Ye Yuan, Haiming Wang, Yichun Yin, Zhengying Liu, Lin Li, Zhijiang Guo, Qingxing Cao, Yinya Huang, Chuanyang Zheng, Xiaodan Liang, Ming Zhang, and Qun Liu. TRIGO: benchmarking formal mathematical proof reduction for generative language models. In Houda Bouamor, Juan Pino, a… find
  59. Wenda Xu, Danqing Wang, Liangming Pan, Zhenqiao Song, Markus Freitag, William Wang, and Lei Li. INSTRUCTSCORE: towards explainable text generation evaluation with automatic feedback. In Houda Bouamor, Juan Pino, and Kalika Bali (eds.), Proceedings of the 2023 Conference on Empirical Methods in Natur…
  60. Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J. Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine (eds.…
  61. Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, Yudong Wang, Zijian Wu, Shuaibin Li, Fengzhe Zhou, Hongwei Liu, Songyang Zhang, Wenwei Zhang, Hang Yan, Xipeng Qiu, Jiayu Wang, Kai Chen, and Dahua Lin. Internlm-math: Open m… find
  62. Peter Young, Alice Lai, Micah Hodosh, and Julia Hockenmaier. From image descriptions to visual denotations: New similarity metrics for semantic inference over event descriptions. Trans. Assoc. Comput. Linguistics, 2:67–78, 2014. doi: 10.1162/TACL\\_A\\_00166. URL https://doi.org/ 10.1162/tacl_a_00166. find
  63. Weizhe Yuan, Graham Neubig, and Pengfei Liu. Bartscore: Evaluating generated text as text generation. In Marc’Aurelio Ranzato, Alina Beygelzimer, Yann N. Dauphin, Percy Liang, and Jennifer Wortman Vaughan (eds.), Advances in Neural Information Processing Systems 34: Annual Conference on Neural Infor…
  64. Xiang Yue, Boshi Wang, Ziru Chen, Kai Zhang, Yu Su, and Huan Sun. Automatic evaluation of attribution by large language models. In Houda Bouamor, Juan Pino, and Kalika Bali (eds.), Findings of the Association for Computational Linguistics: EMNLP 2023, Singapore, December 6-10, 2023, pp. 4615–4635. A… find
  65. Tianyi Zhang, Varsha Kishore, Felix Wu, Kilian Q. Weinberger, and Yoav Artzi. Bertscore: Evaluating text generation with BERT. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. find
  66. OpenReview.net, 2020a. URL https://openreview.net/forum?id=SkeHuCVFDr. ↗
  67. Tianyi Zhang, Varsha Kishore, Felix Wu, Kilian Q. Weinberger, and Yoav Artzi. Bertscore: Evaluating text generation with bert, 2020b. find
  68. Xiaokai Zhang, Na Zhu, Yiming He, Jia Zou, Qike Huang, Xiaoxiao Jin, Yanjun Guo, Chenyang Mao, Zhe Zhu, Dengfeng Yue, Fangzhen Zhu, Yang Li, Yifan Wang, Yiwen Huang, Runan Wang, Cheng Qin, Zhen Zeng, Shaorong Xie, Xiangfeng Luo, and Tuo Leng. Formalgeo: The first step toward human-like imo-level geo… — [arXiv:2310.18021](https://arxiv.org/abs/2310.18021) find
  69. Xueliang Zhao, Wenda Li, and Lingpeng Kong. Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving. CoRR, abs/2305.16366, 2023. doi: 10.48550/ARXIV.2305.16366. URL https://doi.org/10.48550/arXiv.2305.16366. ↗
  70. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022.
  71. OpenReview.net, 2022a. URL https://openreview.net/forum?id=9ZPegFuFTFv. ↗
  72. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022.
  73. OpenReview.net, 2022b. URL https://openreview.net/forum?id=9ZPegFuFTFv. ↗
  74. Lianmin Zheng, Wei-Lin Chiang, Ying Sheng, Siyuan Zhuang, Zhanghao Wu, Yonghao Zhuang, Zi Lin, Zhuohan Li, Dacheng Li, Eric P. Xing, Hao Zhang, Joseph E. Gonzalez, and Ion Stoica. Judging llm-as-a-judge with mt-bench and chatbot arena. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Morit…

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/lu-2024-formalalign-automated-alignment-evaluation-autoformalization/