FMitF: Track I: Formal Verification for Mechanism Design

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

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.