כתבה
arXiv cs.AI ·
TLA-Prover: ייצור תיאור תכונות TLA+ ניתנות לאימות באמצעות תאימות-אופטימיזציה
TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation
מודל חדש, TLA-Prover, יוצר תיאורי TLA+ שניתנים לאימות. המודל משתמש באופטימיזציה של תאימות ולמידה עצמית כדי לשפר את יכולתו לייצר תיאורי TLA+ נאמנים.
תקציר מקורי באנגליתarXiv:2606.06133v4 Announce Type: replace-cross Abstract: TLA+ is a formal specification language for verifying distributed systems and safety-critical protocols. Large language models (LLMs) frequently produce TLA+ specifications that fail the TLC model checker for semantic reasons. Across 25 LLMs, the best public baseline is 26.6% syntactic parse and 8.6% semantic model-check. We present TLA-Prover, a 20-billion-parameter model for TLA+ specification synthesis. Training combines supervised fine-tuning (SFT) on verified examples with repair-based group-relative policy optimization (GRPO). In the GRPO stage, the model learns to fix its own rejected specifications. We also train a direct preference optimization (DPO) variant from the same SFT checkpoint as an ablation. TLC provides the rewa
קרא במקור המקורי
arxiv.org
פתח כתבה מקורית