FMitF: Track I: Formal Verification for Mechanism Design

机制设计领域研究如何构建算法来解决经济问题，例如在拍卖会上出售物品，或在市场上匹配买家和卖家。该项目旨在为经济机制制定正式的核查方法，解决两个主要的技术挑战。首先，机制是复杂的：机制是在结构丰富的、通常是定量的数据上运行的。第二，机制接受由经济代理人控制的投入，这些经济代理人可能有动机操纵他们报告的投入。机制的非经济相关属性需要对代理人的行为进行假设和推理。该项目在沿着两个方面具有更广泛的影响。首先，随着机制越来越多地用于高风险环境，以使人们与稀缺资源相匹配（例如，居民到医院，学生到学校，甚至器官捐赠者到接受者），执行错误的风险和后果增加。该项目旨在制定方法，以验证经济机制是否得到正确实施。第二，由于机制的目的是以社会可接受的方式分配资源，透明度和问责制至关重要。该项目开发的方法可以帮助独立审计员证明机制的行为正确。此外，该项目包括综合教育和推广活动，涵盖计算机科学和经济学。该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的知识价值和更广泛的影响审查标准进行评估。

The field of mechanism design studies how to build algorithms to solve economic problems, such as selling an item at an auction, or matching buyers to sellers in a marketplace. This project aims to develop formal verification methods for economic mechanisms, addressing two main technical challenges. First, mechanisms are complex: mechanisms operate on richly structured, and often quantitative, data. Second, mechanisms accept inputs controlled by economic agents who may have incentives to manipulate the inputs they report. Verifying economically-relevant properties of mechanisms requires assuming and reasoning about how agents behave. This project has broader impacts along two dimensions. First, as mechanisms are increasingly used in high-stakes settings to match people to scarce resources (e.g., residents to hospitals, students to schools, and even organ donors to recipients), the risks and consequences of implementation errors increase. This project aims to develop methods to verify that economic mechanisms are implemented correctly. Second, since mechanisms aim to allocate resources in a socially acceptable manner, transparency and accountability are paramount. Methods developed by this project could help independent auditors certify that mechanisms behave correctly. Further, this project incorporates integrated education and outreach activities spanning both computer science and economics.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.