Accelerating Scientific Research with Gemini: Case Studies and Common Techniques

大型语言模型（LLMs）的最新进展为加速科学研究开辟了新路径。尽管当前模型在辅助完成常规任务方面能力日益增强，但其能否真正参与新颖、高水平的数学发现，仍缺乏深入理解。本文呈现了一系列典型案例，展示了研究人员如何成功地与先进的AI模型——特别是基于谷歌Gemini架构的模型（尤其是Gemini Deep Think及其高级变体）——开展协作，在理论计算机科学的多个方向，以及经济学、优化理论和物理学等其他领域中，解决开放性问题、证伪已有猜想，并生成全新的数学证明。基于这些实践经验，我们提炼出若干在理论研究中实现高效人机协作的通用策略，包括迭代式精化、问题分解，以及跨学科知识迁移。虽然本文绝大多数成果均源于这种交互式、对话式的协作范式，我们也特别指出了一些突破传统聊天界面限制的创新应用：例如，将模型部署为严谨的对抗性审稿人，用以识别现有证明中细微的逻辑漏洞；又如，将模型嵌入一种“神经-符号”闭环系统，使其能够自主编写并执行代码，以验证复杂的数学推导过程。综上所述，这些实例共同表明：AI的潜力远不止于自动化工具——它正日益成长为科学发现创造性过程中一位多才多艺、名副其实的合作伙伴。

探索大型语言模型（特别是Gemini Deep Think系列）在专家级数学与理论科学研究中作为创造性合作伙伴的潜力，验证其能否实质性参与开放问题求解、猜想证伪和新证明生成，而非仅执行常规辅助任务。这是一个新兴且尚未系统验证的方向，超越了当前AI作为‘工具’的主流范式。

提出并实证了一种以人类为中心、多模式协同的AI协作范式，核心包括：（1）结构化交互技术（迭代 refinement、问题 decomposition、跨学科知识迁移）；（2）突破聊天界面的增强用法——将模型角色化为严格对抗性审稿人，以及嵌入神经符号闭环（自动编写→执行→验证代码）。其新意在于将LLM定位为可问责、可验证、具批判性思维的‘科研协作者’，而非被动响应者。

涵盖理论计算机科学、经济学、优化、物理等多领域真实研究案例；强调过程透明性与可复现性——所有案例均基于交互日志与人工监督，未依赖黑箱端到端训练；未使用专用微调或私有数据，全部基于公开可用的Gemini Advanced接口；突出‘人机责任分工’：人类定义语义、设定验证标准、判断数学严谨性，AI承担高维搜索、反例生成、符号推演与自动化检验；值得深入的方向包括：形式化协作协议设计、AI生成证明的机器可检验证明格式对齐、神经符号闭环的泛化架构。

‘Language Models as Zero-Shot Reasoners’ (ICLR 2023); ‘Formal Mathematics for Large Language Models’ (NeurIPS 2023); ‘LeanDojo: An Open Repository for Machine Learning in Theorem Proving’ (ICML 2024); ‘Mathematical Reasoning via Verifiable Reasoning Chains’ (ACL 2024); ‘Collaborative AI for Scientific Discovery’ (Nature Machine Intelligence, 2023)