In the digital age, ensuring the correctness, safety, and reliability of software through formal verification is paramount, particularly as software increasingly underpins critical infrastructure. Formal verification, split into theorem proving and model checking, provides a feasible and reliable path. Unlike theorem proving, which yields notable advances, model checking has been less focused due to the difficulty of automatic program modeling. To fill this gap, we introduce Model-Bench, a benchmark and an accompanying pipeline for evaluating and improving LLMs' program modeling capability by modeling Python programs into verification-ready model checking specifications checkable by its accompanying model checker. Model-Bench comprises 400 Python programs derived from three well-known benchmarks (HumanEval, MBPP, and LiveCodeBench). Our extensive experiments reveal significant limitations in LLMs' program modeling and further provide inspiring directions.

翻译：在数字时代，通过形式化验证确保软件的正确性、安全性和可靠性至关重要，尤其是当软件日益成为关键基础设施的基础时。形式化验证分为定理证明和模型检测，提供了一条可行且可靠的路径。与定理证明取得显著进展不同，由于自动程序建模的困难，模型检测受到的关注较少。为填补这一空白，我们提出了Model-Bench，这是一个基准测试及配套流程，通过将Python程序建模为可由其配套模型检测器检查的、可用于验证的模型检测规范，来评估和改进LLMs的程序建模能力。Model-Bench包含400个源自三个著名基准测试（HumanEval、MBPP和LiveCodeBench）的Python程序。我们广泛的实验揭示了LLMs在程序建模方面的显著局限性，并进一步提供了启发性的未来方向。