機械学習技術による高速な演繹的推論エンジンの開発

利用机器学习技术开发高速演绎推理引擎

• 批准号: 22H03564
• 负责人: 塚田 武志
• 金额: $ 11.07万
• 依托单位: Chiba University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2022
• 资助国家: 日本
• 起止时间: 2022-04-01 至 2027-03-31
• 项目状态: 未结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-22H03564/
• 关键词: 演繹的推論; 機械学習; 定理自動証明; CHCソルバ; プログラム検証; システム検証

SyGuS という競技会における Inv トラックで優勝できるレベルの高性能なソルバを作成することができた。これは当初の計画における最初のステップであり、これが目論見通り達成できたことになる。機械学習としては強化学習を用いており、素朴なアルゴリズムでも専門家が与えたヒューリスティクスや他の SyGuS の参加ソルバよりも高性能なソルバを作成することができ、さらに進んだアルゴリズムを使うことでさらに高性能なソルバを作ることができた。しかしながら SyGuS 競技会の内容が変更されたため、実際に競技会に参加して優勝することは叶わなかった。この成果の意義は不変条件の発見というタスクにおいても機械学習技術が効果を発揮することを明らかにしたことにある。機械学習の演繹的推論への応用例は多いが、それらは不変条件の発見のような適切な論理式を発見するタスクを対象外または苦手とするか、あるいは適切な論理式の発見タスクを扱うが既存ソルバに比べて実行効率の面で劣っていた。不変条件の発見のようなタスクにおいても機械学習技術を援用することでソルバの効率を挙げられるということは、重要な発見である。SyGuS に優勝するレベルのソルバができたことは重要な進展だが、一方でプログラム検証などへの応用を考えると、作成したソルバが完全に満足の行くものとまでは言えない。その理由は (1) SyGuS 競技会に参加していない非常に優秀なあるソルバと比べると必ずしも勝っているとは言えないこと、(2) SyGuS の Inv トラックの問題はある側面では比較的簡単な（正確にいうと未定述語が１つ）ものであり、応用法はこのクラスから外れる問題も多いこと、が挙げられる。

我们能够创建一个名为Sygus的高性能求解器，该求解器的水平使我们能够在比赛中赢得INV赛道。这是原始计划的第一步，这是按计划实现的。强化学习用于机器学习，即使是简单的算法也可以创建比专家监督的启发式方法和其他Sygus参与的求解器更有效的求解器，并且通过使用高级算法，我们能够创建更有效的求解器。但是，由于Sygus竞赛内容的变化，不可能真正参加比赛并赢得冠军。该结果的意义在于，已经揭示了机器学习技术在发现不变条件的任务中有效。尽管机器学习有许​​多应用程序来推理推理，但它们要么排除在外，要么不擅长发现适当的逻辑表达式的任务，例如发现不变条件，或者处理发现适当的逻辑表达式的任务，但在执行方面的效率较小，而不是现有求解者。一个重要的发现，即使在发现不变条件等任务中，也可以通过将机器学习技术纳入求解器的效率来引用。创建将赢得Sygus的求解器是一个重要的发展，但是考虑到其在程序验证中的应用，不能说创建的求解器完全令人满意。原因是（1）不一定会说它优于一个没有参加Sygus竞赛的非常好的求解器，并且（2）Sygus的Inv轨道问题在一个方面（或更确切地说，有一个未确定的谓词）相对简单，并且许多应用程序偏离了这一班级。

项目成果

Optimal CHC Solving via Termination Proofs

通过终止证明最优 CHC 求解

• DOI: 10.1145/3571214
• 发表时间: 2023
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Gu Yu;Tsukada Takeshi;Unno Hiroshi
• 通讯作者: Unno Hiroshi