通过人机交互定理证明推进数学研究
A Human-AI Collaborative Workflow for Mathematical Discovery: A Case Study in Grover-Compatible Riemannian Optimization
AI总结：
本文提出了一种人机交互的定理证明流程，利用大语言模型辅助数学研究，通过案例研究展示其在流形优化与Grover算法间连接的探索能力。
摘要：
我们探讨了大语言模型如何在科学计算中作为研究工具使用，同时保持数学严谨性。我们提出了一种人机交互的定理证明与发现工作流程，利用LLM进行证明或矛盾的搜索，提出候选属性和定理，并帮助构建满足显式约束的结构和参数，通过数值实验和简单验证检查支持。专家将这些输出作为原材料，进一步完善它们，并将结果组织成精确的陈述和严谨的证明。我们通过一个关于流形优化与Grover量子搜索算法之间联系的案例研究来实例化这一工作流程，其中流程帮助识别不变子空间，探索与Grover兼容的退化映射，并获得基于退化映射的梯度方法的收敛保证。该框架为将大语言模型整合到前沿数学研究中提供了一个实用模板，使探索证明空间和算法设计更快，同时保持透明的推理责任。尽管在量子计算中的流形优化问题中进行了示例，但其原理可扩展到科学计算的其他核心领域。
英文摘要：
We investigate how large language models can be used as research tools in scientific computing while preserving mathematical rigor. We propose a human-in-the-loop workflow for interactive theorem proving and discovery with LLMs. Human experts retain control over problem formulation and assumptions, while the model searches for proofs or contradictions, proposes candidate properties and theorems, and helps construct structures and parameters that satisfy explicit constraints, supported by numerical experiments and simple verification checks. Experts treat these outputs as raw material, further refine them, and organize the results into precise statements and rigorous proofs. We instantiate this workflow in a main case study on the connection between manifold optimization and Grover's quantum search algorithm, where the pipeline identifies invariant subspaces and explores Grover-compatible retractions. The main case study uses the corresponding Grover-compatible convergence analysis, including an $O(\sqrt{N} \log(1/\varepsilon))$ PL-based bound established in the companion mathematical work, to illustrate the refinement stage of the workflow. Prompt records and reusable templates for implementing the workflow are provided. We further include a multi-oracle case study, document representative failed and corrected routes arising from this setting, and provide a structured failure-mode analysis.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
