形式検証とセマンティック同値セルフプレイでLLMのコード推論を改善

arXiv cs.CL / 2026/4/21

📰 ニュースDeveloper Stack & InfrastructureSignals & Early TrendsModels & Research

共有:

要点

本論文は、Haskellコードのセマンティック同値を目的にしたセルフプレイ学習フレームワークを提案し、形式検証によりジェネレータとエバリュエータの敵対的学習を誘導します。
同値の検証にはLiquid Haskellの証明を用い、同値でない場合は実行ベースの反例を得て、難易度に応じたカリキュラムで学習の進行を制御します。
著者らは、検証済みHaskellプログラム約2.8万件からなる合成データセットOpInstruct-HSxを公開し、学習とベンチマークを支援します。
実験では下流タスクへの転移が良好で、EquiBenchで最大13.3ポイントの精度向上やPySecDBでの一貫した改善が報告されています。
訓練パイプラインとデータセットはGitHubおよびHugging Faceで公開されており、再現や発展的な研究が可能です。

Abstract

生成器と評価器の間で、敵対的トレーニングを導くために形式的検証を活用し、Haskellにおける意味的同値性のための自己対戦フレームワークを提案します。このフレームワークは、同値性の検証にLiquid Haskellの証明を活用し、非同値性に対しては実行ベースの反例を用います。これらは、難易度を考慮したカリキュラムによって整理されます。これを可能にするために、 \textbf{OpInstruct-HSx} を公開します。これは、

approx

28k件の妥当性確認済みHaskellプログラムからなる合成データセットです。実験結果は、提案する評価器が下流タスクへ効果的に転移し、EquiBenchで最大13.3ppの精度向上を達成し、PySecDBでも一貫した向上が得られることを示しています。SEQ-SINQレジームに関するアブレーション研究では、非同値性の監督がデータ量を提供する一方で、同値性の証明がモデルの推論能力を担う点で独自の役割を果たすことが示されています。学習パイプライン全体とデータセットは、それぞれGitHubとHugging Faceで公開されています。