金融市场交易的正式验证

是 否 +2 论坛币

k人 参与回答

经管之家送您一份

应届毕业生专属福利!

求职就业群

赵安豆老师微信：zhaoandou666

经管之家联合CDA

送您一个全额奖学金名额~ !

立即领取

感谢您参与论坛问题回答

经管之家送您两个论坛币！

+2 论坛币

英文标题：
《Formal verification of trading in financial markets》
---
作者：
Suneel Sarswat and Abhishek Kr Singh
---
最新提交年份：
2019
---
英文摘要：
  We introduce a formal framework for analyzing trades in financial markets. An exchange is where multiple buyers and sellers participate to trade. These days, all big exchanges use computer algorithms that implement double sided auctions to match buy and sell requests and these algorithms must abide by certain regulatory guidelines. For example, market regulators enforce that a matching produced by exchanges should be \\emph{fair}, \\emph{uniform} and \\emph{individual rational}. To verify these properties of trades, we first formally define these notions in a theorem prover and then give formal proofs of relevant results on matchings. Finally, we use this framework to verify properties of two important classes of double sided auctions. All the definitions and results presented in this paper are completely formalised in the Coq proof assistant without adding any additional axioms to it.
---
中文摘要：
我们引入了一个分析金融市场交易的正式框架。交易所是多个买家和卖家参与交易的地方。如今，所有大型交易所都使用实现双边拍卖的计算机算法来匹配买卖请求，这些算法必须遵守某些监管准则。例如，市场监管机构强制要求交易所产生的匹配应该是公平的、统一的和理性的。为了验证交易的这些性质，我们首先在定理证明器中正式定义这些概念，然后在匹配上给出相关结果的正式证明。最后，我们使用这个框架来验证两类重要的双边拍卖的性质。本文给出的所有定义和结果都在Coq证明助手中完全形式化，没有添加任何额外的公理。
---
分类信息：

一级分类：Computer Science        计算机科学
二级分类：Logic in Computer Science        计算机科学中的逻辑
分类描述：Covers all aspects of logic in computer science, including finite model theory, logics of programs, modal logic, and program verification. Programming language semantics should have Programming Languages as the primary subject area. Roughly includes material in ACM Subject Classes D.2.4, F.3.1, F.4.0, F.4.1, and F.4.2; some material in F.4.3 (formal languages) may also be appropriate here, although Computational Complexity is typically the more appropriate subject area.
涵盖计算机科学中逻辑的所有方面，包括有限模型理论，程序逻辑，模态逻辑和程序验证。程序设计语言语义学应该把程序设计语言作为主要的学科领域。大致包括ACM学科类D.2.4、F.3.1、F.4.0、F.4.1和F.4.2中的材料；F.4.3（形式语言）中的一些材料在这里也可能是合适的，尽管计算复杂性通常是更合适的主题领域。
--
一级分类：Computer Science        计算机科学
二级分类：Data Structures and Algorithms        数据结构与算法
分类描述：Covers data structures and analysis of algorithms. Roughly includes material in ACM Subject Classes E.1, E.2, F.2.1, and F.2.2.
涵盖数据结构和算法分析。大致包括ACM学科类E.1、E.2、F.2.1和F.2.2中的材料。
--
一级分类：Computer Science        计算机科学
二级分类：Formal Languages and Automata Theory        形式语言与自动机理论
分类描述：Covers automata theory, formal language theory, grammars, and combinatorics on words. This roughly corresponds to ACM Subject Classes F.1.1, and F.4.3. Papers dealing with computational complexity should go to cs.CC; papers dealing with logic should go to cs.LO.
涵盖自动机理论，形式语言理论，文法，和词的组合学。这大致相当于ACM主题类F.1.1和F.4.3。处理计算复杂性的论文应该上CS.CC；处理逻辑的论文应该去CS.LO。
--
一级分类：Computer Science        计算机科学
二级分类：Computer Science and Game Theory        计算机科学与博弈论
分类描述：Covers all theoretical and applied aspects at the intersection of computer science and game theory, including work in mechanism design, learning in games (which may overlap with Learning), foundations of agent modeling in games (which may overlap with Multiagent systems), coordination, specification and formal methods for non-cooperative computational environments. The area also deals with applications of game theory to areas such as electronic commerce.
涵盖计算机科学和博弈论交叉的所有理论和应用方面，包括机制设计的工作，游戏中的学习（可能与学习重叠），游戏中的agent建模的基础（可能与多agent系统重叠），非合作计算环境的协调、规范和形式化方法。该领域还涉及博弈论在电子商务等领域的应用。
--
一级分类：Computer Science        计算机科学
二级分类：Symbolic Computation        符号计算
分类描述：Roughly includes material in ACM Subject Class I.1.
大致包括ACM学科第一类1的材料。
--
一级分类：Quantitative Finance        数量金融学
二级分类：Trading and Market Microstructure        交易与市场微观结构
分类描述：Market microstructure, liquidity, exchange and auction design, automated trading, agent-based modeling and market-making
市场微观结构，流动性，交易和拍卖设计，自动化交易，基于代理的建模和做市
--

---
PDF下载：
-->

扫码加我 拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

分享0 收藏0 回帖

关键词：金融市场 Verification Applications Environments Coordination

印度孟买塔塔基础研究所Sarswaand Abhishek Kr Singh1 Tata基础研究所金融市场交易正式验证。sarswat@gmail.com2塔塔基础研究所，印度孟买。uor@gmail.comAbstractWe引入一个分析金融市场交易的正式框架。交易所是多个买家和卖家参与交易的场所。如今，所有大型交易所都使用实现双边拍卖的计算机算法来匹配买卖请求，这些算法必须遵守某些监管准则。例如，市场监管机构强制要求交易所进行的匹配应该是公平、统一和个人理性的。为了验证交易的这些性质，我们首先在定理证明中正式定义这些概念，然后给出匹配相关结果的正式证明。最后，我们使用这个框架来验证两类重要的双边拍卖的性质。本文中给出的所有定义和结果都在Coq证明助手中完全形式化，没有添加任何额外的公理。关键词和短语Coq、形式化、拍卖、匹配、金融市场数字对象识别10.4230/LIPIcs。。2019.1简介在本文中，我们介绍了一个分析金融市场交易的正式框架。贸易是所有现代经济的主要组成部分。在过去的几个世纪里，越来越多的复杂工具被引入金融市场进行交易。所有大型证券交易所都使用计算机算法来匹配交易员的买入请求（需求）和卖出请求（供应）。

交易员也使用计算机算法在市场上下订单。随着计算机辅助交易的到来，市场的交易量和流动性急剧增加，因此，市场变得更加复杂。支持整个交易过程的软件程序极其复杂，并且必须满足高效标准，因为它们需要实时处理大量数据。此外，为了提高市场交易者的信心，市场监管机构为这些软件制定了严格的安全和公平准则。传统上，为了满足这些标准，软件开发广泛依赖于在大数据集上测试程序。虽然测试有助于识别bug，但它不能保证bug的存在。即使是交易软件中的小错误也可能对整体经济产生灾难性影响。对手可能会利用一个bug来为自己谋利，也会为其他真正的交易者谋利。在健康的经济中，这些事件当然是不可取的。最近，证券交易所出现了各种违反交易规则的情况。例如，在[1]中，监管机构指出：“纽约证券交易所Arca未能在特定的市场条件下执行特定类型的限制指令，尽管有一条规则，这被称为算法交易。根据知识共享许可证获得许可，由莱布尼茨国际诉讼公司抄送，载于德国达布尼茨出版公司Dagstuhl–Leibniz Zentrum für Informatik，Dagstuhl Publishing，GermanyXX:2金融市场交易的正式验证声明纽约证券交易所Arca将执行此类订单”。这是一个不符合其规范的项目实例。

在这里，该计划是交易所使用的匹配算法，监管指南是该计划的广泛规范。请注意，在大多数情况下，监管机构规定的指南并不是该计划的完整规范。此外，没有正式保证这些准则是一致的。这些都是一些严重的问题，可能会危及市场的安全性和完整性。计算机科学中形式化方法的最新进展可以很好地用于确保安全和公平的金融市场。在过去几十年中，形式化方法工具在证明大型软件和硬件系统的正确性方面越来越成功【9、8、12、10】。虽然模型检查工具已用于硬件验证，但交互式定理证明器在大型软件验证中的使用相当成功。使用这些工具对金融算法进行正式验证，有助于对整个市场行为进行严格分析。交易所（场馆）使用的匹配算法是金融市场广泛使用的算法的核心。验证匹配算法的正式框架也可用于验证金融市场中的其他算法。1.1 exchangeAn交易所的交易概述是一个有组织的金融市场。有各种类型的交易所：股票交易所、商品交易所、外汇交易所等。交易所有助于买卖双方就在交易所注册的产品进行交易。潜在的贸易商（买方或卖方）在市场上为某种产品下订单。这些指令由证券交易所配合执行交易。

大多数证券交易所主要在两个交易时段进行交易：上市前（或拍卖时段）和连续市场（或常规交易时段）。上市前阶段通过发现产品的开盘价来减少市场的不确定性和波动性。在上市前阶段，交易所在固定的时间内收集所有买入请求（出价）和卖出请求（要求）。在此期间结束时，交易所使用匹配算法以单一价格匹配这些买卖请求。在连续的市场交易中，新来的买家和卖家不断地相互匹配。传入的出价（ask）（如果匹配）将立即与现有的出价（ask）匹配。否则，如果出价（ask）不匹配，则将其放置在按价格排序的优先级队列中。交易员可以在这两个交易日下多个数量的每种产品的订单进行交易。然而，为了进行市场分析，必须假设每个订单是单个产品的单个单元；多个quantityorder始终可以被视为一组订单，每个订单都有一个数量，单个产品的分析将分别适用于所有产品。因此，请注意，下多个单位订单的单个交易员被视为多个交易员分别订购一个单位，即使在连续市场中也是如此。因此，在两次交易中，多个买家和卖家同时匹配。一种用于匹配多个买家和卖家的机制称为双边拍卖[7]。在双边拍卖中，拍卖商（如交易所）在一段时间内收集买卖请求。每个潜在的交易者下的订单都有一个限价：纽约证券交易所和群岛交易所合并形成了纽约证券交易所Arca，这是一个股票和期权都可以交易的交易所。Suneel Sarswat和A.K。

辛格XX：3卖方不会出售，超过该标准买方不会购买。该时间段结束时的交易所根据这些订单的限价匹配这些订单。整个过程是使用双边拍卖匹配算法完成的。双边拍卖的设计算法已经得到了很好的研究[13、17、14]。这些研究的一个主要重点是最大化匹配的数量或最大化拍卖商的利益。在拍卖理论文献中，拍卖师的利益被定义为匹配买卖对的限价之间的差异。然而，如今大多数交易所通过向交易员收取交易成本来赚取利润。因此，最大化匹配数量可以提高交易所的收益以及市场的流动性。除了在评估匹配算法的有效性时考虑的匹配数量外，还有其他重要属性，如公平性、一致性和个人合理性。然而，众所周知，没有任何一种算法可以同时拥有所有这些属性【17，13】。1.2相关工作我们之前没有已知的正式确定交易所使用的财务算法的工作。Passmore和Ignatovich在[15]中强调了金融市场正规化的重要性、机遇和挑战。他们的工作详细描述了为确保市场安全和公平而需要验证的金融算法的整体情况。交易所使用的匹配算法是整个频谱的核心。另一方面，有相当多的作品将拍卖理论中的各种概念形式化[6、11、16]。这些作品大多集中于Vickrey拍卖机制。在Vickreyauction中，有一个卖方拥有不同的项目，多个买方拥有每个项目子集的估值。

每个买家对每一个项目组合进行投标。在投标结束时，卖方的目标是通过适当地将项目分配给买方，使项目的总价值最大化。1.3我们的贡献在这项工作中，我们正式定义了拍卖理论中与金融市场交易分析相关的各种概念。我们在Coqproof assistant中定义了出价、请求和匹配等概念。Coq的相关类型对于这些概念的简洁表达非常有用，这也反映了它们的自然定义。在准备好基本框架后，我们定义了双边拍卖中匹配的重要属性：公平性、一致性、最大化和个人理性。这些物业反映了各种交易监管准则。此外，我们正式证明了这些性质的各种组合的存在性的一些结果。例如，公平和最大化总是可以同时实现的。这些结果也可以解释为监管指南各子集的一致性证明。我们在Coq证明助手的构造性设置中证明了所有这些结果，而没有添加任何额外的公理。这些证明是使用可计算的函数完成的，这些函数计算的是实际情况（Certificate）。我们还使用可计算函数在列表上表示各种谓词。最后，我们使用此设置来验证两类重要匹配算法的属性：动态价格算法和统一价格算法。在第2节中，我们正式定义了双边拍卖的理论。在第3节中，我们定义并证明了双边拍卖中匹配算法的一些重要性质。特别地，我们提出了一种动态价格匹配算法，该算法可以产生最大匹配和公平匹配。

在第3.3节中，我们描述了一种统一的价格匹配算法，该算法使用DXX:4金融市场交易的正式验证来发现金融市场中的价格。此外，我们证明了它产生的匹配在所有可能的一致匹配中是最大的。我们在第4节总结了这项工作，并对未来可能的工作进行了概述。本文中概念和证明的Coq形式化可参见[4]。2建模双边拍卖拍卖是一项竞争性活动，将商品和服务出售给最具竞争力的参与者。参与交易的交易者的优先级取决于出价和要价的各种属性（例如价格、时间等）。这种优先级最终可以通过按顺序对其排序来表示。序列最好使用Coqstandard库中的列表数据结构来表示。2.1出价、要价和限价在任何双边拍卖中，多个买家和卖家下单购买或出售标的产品。拍卖商根据他们的限价匹配这些买卖请求。虽然采购订单（即bid）的限价是买方不想购买的价格，但销售订单（即ask）的限价是卖方不想出售的价格。如果交易者希望买卖多个单位，他可以创建多个具有不同ID的出价或询问。我们可以使用包含两个字段的记录来表达出价和请求。记录Bid：类型：=Mk\\u Bid{bp：>nat；idb:nat}。记录Ask：类型：=Mk\\u Ask{sp：>nat；ida:nat}。对于标书b，（bp b）是限价，（idb b）是其唯一标识符。同样，对于ANAK a，（sp a）是限额价格，（ida a）是a的唯一标识符。请注意，当以最低面值的货币单位（如美国的美分）表示时，限额价格是自然数。

另请注意，在第一个投标字段中使用了强制符号：>。它将bp声明为一个隐式函数，该函数应用于在预期自然数的上下文中出现的Bid类型的任何术语。因此，从现在起，我们可以简单地使用binstead of（bp b）来表示b的限价。同样，我们可以使用a来表示ask a的限价。由于Bid和ask两个领域的相等性都是可判定的（即nat:eqType），因此也可以证明Bid和ask的相等性是可判定的。这是通过取消两个规范实例bid\\u eqType和ask\\u eqType来实现的，这两个实例将bid和ask连接到eqType。2.2双边拍卖中的匹配所有买卖请求可假设分别存在于列表B和列表A中。在拍卖时，拍卖师将B中的出价与A中的要求进行匹配。如果B≥ a（即bp b≥ sp a）。此外，拍卖师为每个匹配的买卖对指定一个交易价格。这个过程产生一个匹配的M，它由所有匹配的买卖对及其交易价格组成。我们将匹配定义为一个列表，其条目类型为fill\\u类型。记录fill\\u type:type：=Mk\\u fill{bid\\u of:bid；ask\\u of:ask；tp:nat}Suneel Sarswat和A.K.Singh XX:5在匹配的M中，bid或ask最多出现一次。请注意，B中可能有一些出价与M中的任何请求都不匹配。类似地，可能有一些任务inA与M中的任何投标不匹配。M中的投标列表由BM表示，M中的任务列表由AM表示。例如，图1显示了投标清单B和询价清单a之间的匹配M。请注意，BM中不存在限价37的投标，因为它与M中的任何询价都不匹配。][][][][][][][][][][][][][][][][][][][][][][][][][BAM图1 B中的投标和a中的询价分别用右括号和左括号与其限价一起表示。

M中每个匹配的买卖对都使用相同颜色的括号显示。限价37、83和120的投标与匹配M中的任何ask都不匹配。更准确地说，对于给定的bid B列表和ask a列表，M是匹配的i F，（1）M中的所有bid-ask对都是匹配的，（2）BMis无重复，（3）AMis无重复，（4）BM B、 和（5）上午 A、 我的定义1。matching\\u in B A M：=所有\\u可匹配的M∧ NoDup BM公司∧ NoDup AM∧ BM公司 B∧ 调幅 A、 上述定义中的“NoDup BMI”一词表示，每次投标都是对一个单位项目的交易请求，项目是不可分割的。我们使用表达式BM B表示术语（子集BMB）。它表达了这样一个事实，即列表中的每个元素bmi也存在于列表B中。虽然谓词NoDup和Subset能够有效地表达匹配的概念，但我们需要更多的定义来描述双边摩擦中匹配的属性。在图2中，我们描述了列表上的三个二元关系，即sublist、included和perm，它们有助于说明导致重要匹配结果的一些中间引理。例如，考虑以下引理，该引理指出匹配的性质在置换下是不变的。I引理2。匹配库存：perm M M->perm B B->perm A A->在BA M中匹配\\u->在B“A”M中匹配\\u。请注意，列表的置换概念类似于多重集中的相等。更准确地说，我们有以下指定perm关系的引理。引理3。perm\\u简介：( a、 count a l=count a s）->perm l s.I引理4。perm\\u elim：perm l s->( a、 计数a l=计数a s）。引理3中的术语（计数a l）表示列表l中元素a的出现次数。在证明匹配M的各种属性时，我们经常以BM、AMAN和PM中的信息为基础进行论证。