基于编码智能体生成的验证编译器的自动化测试与修复
Automated Testing and Repair for Verified Compilers Generated by a Coding Agent
浏览论文内容
中文总结 AI 辅助
该研究针对编码智能体生成的验证编译器，提出了基于智能体的自动化测试与修复系统，经评估其在Axon编译器上无奖励黑客攻击问题，可有效开展测试与修复。
中文摘要 AI 辅助
我们提出了一种基于智能体的自动化测试与修复系统，用于处理包含四类代码的验证编译器：验证代码、已检查代码、未验证代码以及规范。该系统采用专门的缺陷检测技术，利用此类编译器的结构特性来识别问题。对于每个检测到的缺陷，系统会调用编码智能体对缺陷进行修复，并验证修复的有效性。我们在Axon编译器上对该系统进行了评估，Axon是一款完全由开发者监督下运行的编码智能体生成的编译器。该编译器在开发过程中通过小型基准集（Livermore基准）进行了验证，这引发了其编码智能体存在奖励黑客攻击编译器的可能性。我们还评估了修复系统存在奖励黑客攻击修复的可能性，结果发现无论是Axon编译器还是其修复方案，都没有奖励黑客攻击的证据。我们提供了表征测试与修复有效性的结果，并讨论了修复的相关特性。
英文摘要
We present an agent based automated testing and repair system for verified compilers that contain four kinds of code: verified code, checked code, unverified code, and specification. We present specialized defect detection techniques that exploit the structure present in such compilers. For each surfaced defect the system invokes a coding agent to repair the defect and validate the repair. We evaluate the system on the Axon compiler, a compiler completely generated by a coding agent operating under developer supervision. The compiler was validated during development on a small benchmark set (the Livermore benchmarks), raising the possibility that its coding agent reward hacked the compiler. We also evaluate the possibility that the repair system reward hacked the repairs and find no evidence of reward hacking in either the Axon compiler or the repairs. We present results that characterize the testing and repair effectiveness and discuss repair characteristics.
