描述初始人機交互的證明形式化工作流
這項研究探討了數學家如何利用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工具的改進，這種人機協作模式有望進一步優化證明形式化的效率與可靠性。