Elamur Research⌕
☰
home / papers / 2023 / Evaluating Language Models for Mathematics through Interactions

Evaluating Language Models for Mathematics through Interactions

Paper · 2023 · Katherine M. Collins, Albert Q. Jiang, Simon Frieder et al.

Summary

Standard LLM benchmarks compare a single model output with a fixed reference answer. That approach says little about how useful a model is when a person works with it over several turns. The authors argue that assistant-style use needs interactive evaluation. They test this on informal proofs of undergraduate mathematics, where correctness is strict but automatic scores such as BLEU or ROUGE cannot judge quality.

They built CheckMate, a lightweight, adaptable platform in which users chat with a model and grade every reply for correctness and helpfulness. Participants ranging from students to mathematics professors used it to tackle ProofWiki problems with InstructGPT, ChatGPT and GPT-4. This produced the MathConverse dataset. From these logs the team coded a taxonomy of user behaviours, and three expert mathematicians ran in-depth case studies with GPT-4.

Correctness and perceived helpfulness usually go together but sometimes diverge. The models struggle with algebra, tend to be wordy, and lean on memorised solutions. The study shows that interactive, expert-involved evaluation is feasible and informative for judging when LLM assistants can be trusted.

Key points

  • Resources: CheckMate is an open interactive evaluation platform that can be extended beyond mathematics. MathConverse is the released dataset of 261 rated human–model interactions.
  • Models and ranking: The study compared InstructGPT, ChatGPT and GPT-4. GPT-4 performed best overall and was therefore chosen for the expert case studies.
  • Taxonomy: User queries were sorted into 10 behaviour categories plus an "Other" bucket. Four authors did the annotation and resolved unclear cases through discussion.
  • Expert case studies: William Hart (number theory), Wenda Li (formal mathematics) and Fields medalist Timothy Gowers examined memorisation via problem perturbation. They also probed where GPT-4's easy problems end and hard ones begin.
  • Recommendations:
    • Developers should build assistants that convey uncertainty, accept user corrections, and stay concise and interpretable.
    • Users should check outputs carefully, because mistakes can be subtle.

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

🎓New York UniversityNew York · United States233 works · 104,003 citations🎓University of CambridgeCambridge · United Kingdom287 works · 125,174 citations🎓University of OxfordOxford · United Kingdom138 works · 161,448 citations🔬The Alan Turing InstituteLondon · United Kingdom35 works · 5,111 citations🎓TU WienVienna · Austria10 works · 943 citations🎓Collège de FranceParis · France4 works · 65 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksInformation Systems · 1,888 works

🧭 Topics 2Research subjects and languages the work is about.Language models & pretraining · 4,145 worksEvaluation & benchmarks · 1,394 works

Cite

Cite as Katherine M. Collins, Albert Q. Jiang, Simon Frieder, Lionel Wong, Miri Zilka, Umang Bhatt, Thomas Lukasiewicz, Yuhuai Wu, Joshua B. Tenenbaum, William Hart, Timothy Gowers, Wenda Li, Adrian Weller and Mateja Jamnik. 2023. Evaluating Language Models for Mathematics through Interactions. arXiv:2306.01694.

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

@misc{collins2023evaluating,
  title = {{Evaluating Language Models for Mathematics through Interactions}},
  author = {Katherine M. Collins, Albert Q. Jiang, Simon Frieder, Lionel Wong, Miri Zilka, Umang Bhatt, Thomas Lukasiewicz, Yuhuai Wu, Joshua B. Tenenbaum, William Hart, Timothy Gowers, Wenda Li, Adrian Weller and Mateja Jamnik},
  year = {2023},
  doi = {10.48550/arxiv.2306.01694},
  eprint = {2306.01694},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2306.01694}
}

References

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

  1. A. Abid, A. Abdalla, A. Abid, D. Khan, A. Alfozan, and J. Zou. Gradio: Hassle-Free Sharing and Testing of ML Models in the Wild. arXiv preprint arXiv:1906.02569, 2019. — [arXiv:1906.02569](https://arxiv.org/abs/1906.02569) find
  2. J. S. Aitken, P. Gray, T. Melham, and M. Thomas. Interactive theorem proving: An empirical study of user activity. Journal of Symbolic Computation, 25(2):263–284, 1998. find
  3. A. F. Akyürek, E. Akyürek, A. Madaan, A. Kalyan, P. Clark, D. Wijaya, and N. Tandon. RL4F: Generating Natural Language Feedback with Reinforcement Learning for Repairing Model Outputs. arXiv preprint arXiv:2305.08844, 2023.
  4. A. Amini, S. Gabriel, S. Lin, R. Koncel-Kedziorski, Y. Choi, and H. Hajishirzi. Mathqa: Towards interpretable math word problem solving with operation-based formalisms. In J. Burstein, C. Doran, and T. Solorio, editors, Proceedings of the 2019 Conference of the North American Chapter of the Associat…
  5. R. Anil, A. M. Dai, O. Firat, M. Johnson, D. Lepikhin, A. Passos, S. Shakeri, E. Taropa, P. Bailey, Z. Chen, E. Chu, J. H. Clark, L. E. Shafey, Y. Huang, K. Meier-Hellstern, G. Mishra, E. Moreira, M. Omernick, K. Robinson, S. Ruder, Y. Tay, K. Xiao, Y. Xu, Y. Zhang, G. H. Abrego, J. Ahn, J. Austin,… — PaLM 2 Technical Report
  6. J. W. Ayers, A. Poliak, M. Dredze, E. C. Leas, Z. Zhu, J. B. Kelley, D. J. Faix, A. M. Goodman, C. A. Longhurst, M. Hogarth, and D. M. Smith. Comparing Physician and Artificial Intelligence Chatbot Responses to Patient Questions Posted to a Public Social Media Forum. JAMA Internal Medicine, 04 2023.… — [doi:10.1001/jamainternmed.2023.1838](https://doi.org/10.1001/jamainternmed.2023.1838) find
  7. R. Azamfirei, S. R. Kudchadkar, and J. Fackler. Large language models and the perils of their hallucinations. Critical Care, 27(1):1–2, 2023. find
  8. J. Ba and B. Wang. Csc413/2516 winter 2023 university of toronto, assignment 1, 2023. URL https://uoft-csc413.github.io/2023/assets/assignments/a1.pdf. ↗
  9. B. Beckert, S. Grebing, and F. Böhl. A usability evaluation of interactive theorem provers using focus groups. In Software Engineering and Formal Methods: SEFM 2014 Collocated Workshops: HOFM, SAFOME, OpenCert, MoKMaSD, WS-FMDS, Grenoble, France, September 1-2, 2014, Revised Selected Papers 12, page… find
  10. E. M. Bender, T. Gebru, A. McMillan-Major, and S. Shmitchell. On the dangers of stochastic parrots: Can language models be too big? In Proceedings of the 2021 ACM conference on fairness, accountability, and transparency, pages 610–623, 2021a. find
  11. E. M. Bender, T. Gebru, A. McMillan-Major, and S. Shmitchell. On the dangers of stochastic parrots: Can language models be too big? In Proceedings of the 2021 ACM Conference on Fairness, Accountability, and Transparency, FAccT ’21, page 610–623, New York, NY, USA, 2021b. Association for Computing Ma… — [doi:10.1145/3442188.3445922](https://doi.org/10.1145/3442188.3445922) find
  12. U. Bhatt, A. Xiang, S. Sharma, A. Weller, A. Taly, Y. Jia, J. Ghosh, R. Puri, J. M. Moura, and P. Eckersley. Explainable machine learning in deployment. In Proceedings of the 2020 conference on fairness, accountability, and transparency, pages 648–657, 2020. find
  13. U. Bhatt, J. Antorán, Y. Zhang, Q. V. Liao, P. Sattigeri, R. Fogliato, G. Melançon, R. Krishnan, J. Stanley, O. Tickoo, et al. Uncertainty as a form of transparency: Measuring, communicating, and using uncertainty. In Proceedings of the 2021 AAAI/ACM Conference on AI, Ethics, and Society, pages 401–… find
  14. U. Bhatt, V. Chen, K. M. Collins, P. Kamalaruban, E. Kallina, A. Weller, and A. Talwalkar. Learning personalized decision support policies. arXiv e-prints, pages arXiv–2304, 2023. find
  15. P. A. Bishop and R. L. Herron. Use and misuse of the likert item responses and other ordinal measures. International journal of exercise science, 8(3):297, 2015. find
  16. W. W. Bledsoe. Non-resolution theorem proving. Artif. Intell., 9:1–35, 1977. find
  17. R. Bommasani, D. A. Hudson, E. Adeli, R. Altman, S. Arora, S. von Arx, M. S. Bernstein, J. Bohg, A. Bosselut, E. Brunskill, et al. On the opportunities and risks of foundation models. arXiv preprint arXiv:2108.07258, 2021.
  18. T. Brown, B. Mann, N. Ryder, M. Subbiah, J. D. Kaplan, P. Dhariwal, A. Neelakantan, P. Shyam, G. Sastry, A. Askell, et al. Language models are few-shot learners. NeurIPS, 33:1877–1901, 2020.
  19. S. Bubeck, V. Chandrasekaran, R. Eldan, J. Gehrke, E. Horvitz, E. Kamar, P. Lee, Y. T. Lee, Y. Li, S. Lundberg, H. Nori, H. Palangi, M. T. Ribeiro, and Y. Zhang. Sparks of artificial general intelligence: Early experiments with gpt-4, 2023.
  20. A. Bundy. The Computer Modelling of Mathematical Reasoning. Academic Press, 1983. find
  21. A. Bundy. The use of explicit plans to guide inductive proofs. In CADE, 1988. find
  22. A. Bundy, A. Stevens, F. V. Harmelen, A. Ireland, and A. Smaill. Rippling: A heuristic for guiding inductive proofs. Artif. Intell., 62:185–253, 1993. find
  23. R. Burnell, W. Schellaert, J. Burden, T. D. Ullman, F. Martinez-Plumed, J. B. Tenenbaum, D. Rutar, L. G. Cheke, J. Sohl-Dickstein, M. Mitchell, D. Kiela, M. Shanahan, E. M. Voorhees, A. G. Cohn, J. Z. Leibo, and J. Hernandez-Orallo. Rethink reporting of evaluation results in ai. Science, 380(6641):1… find
  24. S. Casper, X. Davies, C. Shi, T. Krendl Gilbert, J. Scheurer, J. Rando, R. Freedman, T. Korbak, D. Lindner, P. Freire, et al. Open problems and fundamental limitations of reinforcement learning from human feedback. arXiv e-prints, pages arXiv–2307, 2023. find
  25. P. F. Christiano, J. Leike, T. Brown, M. Martic, S. Legg, and D. Amodei. Deep reinforcement learning from human preferences. Advances in neural information processing systems, 30, 2017. find
  26. E. Clark, A. S. Ross, C. Tan, Y. Ji, and N. A. Smith. Creative writing with a machine in the loop: Case studies on slogans and stories. In Proceedings of IUI, 2018. find
  27. K. Cobbe, V. Kosaraju, M. Bavarian, J. Hilton, R. Nakano, C. Hesse, and J. Schulman. Training verifiers to solve math word problems. CoRR, abs/2110.14168, 2021. URL https://arxiv.org/abs/2110.14168. ↗
  28. A. G. Cohn and J. Hernandez-Orallo. Dialectical language model evaluation: An initial appraisal of the commonsense spatial reasoning abilities of llms. arXiv preprint arXiv:2304.11164, 2023. find
  29. M. L. Cummings. Automation bias in intelligent time critical decision support systems. In AIAA 1st Intelligent Systems Technical Conference, 2004. URL https://api.semanticscholar.org/CorpusID:10328335. ↗
  30. A. Davies, P. Veličković, L. Buesing, S. Blackwell, D. Zheng, N. Tomašev, R. Tanburn, P. Battaglia, C. Blundell, A. Juhász, et al. Advancing mathematics by guiding human intuition with ai. Nature, 600(7887):70–74, 2021. find
  31. M. Davis, G. Logemann, and D. Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394–397, 1962. find
  32. L. M. de Moura and N. S. Bjørner. Z3: An efficient smt solver. In International Conference on Tools and Algorithms for Construction and Analysis of Systems, 2008. find
  33. D. Delahaye. A tactic language for the system coq. In M. Parigot and A. Voronkov, editors, Logic for Programming and Automated Reasoning, 7th International Conference, LPAR 2000, Reunion Island, France, November 11-12, 2000, Proceedings, volume 1955 of Lecture Notes in Computer Science, pages 85–95. find
  34. Springer, 2000. doi: 10.1007/3-540-44404-1\\_7. URL https://doi.org/10.1007/3-540-44404-1_7. — [doi:10.1007/3-540-44404-1\\_7](https://doi.org/10.1007/3-540-44404-1_7) ↗
  35. D. Dohan, W. Xu, A. Lewkowycz, J. Austin, D. Bieber, R. G. Lopes, Y. Wu, H. Michalewski, R. A. Saurous, J. Sohl-Dickstein, et al. Language model cascades. ICML, 2022.
  36. N. Dziri, X. Lu, M. Sclar, X. L. Li, L. Jian, B. Y. Lin, P. West, C. Bhagavatula, R. L. Bras, J. D. Hwang, et al. Faith and fate: Limits of transformers on compositionality. arXiv preprint arXiv:2305.18654, 2023.
  37. A. P. Felty. Implementing tactics and tacticals in a higher-order logic programming language. J. Autom. Reason., 11(1):41–81, 1993. doi: 10.1007/BF00881900. URL https://doi.org/10.1007/BF00881900. — [doi:10.1007/bf00881900](https://doi.org/10.1007/bf00881900) ↗
  38. E. First, M. N. Rabe, T. Ringer, and Y. Brun. Baldur: Whole-proof generation and repair with large language models. CoRR, abs/2303.04910, 2023. doi: 10.48550/arXiv.2303.04910. URL https://doi.org/ 10.48550/arXiv.2303.04910.
  39. S. Frieder, L. Pinchetti, R.-R. Griffiths, T. Salvatori, T. Lukasiewicz, P. C. Petersen, A. Chevalier, and J. Berner. Mathematical Capabilities of ChatGPT, 2023.
  40. M. Ganesalingam and W. T. Gowers. A fully automatic problem solver with human-style output. CoRR, abs/1309.4501, 2013. URL http://arxiv.org/abs/1309.4501. — [arXiv:1309.4501](https://arxiv.org/abs/1309.4501) ↗
  41. Github. Github copilot · your ai pair programmer, 2021. URL https://github.com/features/copilot/. ↗
  42. O. Golovneva, M. Chen, S. Poff, M. Corredor, L. Zettlemoyer, M. Fazel-Zarandi, and A. Celikyilmaz. ROSCOE: A suite of metrics for scoring step-by-step reasoning. CoRR, abs/2212.07919, 2022. doi: 10.48550/arXiv.2212.07919. URL https://doi.org/10.48550/arXiv.2212.07919. ↗
  43. W. T. Gowers. How can it be feasible to find proofs?, 2022. URL https://drive.google.com/file/d/ 1-FFa6nMVg18m1zPtoAQrFalwpx2YaGK4/view. ↗
  44. T. Hales. The flyspeck project, Aug 2014. URL https://code.google.com/archive/p/flyspeck/. ↗
  45. T. C. Hales. A proof of the kepler conjecture. Annals of Mathematics, 162:1063–1183, 2005. find
  46. J. M. Han, J. Rute, Y. Wu, E. W. Ayers, and S. Polu. Proof artifact co-training for theorem proving with language models. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022.
  47. OpenReview.net, 2022. URL https://openreview.net/forum?id=rpxJc9j04U. ↗
  48. J. Harrison, J. Urban, and F. Wiedijk. History of interactive theorem proving. In Computational Logic, volume 9, pages 135–214, 2014.
  49. Hugging Face. Hugging face spaces, 2021. URL https://huggingface.co/spaces. ↗
  50. J. Hullman, X. Qiao, M. Correll, A. Kale, and M. Kay. In pursuit of error: A survey of uncertainty visualization evaluation. IEEE transactions on visualization and computer graphics, 25(1):903–913, 2018. find
  51. A. Q. Jiang, W. Li, S. Tworkowski, K. Czechowski, T. Odrzygózdz, P. Milos, Y. Wu, and M. Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. CoRR, abs/2205.10893, 2022a. doi: 10.48550/arXiv.2205.10893. URL https://doi.org/10.48550/arXiv.2205.10893. ↗
  52. A. Q. Jiang, S. Welleck, J. P. Zhou, W. Li, J. Liu, M. Jamnik, T. Lacroix, Y. Wu, and G. Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. CoRR, abs/2210.12283, 2022b. doi: 10.48550/arXiv.2210.12283. URL https://doi.org/10.48550/arXiv.2210.12283. ↗
  53. S. M. Kazemi, N. Kim, D. Bhatia, X. Xu, and D. Ramachandran. Lambada: Backward chaining for automated reasoning in natural language. arXiv preprint arXiv:2212.13894, 2022.
  54. M. Kelly, A. Kumar, P. Smyth, and M. Steyvers. Capturing humans’ mental models of ai: An item response theory approach. FAccT, 2023. find
  55. R. Kocielnik, S. Amershi, and P. N. Bennett. Will you accept an imperfect ai? exploring designs for adjusting end-user expectations of ai systems. In Proceedings of the 2019 CHI Conference on Human Factors in Computing Systems, pages 1–14, 2019. find
  56. A. Köpf, Y. Kilcher, D. von Rütte, S. Anagnostidis, Z.-R. Tam, K. Stevens, A. Barhoum, N. M. Duc, O. Stanley, R. Nagyfi, S. ES, S. Suri, D. Glushkov, A. Dantuluri, A. Maguire, C. Schuhmann, H. Nguyen, and A. Mattick. Openassistant conversations – democratizing large language model alignment, 2023. — OpenAssistant Conversations — Democratizing Large Language Model Alignment
  57. E. Kıcıman, R. Ness, A. Sharma, and C. Tan. Causal reasoning and large language models: Opening a new frontier for causality, 2023. find
  58. G. Lample, T. Lacroix, M.-A. Lachaux, A. Rodriguez, A. Hayat, T. Lavril, G. Ebner, and X. Martinet. Hypertree proof search for neural theorem proving. Advances in Neural Information Processing Systems, 35:26337–26349, 2022.
  59. M. Lee, P. Liang, and Q. Yang. Coauthor: Designing a human-ai collaborative writing dataset for exploring language model capabilities. In Proceedings of the 2022 CHI Conference on Human Factors in Computing Systems, pages 1–19, 2022a.
  60. M. Lee, M. Srivastava, A. Hardy, J. Thickstun, E. Durmus, A. Paranjape, I. Gerard-Ursin, X. L. Li, F. Ladhak, F. Rong, R. E. Wang, M. Kwon, J. S. Park, H. Cao, T. Lee, R. Bommasani, M. Bernstein, and P. Liang. Evaluating human-language model interaction, 2022b. URL https://arxiv.org/abs/2212.09746. ↗
  61. M. Lee, M. Srivastava, A. Hardy, J. Thickstun, E. Durmus, A. Paranjape, I. Gerard-Ursin, X. L. Li, F. Ladhak, F. Rong, et al. Evaluating human-language model interaction. arXiv preprint arXiv:2212.09746, 2022c. find
  62. A. Lewkowycz, A. Andreassen, D. Dohan, E. Dyer, H. Michalewski, V. V. Ramasesh, A. Slone, C. Anil, I. Schlag, T. Gutman-Solo, Y. Wu, B. Neyshabur, G. Gur-Ari, and V. Misra. Solving quantitative reasoning problems with language models. CoRR, abs/2206.14858, 2022. doi: 10.48550/arXiv.2206.14858. URL h…
  63. B. Z. Li, W. Chen, P. Sharma, and J. Andreas. Lampp: Language models as probabilistic priors for perception and action. arXiv e-prints, pages arXiv–2302, 2023. find
  64. Z. Li, G. Poesia, O. Costilla-Reyes, N. D. Goodman, and A. Solar-Lezama. LEMMA: bootstrapping high-level mathematical reasoning with learned symbolic abstractions. CoRR, abs/2211.08671, 2022. doi: 10.48550/arXiv.2211.08671. URL https://doi.org/10.48550/arXiv.2211.08671. — [doi:10.48550/arxiv.2211.08671](https://doi.org/10.48550/arxiv.2211.08671) ↗
  65. C.-Y. Lin. ROUGE: A package for automatic evaluation of summaries. In Text Summarization Branches Out, pages 74–81, Barcelona, Spain, July 2004. Association for Computational Linguistics. URL https://aclanthology.org/W04-1013. ↗
  66. B. Lipkin, L. Wong, G. Grand, and J. B. Tenenbaum. Evaluating statistical language models as pragmatic reasoners. arXiv preprint arXiv:2305.01020, 2023.
  67. B. F. Liu, L. Bartz, and N. Duke. Communicating crisis uncertainty: A review of the knowledge gaps. Public relations review, 42(3):479–487, 2016. find
  68. P. Lu, L. Qiu, W. Yu, S. Welleck, and K. Chang. A survey of deep learning for mathematical reasoning. CoRR, abs/2212.10535, 2022. doi: 10.48550/arXiv.2212.10535. URL https://doi.org/10.48550/arXiv. 2212.10535. ↗
  69. T. McGrath, A. Kapishnikov, N. Tomašev, A. Pearce, M. Wattenberg, D. Hassabis, B. Kim, U. Paquet, and V. Kramnik. Acquisition of chess knowledge in alphazero. Proceedings of the National Academy of Sciences, 119(47):e2206625119, 2022. find
  70. K. Meng, D. Bau, A. Andonian, and Y. Belinkov. Locating and editing factual associations in gpt. Advances in Neural Information Processing Systems, 35:17359–17372, 2022. find
  71. M. Mikula, S. Antoniak, S. Tworkowski, A. Q. Jiang, J. P. Zhou, C. Szegedy, L. Kucinski, P. Milos, and Y. Wu. Magnushammer: A transformer-based approach to premise selection. CoRR, abs/2303.04488, 2023. doi: 10.48550/arXiv.2303.04488. URL https://doi.org/10.48550/arXiv.2303.04488. ↗
  72. T. Miller. Explainable ai is dead, long live explainable ai! hypothesis-driven decision support, 2023. find
  73. P. Mirowski, K. W. Mathewson, J. Pittman, and R. Evans. Co-writing screenplays and theatre scripts with language models: Evaluation by industry professionals. In Proceedings of the 2023 CHI Conference on Human Factors in Computing Systems, CHI ’23, New York, NY, USA, 2023. Association for Computing… — [doi:10.1145/3544548.3581225](https://doi.org/10.1145/3544548.3581225) find
  74. E. Mitchell, C. Lin, A. Bosselut, C. D. Manning, and C. Finn. Memory-based model editing at scale. In International Conference on Machine Learning, pages 15817–15831. PMLR, 2022. find
  75. H. Moravec. Mind children: The future of robot and human intelligence. Harvard University Press, 1988. find
  76. A. Newell and H. Simon. The logic theory machine–a complex information processing system. IRE Transactions on information theory, 2(3):61–79, 1956. — The logic theory machine: A complex information processing system
  77. OpenAI. Introducing chatgpt, 2022. URL https://openai.com/blog/chatgpt. ↗
  78. OpenAI. Chatgpt plugins, 2023a. URL https://openai.com/blog/chatgpt-plugins. ↗
  79. OpenAI. Gpt-4 technical report, 2023b.
  80. L. Ouyang, J. Wu, X. Jiang, D. Almeida, C. L. Wainwright, P. Mishkin, C. Zhang, S. Agarwal, K. Slama, A. Ray, J. Schulman, J. Hilton, F. Kelton, L. Miller, M. Simens, A. Askell, P. Welinder, P. Christiano, J. Leike, and R. Lowe. Training language models to follow instructions with human feedback, 20…
  81. K. Papineni, S. Roukos, T. Ward, and W. 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, pages 311–318.
  82. ACL, 2002. doi: 10.3115/1073083.1073135. URL https://aclanthology.org/P02-1040/. ↗
  83. L. C. Paulson. Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In R. A. Schmidt, S. Schulz, and B. Konev, editors, Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, PAAR-2010, Edinburgh, Scotland, UK, July 14… find
  84. EasyChair, 2010. doi: 10.29007/tnfd. URL https://doi.org/10.29007/tnfd. ↗
  85. S. T. Piantadosi and F. Hill. Meaning without reference in large language models. CoRR, abs/2208.02957, 2022. doi: 10.48550/arXiv.2208.02957. URL https://doi.org/10.48550/arXiv.2208.02957. — [doi:10.48550/arxiv.2208.02957](https://doi.org/10.48550/arxiv.2208.02957) ↗
  86. G. Poesia and N. D. Goodman. Peano: Learning formal mathematical reasoning. CoRR, abs/2211.15864, 2022. doi: 10.48550/arXiv.2211.15864. URL https://doi.org/10.48550/arXiv.2211.15864. ↗
  87. S. Polu and I. Sutskever. Generative language modeling for automated theorem proving. CoRR, abs/2009.03393, 2020. URL https://arxiv.org/abs/2009.03393. ↗
  88. S. Polu, J. M. Han, K. Zheng, M. Baksys, I. Babuschkin, and I. Sutskever. Formal mathematics statement curriculum learning. CoRR, abs/2202.01344, 2022. URL https://arxiv.org/abs/2202.01344. ↗
  89. A. Radford, J. Wu, R. Child, D. Luan, D. Amodei, and I. Sutskever. Language models are unsupervised multitask learners. In OpenAI blog, 2019. find
  90. T. Ringer, A. Sanchez-Stern, D. Grossman, and S. Lerner. Replica: REPL instrumentation for coq analysis. In J. Blanchette and C. Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 9… find
  91. ACM, 2020. doi: 10.1145/3372885.3373823. URL https://doi.org/10.1145/3372885.3373823. — [doi:10.1145/3372885.3373823](https://doi.org/10.1145/3372885.3373823) ↗
  92. S. Schulz. E - a brainiac theorem prover. AI Commun., 15:111–126, 2002. find
  93. R. Sevastjanova and M. El-Assady. Beware the rationalization trap! when language model explainability diverges from our mental models of language. arXiv preprint arXiv:2207.06897, 2022. — [arXiv:2207.06897](https://arxiv.org/abs/2207.06897) find
  94. H. Shen and T. Wu. Parachute: Evaluating interactive human-lm co-writing systems. arXiv e-prints, pages arXiv–2303, 2023. find
  95. C. Si, Z. Gan, Z. Yang, S. Wang, J. Wang, J. Boyd-Graber, and L. Wang. Prompting gpt-3 to be reliable. arXiv preprint arXiv:2210.09150, 2022.
  96. D. Spiegelhalter. Risk and Uncertainty Communication. Annual Review of Statistics and Its Application, 4(1):31–60, 2017. ISSN 2326-8298, 2326-831X. doi: 10.1146/annurev-statistics-010814-020148. URL http://www.annualreviews.org/doi/10.1146/annurev-statistics-010814-020148. — [doi:10.1146/annurev-statistics-010814-020148](https://doi.org/10.1146/annurev-statistics-010814-020148) ↗
  97. G. Sutcliffe and C. Suttner. Evaluating general purpose automated theorem proving systems. Artificial intelligence, 131(1-2):39–54, 2001. find
  98. R. Taori, I. Gulrajani, T. Zhang, Y. Dubois, X. Li, C. Guestrin, P. Liang, and T. B. Hashimoto. Stanford alpaca: An instruction-following llama model. https://github.com/tatsu-lab/stanford_alpaca, 2023. ↗
  99. A. Tarski. Truth and proof. Scientific American, 220(6):63–77, 1969. find
  100. H. Touvron, T. Lavril, G. Izacard, X. Martinet, M.-A. Lachaux, T. Lacroix, B. Rozière, N. Goyal, E. Hambro, F. Azhar, et al. Llama: Open and efficient foundation language models. arXiv e-prints, pages arXiv–2302, 2023.
  101. H. Vasconcelos, G. Bansal, A. Fourney, Q. V. Liao, and J. Wortman Vaughan. Generation probabilities are not enough: Exploring the effectiveness of uncertainty highlighting in ai-powered code completions. arXiv e-prints, pages arXiv–2302, 2023. find
  102. H. Wang. Toward mechanical mathematics. IBM J. Res. Dev., 4(1):2–22, jan 1960. ISSN 0018-8646. doi: 10.1147/rd.41.0002. URL https://doi.org/10.1147/rd.41.0002. ↗
  103. J. Wei, X. Wang, D. Schuurmans, M. Bosma, F. Xia, E. H. Chi, Q. V. Le, D. Zhou, et al. Chain-of-thought prompting elicits reasoning in large language models. In Advances in Neural Information Processing Systems, 2022.
  104. S. Welleck, J. Liu, X. Lu, H. Hajishirzi, and Y. Choi. Naturalprover: Grounded mathematical proof generation with language models, 2022a. URL https://arxiv.org/abs/2205.12910. ↗
  105. S. Welleck, J. Liu, X. Lu, H. Hajishirzi, and Y. Choi. Naturalprover: Grounded mathematical proof generation with language models. In NeurIPS, 2022b. URL http://papers.nips.cc/paper_files/paper/2022/ hash/1fc548a8243ad06616eee731e0572927-Abstract-Conference.html. ↗
  106. B. Wilder, E. Horvitz, and E. Kamar. Learning to complement humans. In Proceedings of the Twenty-Ninth International Conference on International Joint Conferences on Artificial Intelligence, pages 1526–1533, 2021a. find
  107. B. Wilder, E. Horvitz, and E. Kamar. Learning to complement humans. In Proceedings of the Twenty-Ninth International Conference on International Joint Conferences on Artificial Intelligence, pages 1526–1533, 2021b. find
  108. L. Wong, G. Grand, A. K. Lew, N. D. Goodman, V. K. Mansinghka, J. Andreas, and J. B. Tenenbaum. From word models to world models: Translating from natural language to the probabilistic language of thought. arXiv preprint arXiv:2306.12672, 2023. find
  109. Y. Wu, A. Q. Jiang, W. Li, M. N. Rabe, C. Staats, M. Jamnik, and C. Szegedy. Autoformalization with large language models. CoRR, abs/2205.12615, 2022. doi: 10.48550/arXiv.2205.12615. URL https://doi.org/10.48550/arXiv.2205.12615. ↗
  110. Z. Wu, A. Geiger, C. Potts, and N. D. Goodman. Interpretability at scale: Identifying causal mechanisms in alpaca. arXiv preprint arXiv:2305.08809, 2023.
  111. Y. Xiao, P. P. Liang, U. Bhatt, W. Neiswanger, R. Salakhutdinov, and L.-P. Morency. Uncertainty quantification with pre-trained language models: A large-scale empirical analysis. In Findings of the Association for Computational Linguistics: EMNLP 2022, pages 7273–7284, Abu Dhabi, United Arab Emirate… find
  112. S. Yao, D. Yu, J. Zhao, I. Shafran, T. L. Griffiths, Y. Cao, and K. Narasimhan. Tree of thoughts: Deliberate problem solving with large language models, 2023. find
  113. E. Zelikman, Q. Huang, G. Poesia, N. D. Goodman, and N. Haber. Parsel: A unified natural language framework for algorithmic reasoning. CoRR, abs/2212.10561, 2022a. doi: 10.48550/arXiv.2212.10561. URL https://doi.org/10.48550/arXiv.2212.10561. ↗
  114. E. Zelikman, Y. Wu, J. Mu, and N. D. Goodman. Star: Bootstrapping reasoning with reasoning, 2022b.
  115. J. Zerilli, U. Bhatt, and A. Weller. How transparency modulates trust in artificial intelligence. Patterns, 3(4): 100455, 2022. find
  116. K. Zheng, J. M. Han, and S. 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.
  117. OpenReview.net, 2022. URL https://openreview.net/forum?id=9ZPegFuFTFv. ↗
  118. D. Zhou, N. Schärli, L. Hou, J. Wei, N. Scales, X. Wang, D. Schuurmans, O. Bousquet, Q. Le, and E. Chi. Least-to-most prompting enables complex reasoning in large language models. ICLR, 2023.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/collins-2023-evaluating-language-models-mathematics-through/