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 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。