Odyssey：面向专家驱动的浮点表达式重写的交互式工作台

文献标题

Odyssey: An Interactive Workbench for Expert-Driven Floating-Point Expression Rewriting

文献信息

• 主题领域: 浮点数学表达式重写及可视化开发工具
• 关键词: 浮点运算, 专家程序设计, 调试, 开发工具, 表达式重写, 动态分析

研究背景与问题

• 发现的问题或挑战:

  1. 浮点数运算在科学、工程和图形应用中广泛应用，但浮点数舍入误差可能导致结果严重偏离实际值。
  2. 尽管已有自动化工具（例如 Herbie）用于识别和改进浮点表达式的舍入误差，但用户难以有效地应用这些工具，特别是在指定目标、解释结果和开展独立探索时。
  3. 当前工具通常忽视对表达式重写的多来源对比，导致工具输出复杂并缺乏用户信任。

• 重要性: 浮点数舍入误差可能引发不可重复的科学研究、金融市场指数偏差，甚至在军事应用中导致严重后果。因此，准确诊断和修复此类错误对确保这些领域的结果可靠性至关重要。

• 研究动机与相关工作:

  1. 现有工具（如 Herbie）采用自动化方法改写浮点表达式，但在用户体验和准确性方面仍存在不足。
  2. 浮点运算相关的分析工具涵盖误差分析、动态分析、代码优化等，这些功能若结合用户交互工具，可能提供更全面的解决方案。

解决方案

• 提出的解决方案: 开发一个新的交互式工作平台 Odyssey，使用户能够以一个三阶段工作流程（诊断问题、生成解决方案、优化结果）分析和优化浮点表达式。

• 创新之处:

  1. 提供交互式错误诊断工具，包括局部误差热图和范围调整。
  2. 支持从多来源（例如自动化工具、人主观输入及其他参考资料）收集并管理表达式改写。
  3. 提供表达式的实时错误反馈，帮助用户优化、调整分支条件，避免舍入误差。

• 实施步骤与关键技术:

  1. 问题诊断: 使用误差可视化工具（如局部误差热图）标记问题表达式，并识别特定的错误操作。
  2. 解决生成: 用户可通过与 Herbie 集成生成重新表达式，也允许用户手动输入表达式并即时反馈错误数据。
  3. 结果优化: 通过调整表达式分支条件和特定参数，实现更优性能与误差特性；支持多表达式对比及分支重写。

研究成果

• 具体成果:

  1. 创造了一个集成的工作平台，通过用户交互及便捷的工具组合显著提升了浮点表达式分析效率。
  2. 在用户测试中，不同浮点专家使用 Odyssey 能够解决 5/7 现实难题，并普遍对工具可视化功能表示赞赏。

• 与现有解决方案的优势:

  1. Odyssey 显著改进了表达式重写的交互性，解决了现有工具在分析速度和用户参与上的不足。
  2. 提供可调和即时反馈的手段，使专家可以专注于创造性问题解决而非工具限制。

• 实验与评估结果:

  1. 专家用户在实验中展现出高效的表达式问题分析及改进能力，平均能快速完成多任务。
  2. 调查结果显示，专家一致认为 Odyssey 能高效辅助其识别问题、生成新解、混合和优化表达式。

• 局限性与未来方向:

  1. 工具实现方面仍需更多技术打磨，如界面布局改进及更深入的表达式编辑支持。
  2. 未来计划扩展对多源分析工具的整合，支持多精度表达式、操作成本分析等高级功能。
  3. 探讨利用语言模型（如 GPT）生成表达式重写和错误解释，以进一步提升工具智能化水平。