# Faultless：验证和评估神经反编译器的程序等价性方法

> 利用符号执行与专门的内存模型，将神经反编译器生成的 C 代码与确定性反编译结果或参考函数比较，无需完整周边代码库，可用于分析人员的结果核查及模型评估。

- 作者：Luke Dramko; Claire Le Goues; Edward Schwartz
- 原标题：Faultless: A Program Equivalence Technique for Validating and Evaluating Neural Decompilers
- 发表载体：arXiv
- 发表状态：预印本
- 出版／提交日期：2026 年 9 月 28 日
- 日期依据：采用 arXiv v1 首次提交日期；未核实正式发表场所。
- arXiv 首次提交：2026 年 9 月 28 日
- arXiv：2609.34089
- 已复核的 arXiv 版本：v1
- DOI：10.48550/arxiv.2609.34089
- 来源复核于：2026-10-20
- 收录于：2026-10-20
- 原始论文：<https://arxiv.org/abs/2609.34089>
- PDF：<https://arxiv.org/pdf/2609.34089v1>
- 代码：<https://github.com/squaresLab/faultless>
- BibTeX：<https://awesomerea.org/papers/citations/paper-faultless.bib>
- 目录页面：<https://awesomerea.org/zh/papers/paper-faultless/>
- 记录 JSON：<https://awesomerea.org/papers/paper-faultless/record.json>
- 英文版：[English](https://awesomerea.org/papers/paper-faultless/index.md)

## 研究范围与局限

检查限定于函数级，抽象掉副作用顺序和部分编译器细节，选项还可放宽返回值、实参及类型条件。实现明确存在与堆有关的可靠性缺口，并要求兼容的循环结构；不支持的 C 特性及脱离上下文的依赖假设也限制覆盖。未能建立等价关系并不证明不等价。实验使用筛选后的 realtype 与 ExeBench 函数对，不代表任意整程序等价。

## 与本合集的关联

为恢复代码提供具体核查方法，同时揭示无条件“等价”标签可能掩盖的假设与不可靠情形。

## 发表与复核说明

三位作者顺序与首投日期依据 arXiv v1。摘要页虽仍显示 DOI 待登记，DataCite 已将其列为可检索，登记于 2026-09-29。论文采用 CC BY-SA 4.0。作者链接的公开仓库固定核查于 059023d874f4103b5e645a9d6d6ddbdb2bbb6da0；根目录为 MIT 许可，README 将基于 Python、tree-sitter 与 Z3 的实现称为概念验证。

## 一手来源

1. <https://arxiv.org/abs/2609.34089>
2. <https://arxiv.org/html/2609.34089v1>
3. <https://api.datacite.org/dois/10.48550/arxiv.2609.34089>
4. <https://github.com/squaresLab/faultless>
5. <https://github.com/squaresLab/faultless/blob/059023d874f4103b5e645a9d6d6ddbdb2bbb6da0/README.md>
6. <https://github.com/squaresLab/faultless/blob/059023d874f4103b5e645a9d6d6ddbdb2bbb6da0/LICENSE>
7. <https://github.com/squaresLab/faultless/blob/059023d874f4103b5e645a9d6d6ddbdb2bbb6da0/pyproject.toml>

## 关于此条目

已依据论文及一手来源复核。请通过原始论文或 BibTeX 引用原作者。
原创说明采用 MIT 许可；外部项目、论文与素材保留各自的权利和许可。