描述初始人机交互的证明形式化工作流
这项研究探讨了数学家如何利用AI进行数学证明的形式化。通过调查和用户实验，发现人们希望AI协助但保留高级控制权，使用AI能提高准确率，并且用户倾向于使用多种AI工具。
来源arXiv AI作者: Katherine M. Collins, Simon Frieder, Jonas Bayer, Jacob Loader, Jeck Lim, Peiyang Song, Fabian Zaiser, Lexin Zhou, Shanda Li, Sam Looi, Joshua B. Tenenbaum, Umang Bhatt, Adrian Weller, Jose Hernandez-Orallo, Cameron E. Freer, Valerie Chen, Ilia Sucholutsky
长期以来，数学证明的形式化一直是自动验证中的核心挑战。随着AI系统在代码生成和高级数学推理方面的能力不断提升，人们有望改变形式化证明的方式，进而实现自动验证。然而，现有研究大多聚焦于基准测试AI的性能，而非人类如何使用这些工具。本研究采用混合方法，深入分析了AI对形式化工作流的初始影响。
研究团队首先通过定性调查了解了数学家的偏好。结果显示，尽管受访者的期望各异，但普遍希望AI在形式化过程中提供协助，同时保留人类对证明发现过程的高层控制。例如，许多数学家希望AI能处理繁琐的细节，但由人类决定证明的总体方向。
为了评估实际使用情况，研究者进行了一项控制实验。参与者需要将非正式的数学问题及其证明形式化，涉及不同难度和领域的问题。部分参与者可以使用AI工具，部分则不能。结果发现，尽管当时的AI工具在自动形式化方面存在局限，使用AI的参与者仍然获得了更高的形式化准确率。大多数参与者会灵活地结合多种AI工具来完成任务，而非依赖单一工具。
这项研究揭示了AI整合到形式化工作流初期的关键特征：人类与AI的密切互动。研究强调了在保留人类主导性的前提下，充分发挥AI辅助潜力的重要性。未来，随着AI工具的改进，这种人机协作模式有望进一步优化证明形式化的效率与可靠性。