2026-08-22·★ 会員·論文·18分で読めます

論文解説 SemaPLC — 「できました」と言わせない検証ゲート型エージェント

工場の制御コードをLLMに書かせる研究の多くは「動いて見せる」で止まっていた。SemaPLCは外部検査のログが揃うまでエージェントに完了を宣言させない設計で、実機ランタイム上の挙動スコアをベースラインの最大31.4に対し52.2まで引き上げた。

#agents #plc #code-generation #verification #industrial-control #benchmark

対象textタスクagents

SemaPLC: A Project-Grounded, Verification-Gated Agent Harness for PLC Code Generation

一次資料 — この記事の根拠

論文の発表 2026-08-19→この解説の公開 2026-08-22同月

SemaPLC: A Project-GroundedYanlun Tu, Huacan Wang, Ziyue Zhou ほか · 2026-08-19 · v1"arXiv:2608.18565論文ページ·PDF

https://arxiv.org/abs/2608.18565"Verification-Gated Agent Harness for PLC Code Generation

原文の要旨（Abstract）を読む

Programmable logic controllers (PLCs) run industrial plants, and large language models can already generate independent program organization units (POUs) for them. Whether such logic integrates into an existing PLC project and then runs correctly has been checked only in limited tests. We present \textsc{SemaPLC}, a project-grounded and verification-gated agent harness assembled from conventional tools but governed by a strict completion rule. Rather than stopping when the model judges its own output adequate, \textsc{SemaPLC} declares a task complete only when logged external checks confirm it. Those checks cover the specification, the compilation, and the behavior on a live runtime. On 117 independent-POU tasks matching existing benchmarks, it attains the highest strict verified pass rate on all seven models (72.6\% mean). On a project-context track of 65 tasks whose generated logic must compile and run inside a real project, it attains the highest mean on integrated compilation, static behavior, and dynamic behavior. Of the three layers, dynamic behavior is the most revealing. We measure it by deploying the generated and the reference logic to a live PLC runtime and comparing their executed traces. All methods fall within 10 static points of one another, whereas dynamic scores separate them sharply, from 22.4 to 31.4 for the baselines against 52.2 for \textsc{SemaPLC}. Overall, our verification-gated harness raises the mean at every layer and most sharply at runtime. Execution, not static scoring, is the faithful test of whether generated control logic actually works. \textsc{SemaPLC} is open-sourced at https://github.com/midea-ai/SemaPLC.

工場を動かすコードを、AIに書かせる

PLC（Programmable Logic Controller）は、工場のライン、発電所、浄水場を実際に動かしている制御装置です（§1）。ポンプを回す、流量が下がったら絞る、異常が出たら安全側に倒す——そうした判断が、電源が入っている間ずっとループで回り続けます。

プログラムは IEC 61131-3 という規格で書かれ、そのうち文字で書く方言が Structured Text（ST） です。見た目は Pascal に近く、LLMに書かせやすい形をしています。単体の POU（Program Organization Unit＝ファンクションブロックなど、プログラムの部品ひとつ）を生成する研究はすでに積み上がっており、コンパイラのエラーを返して直させる、モデル検査にかける、複数エージェントで回す、といった工夫が試されてきました（§2）。

ところが現場の制御ロジックは、単体で完結した部品ではありません。既存プロジェクトの中に入り、そこにある変数・型・ファンクションブロックを再利用し、ビルドや初期化の流儀に従い、その上で通電したときに正しいタイミングで動く必要があります。論文はこれを「プロジェクト接地」と「正しいランタイム挙動」と呼びます（§1）。

比喩: 「合っています」と言う職人と、通電して確かめる職人

この論文の中心は、技術的には地味な一点です。エージェントに「完了」を自己申告させない。

盤の配線を頼んだとします。片方の職人は図面と見比べて「合っています」と言う。もう片方は導通を当て、実際に電源を入れて動かし、その記録を見せてから「終わりです」と言う。出てくる配線が同じに見えても、後者だけが外部の証拠を持っています。

SemaPLC は後者を機械化したものです。モデルが自分の出力を十分だと判断した時点では止まらず、記録された外部チェックが確認したときにだけタスクを完了とする（Abstract）。チェックは仕様との突き合わせ、コンパイル、そして実機ランタイム上の挙動の3種類。道具立て自体は既存のコンパイラ・モデル検査器・ランタイムであり、新しいのはそれらをどう縛りに使うかの側だと著者らは位置づけています（§1）。

「動くのを見せた」と「どれだけ動くか測った」は違う

論文が先行研究に向けた指摘は、小見出しがそのまま主張になっています——Demonstrated, not measured（§1）。既存システムは生成コードを実行してみせるが、それは「動きうる」ことの提示であって「どれだけ確実に動くか」の測定ではない。だから著者らは、手法と測定をセットで出します。

何を測るか: 同じプログラムの3つの性質

関数トラック（単体POU）では、要求 $R_f$ とインタフェース $I_f$ から生成した POU $L_f$ を、伏せた判定器が要求由来の性質でモデル検査し、満たされた割合 $V_f$ で採点します。

\text{VerifiedPass}(L_f)=\mathbb{1}\!\left[V_f \geq 0.80\right]

(1)

$\mathbb{1}[\cdot]$ は括弧の中が成り立てば1、そうでなければ0を返す記号です。つまり式(1)は「要求から作った性質のうち8割以上が検証で満たされたときだけ合格」と言っているだけ。閾値0.80は先行研究 Agents4PLC に合わせたもので、モデル検査が「満たされた」とも「破られた」とも言えなかった性質（未対応の構文、変換失敗、タイムアウト）は不確定＝不合格として数えます（§3）。

プロジェクトトラックはもっと現場寄りです。既存プロジェクト $P$ に新しいロジック $L_p$ を差し込んだ統合プログラムを $P' = P \oplus L_p$ とし、3つの指標で別々に測ります（§3）。

$C(P')\in\{0,1\},\qquad S(P',R_p)\in[0,100],\qquad D(P',\mathcal{T})\in[0,100]$

$C$ は統合プログラムがビルドできたかの0/1、 $S$ はプログラムの文面に対して要求由来の断定が何％満たされたか、 $D$ は実機ランタイムにデプロイしてシナリオ入力 $\mathcal{T}$ を流し、隠された参照実装の実行トレースとどれだけ一致したか。順に「組み上がるか」「読めば正しそうか」「通電したら本当に正しいか」です。この3つが同じプログラムの別々の性質である、というのが論文の出発点になります（§1）。

形式検証には、黙ってしまう場所がある

なぜ実機で動かす必要があるのか。PLCのモデル検査（取りうる状態を網羅的に調べる手法）は古くから確立していますが、論文は限界を明示します——形式化済みの性質には強い保証を与える一方、TONタイマーや大きな状態空間では、未対応や結論不能に終わることが実務上ある（§2）。状態を持つビットが1つ増えるたびに探索対象は倍になるので、「大きな状態空間」は思ったより早くやってきます。

FIG 1nを動かして対数/線形を切り替えると、指数的に伸びる曲線だけが他と桁で離れていく。網羅的に状態を調べる検査が「時間内に答えられない」側へ落ちるのは、この伸び方のせい

検証ゲート: 「完了」を自己申告させない

ハーネス（harness＝実行を包む枠組み）の心臓部は、3つの不変条件です（§4.5）。

限られた再試行: 各チェックにつき修復は最大 $r=2$ ラウンド。無限に直し続けることはできません。

編集による無効化: コードを1文字でも直したら、それまでの合格判定はすべて破棄され、全チェックが走り直します。判定は「そのプログラム」ではなく「そのバイト列」に紐づく、ということです。

獲得された主張: 各チェック結果は機械可読の印として出力され、ツール呼び出しログと突き合わせて検証されます。裏付けのない自己申告は未チェックに格下げされます。

この3つが揃うと、論文が「配達整合性（delivery integrity）」と呼ぶ性質が出ます——納品されたプログラムは、報告されたすべての合格を実際に獲得した候補と同一であり、ツールログのない自己申告合格は生き残らない（§4.5）。付録Dの納品ゲートはさらに具体的で、納品バイト列が最後に成功したコンパイルの内容とハッシュ一致すること、セッションログにデプロイと強制入力の証跡があることを条件にします。要求しているのは満点ではなく、納品したバイト列に対応する、記録された外部証拠です。停止条件の一般論はLLMエージェントの基本でも扱いましたが、SemaPLC はそれを外部プロセス側へ完全に持ち出した例と言えます。