Ranking Formal Specifications using LLMs
summary
An LLM-driven four-metric rating workflow scores mined first-order specifications (generalizability, criticality, distinguishability, visibility) by prompting the model to output four confidence scores then combining them with tunable lambdas. Inputs come from P-based miners (Pinfer/P framework) that can produce thousands of candidates; evaluation on 14 benchmarks (11 open-source, 3 proprietary) shows goal specs are all recovered within top 50 ranked items and many within top 10, while a term-frequency baseline stalls around K=60; cost is reported as negligible.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 4:35P language and specs
- 6:59Rating framework design
- 9:24LLMs for ranking specs
- 10:48Preliminary experiments
- 13:36Summary and applications
- 15:22Q&A
related talks
38mMaking LLMs reliable - A practical framework
35mEvaluating LLM systems: the nuts and bolts
32mA Practical Guide to LLM Evaluation
25mEngineering Better Evals: Scalable LLM Evaluation Pipelines That Work
25mEvaluating An LLM's Ability To Code
29mGenerative-AI: Usecase-Specific Evaluation of LLM-powered Applications
28mTrustworthy LLMs: Vibe checks are not all you need
29mAutomating Privacy Reviews with LLMs: Challenges & Opportunities