{"id":"W2058282107","doi":"10.1145/2406336.2406349","title":"Formalization of Measure Theory and Lebesgue Integration for Probabilistic Analysis in HOL","year":2013,"lang":"en","type":"article","venue":"ACM Transactions on Embedded Computing Systems","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":13,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"HOL; Computer science; Probabilistic logic; Dependability; Theoretical computer science; Automated theorem proving; Measure (data warehouse); Class (philosophy); Artificial intelligence; Programming language; Data mining; Software engineering","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.001938057,0.000144953,0.0002973597,0.0005388192,0.0001263797,0.000124726,0.0004610535,0.0001024771,0.000002185207],"category_scores_gemma":[0.0003544488,0.0001333144,0.00009117189,0.001195221,0.00004460736,0.0005460507,0.00001105516,0.0001226291,0.000002245822],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00008272197,"about_ca_system_score_gemma":0.00003288626,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0001222944,"about_ca_topic_score_gemma":0.00002078428,"domain_scores_codex":[0.9982031,0.0004534746,0.0005785952,0.0003534476,0.0002207784,0.0001905918],"domain_scores_gemma":[0.9980611,0.0006399276,0.0002584087,0.0006900468,0.0003056687,0.00004489181],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.00006799184,0.000271527,0.0003537911,0.0004165562,0.000283753,2.997446e-7,0.01024639,0.5006757,0.00333985,0.241282,0.00001324608,0.2430489],"study_design_scores_gemma":[0.0002880401,0.0001189513,0.001564763,0.0001165087,0.00007094659,0.00000437594,0.0006282703,0.9892831,0.002218783,0.005562543,0.000004775138,0.0001389128],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.05040116,0.00005121301,0.9480222,0.00003899951,0.0002798359,0.001041649,0.000003882745,0.00008960121,0.0000714896],"genre_scores_gemma":[0.799019,0.000002776507,0.2007899,0.00001487519,0.00001332482,0.0001275238,0.000005238971,0.000007975163,0.00001939561],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.7486178,"threshold_uncertainty_score":0.5436403,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02621687487000435,"score_gpt":0.2903207323166397,"score_spread":0.2641038574466353,"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."}}