{"id":"W4415002674","doi":"10.1145/3759425.3763391","title":"A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants","year":2025,"lang":"en","type":"article","venue":"","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"University of Toronto","keywords":"Mathematical proof; Context (archaeology); Proof of concept; Qualitative research","routes":{"ca_aff":true,"ca_fund":true,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.03389622,0.0006714144,0.0004669711,0.001794048,0.00134765,0.001797229,0.002238522,0.001861507,0.001643942],"category_scores_gemma":[0.1304559,0.0005544054,0.0007540686,0.001545886,0.002726053,0.004030747,0.002850211,0.002151835,0.0003924115],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002382279,"about_ca_system_score_gemma":0.001630238,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.003015143,"about_ca_topic_score_gemma":0.003781482,"domain_scores_codex":[0.9460945,0.04123216,0.001680469,0.002076229,0.007954928,0.0009617628],"domain_scores_gemma":[0.6328291,0.3192746,0.005796586,0.02911709,0.0113367,0.0016459],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.004845293,0.004097454,0.04961459,0.004498548,0.0005359401,0.006965972,0.02670572,0.1830094,0.06894835,0.1785557,0.01524916,0.4569739],"study_design_scores_gemma":[0.001305328,0.005212674,0.01904237,0.001192189,0.0004225986,0.006092258,0.007399306,0.6251352,0.1830932,0.07328271,0.0775278,0.0002943346],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.7469147,0.001179507,0.2315203,0.00249755,0.00006159275,0.0007114548,0.0005355026,0.004917271,0.01166215],"genre_scores_gemma":[0.8077438,0.0001677017,0.1901178,0.000183861,0.00001945007,0.0001463358,0.0002258757,0.0004206172,0.0009745205],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.03389622,"threshold_uncertainty_score":0.1792625,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02846436866829156,"score_gpt":0.2796568834061952,"score_spread":0.2511925147379036,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}