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.