FMitF: Track I: Formal Verification for Mechanism Design

FMITF：第一轨：机制设计的形式验证

• 批准号: 2319186
• 负责人: Justin Hsu
• 金额: $ 60万
• 依托单位: Cornell University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-09-15 至 2027-08-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2319186&HistoricalAwards=false
• 关键词: FMitF; Track; Formal; Verification; Mechanism

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.

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