面向自动定理证明树搜索的大模型生成器直接优化研究
该论文针对自动定理证明（ATP）中微调大语言模型的对齐问题展开研究。当前大模型常作为树搜索的引导策略，而传统交叉熵损失在搜索场景下并非最优。将对齐策略拓展至树搜索具有较大挑战，因为证明发现过程高度依赖监督演示中未包含的偏离轨迹状态的探索与恢复。为此，作者拓展了相关计算对齐方法以直接优化搜索生成器。注：由于原摘要结尾截断，更多技术细节尚未完整披露。
DC AI 热点
全部 AI 动态
9月24日2026-09-24
该论文针对自动定理证明（ATP）中微调大语言模型的对齐问题展开研究。当前大模型常作为树搜索的引导策略，而传统交叉熵损失在搜索场景下并非最优。将对齐策略拓展至树搜索具有较大挑战，因为证明发现过程高度依赖监督演示中未包含的偏离轨迹状态的探索与恢复。为此，作者拓展了相关计算对齐方法以直接优化搜索生成器。注：由于原摘要结尾截断，更多技术细节尚未完整披露。