我们介绍了一个使用Gemini帮助科学家严格验证其会议投稿论文正确性的新工具,该工具在STOC 2026大会上进行了测试。
理论计算机科学和数学对真理的追求依赖于最高标准的证明、严谨性和清晰度。虽然同行评议是关键的最终检查,但起草和完善复杂理论工作的过程往往需要数月时间,简单错误、变量不一致或细微的逻辑漏洞经常拖慢整个研究流程。但是,一个高度专业化的AI工具能否作为快速、严谨的合作伙伴,帮助作者在论文提交给人类评审员之前预先审查他们的工作?
为了测试这种潜力,我们为计算理论年度ACM研讨会(STOC 2026)创建了一个实验项目——这是理论计算机科学领域最权威的会议之一。该项目为作者提供由专门的Gemini AI工具生成的自动化预提交反馈。我们的目标是在提交后24小时内提供建设性建议并识别潜在的技术问题,帮助作者在提交截止日期前完善最终草稿。
反响非常积极:该工具成功识别了各种问题,包括计算和逻辑错误。以下是我们如何开发这个工具以及其使用结果的报告。
技术架构
反馈工具利用了Gemini 2.5 Deep Think高级版本中的推理扩展方法。这种设置使该方法能够在给出最终答案之前同时探索和组合多个可能的解决方案,而不是追求单一的线性思维链。通过结合不同的推理和评估轨迹,该方法减少了固有的幻觉,专注于最突出的问题。
反馈结构
作者收到分为关键部分的结构化反馈:论文贡献摘要、潜在错误和改进建议列表(通常分析特定引理或定理),以及小错误和拼写错误列表。
识别的问题类型
该工具成功识别了广泛的问题,从变量名不一致到复杂问题,如计算错误、不等式应用错误和证明中的逻辑漏洞。正如一位作者所指出的,该工具发现了"一个关键错误...使我们的证明完全错误",并补充说这是一个"让我们困扰数月的令人尴尬的简单错误"。
用户反馈
超过120名参与者回应了我们的实验后调查并给予同意,反响非常积极,个人称赞该模型在发现关键错误方面的成功以及其返回深刻评论的能力。总结如下:
除了技术准确性,作者还重视AI评审的速度和中立性。参与者注意到仅在两天内就收到了反馈。其他人赞扬了输出的"中立语调和严谨性",认为这是人类读者的有用补充。
专家验证和协作潜力
由于参与者是各自领域的专家,他们能够轻松区分有用见解和偶尔的"幻觉"。虽然该模型有时会遇到困难——特别是在解析复杂符号或解释图形时——作者并不会忽视大语言模型的输出。相反,他们仔细过滤噪音,提取输出中重要和正确的部分,然后将反馈作为验证的起点。这一结果清楚地展示了AI作为协作伙伴的潜力,通过帮助人类专家基于模型的严谨输出做出明智决策来增强研究工作流程。
教育价值
在此实验中调查的研究社区看到了该工具在培训下一代方面的巨大潜力。75%的受访作者认为该工具通过提供关于数学严谨性和表述清晰度的即时反馈对学生具有教育价值。
未来展望
这个试点项目展示了专业化AI工具在基础领域作为协作伙伴服务的潜力,为潜在的未来研究计划确立了目标。我们的总体目标不是取代关键的同行评议过程,而是增强和改进它。反映这一点,88%的参与者表达了在整个研究过程中持续使用此类工具的强烈兴趣。
Q&A
Q1:这个Gemini反馈工具的主要功能是什么?
A:该工具为理论计算机科学论文提供自动化预提交反馈,能在24小时内识别计算错误、逻辑漏洞、变量不一致等技术问题,并提供论文贡献摘要、错误改进建议和小错误修正列表。
Q2:研究人员对这个AI反馈工具的评价如何?
A:超过120名参与者的反馈非常积极。一位作者表示工具发现了"让我们困扰数月的关键错误",参与者称赞其速度快(两天内收到反馈)、语调中立严谨,88%的参与者希望在整个研究过程中持续使用此类工具。
Q3:这个工具会取代人类同行评议吗?
A:不会。该工具的目标是增强而非取代同行评议过程。75%的受访者认为它对学生有教育价值,专家能够区分有用见解和偶尔的"幻觉",将其作为协作伙伴来辅助研究工作流程。
好文章,需要你的鼓励
企业AI搜索公司Glean宣布年度经常性收入(ARR)达3亿美元,较15个月前的1亿美元增长三倍。尽管谷歌、微软、OpenAI等科技巨头纷纷入局企业AI搜索市场,Glean凭借"上下文图谱"技术深度理解企业业务需求,并帮助客户显著降低AI计算成本。该公司提供按用量计费和混合定价两种模式,客户涵盖Databricks、Reddit、Pinterest及三星等企业。Glean上轮融资后估值达72亿美元。
香港中文大学与MiniMax提出ClaimDiff-RL框架,将图像描述的AI训练从整体打分升级为逐条核查,有效解决了传统方式导致AI"少说保平安"的问题,同时在多项基准测试上超越Gemini-3-Pro-Preview。
杰夫·贝索斯旗下的蓝色起源公司在佛罗里达卡纳维拉尔角进行静态点火测试时,新格伦重型火箭发生爆炸。这是美国历史上最大规模的火箭爆炸之一,也是蓝色起源公司遭遇的最严重失败。所有人员安全,但该事故可能导致新格伦火箭项目长期暂停。此前该火箭已成功完成三次发射,并实现了助推器回收和重复使用。
ParaVT是一个由南洋理工等多校联合提出的并行视频工具调用框架,通过让AI同时分析多段视频并引入PARA-GRPO算法解决训练中的格式崩溃与工具跳过问题,在六项长视频理解测试中平均提升约7.9%。