一、文章主要内容总结
本文聚焦大语言模型（LLMs）在程序优化中无法保证正确性的核心问题，提出了一种名为LGuess的新方法——基于LLM引导的等式饱和（equality saturation），通过引入e-图作为LLMs与形式化重写系统之间的中间层，弥补LLMs生成可靠重写链能力不足的缺陷。
- 分阶段执行等式饱和：每个阶段为当前程序构建e-图，在资源限制内完成饱和后，通过LLM从e-图中提取高层面的“检查点”（checkpoint）作为下一阶段输入，循环直至收敛。
- 关键技术：采用从LLM中学习的二元语法（bigram）概率模型，高效从庞大的饱和e-图中提取合适的检查点——通过迭代采样、LLM对比反馈、模型迭代优化，减少搜索空间，避免逐一查询e-图中所有程序的低效问题。
