{"id":"W4385005490","doi":"10.1145/3632872","title":"Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs","year":2024,"lang":"en","type":"article","venue":"Proceedings of the ACM on Programming Languages","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":6,"is_retracted":false,"has_abstract":true,"ca_institutions":"","funders":"European Research Council; Technische Universität Wien; Vienna Science and Technology Fund; McGill University","keywords":"Invariant (physics); Probabilistic logic; Mathematics; Polynomial; Decidability; Bracket polynomial; Reachability; Discrete mathematics; Matrix polynomial; Combinatorics; Square-free polynomial; Mathematical analysis","routes":{"ca_aff":false,"ca_fund":true,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":true},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.004472055,0.00111262,0.001667676,0.0018161,0.002853416,0.005088899,0.003234287,0.002186337,0.006158532],"category_scores_gemma":[0.0289278,0.001209987,0.003924629,0.001551825,0.008235572,0.01324083,0.007182861,0.0081777,0.0008034548],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00315664,"about_ca_system_score_gemma":0.00241413,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002249885,"about_ca_topic_score_gemma":0.002282836,"domain_scores_codex":[0.9938449,0.001093437,0.0003148724,0.001645288,0.001629218,0.001472209],"domain_scores_gemma":[0.9445589,0.04683599,0.00199224,0.003804531,0.001484041,0.001324238],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.001428734,0.0004255719,0.005021873,0.0008686826,0.0001570739,0.0005850955,0.001838587,0.09809736,0.01029945,0.8220324,0.008941544,0.05030355],"study_design_scores_gemma":[0.00007875711,0.00008917102,0.0005811764,0.00004712863,0.00007831798,0.0001466355,0.0002001204,0.1117974,0.006079042,0.8789672,0.001879292,0.00005579365],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.4172672,0.0009164854,0.5445199,0.00767437,0.0002062276,0.0002656232,0.001311132,0.003832641,0.02400648],"genre_scores_gemma":[0.9375468,0.0004018029,0.05579814,0.0007154281,0.000387047,0.0001438513,0.0006996489,0.0005800371,0.003727321],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.006158532,"threshold_uncertainty_score":0.02365083,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.06247433803599339,"score_gpt":0.307724305620952,"score_spread":0.2452499675849587,"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."}}