{"id":"W4414360614","doi":"10.24963/ijcai.2025/292","title":"Verified Certificates via SAT and Computer Algebra Systems for the Ramsey R(3,8) and R(3,9) Problems","year":2025,"lang":"en","type":"article","venue":"","topic":"Computability, Logic, AI Algorithms","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Windsor; University of Waterloo","funders":"","keywords":"Boolean satisfiability problem; Correctness; Satisfiability; Solver; Verifiable secret sharing; Maximum satisfiability problem; Conjunctive normal form; Graph","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.000663579,0.0002213652,0.0002887983,0.00008837761,0.0003215826,0.0007537305,0.0007626641,0.00009091404,0.000003165776],"category_scores_gemma":[0.00002927042,0.0001427913,0.0000574929,0.0003122457,0.0001836061,0.0002421774,0.0007213527,0.0001240556,0.000006635696],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00003231335,"about_ca_system_score_gemma":0.00004024737,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0001941714,"about_ca_topic_score_gemma":0.00002338584,"domain_scores_codex":[0.9983366,0.00009089662,0.0003556267,0.0007105094,0.0001648971,0.0003414392],"domain_scores_gemma":[0.9979024,0.001081627,0.00007514151,0.0007234987,0.0001324088,0.0000849545],"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.00003707345,0.0002433319,0.004448548,0.0008291858,0.000280933,0.000004192897,0.001752737,0.00219351,0.0007429475,0.4717855,0.01273671,0.5049453],"study_design_scores_gemma":[0.0004443467,0.0001063102,0.008933348,0.00002786215,0.00001784529,0.00002004414,0.0000353833,0.960422,0.000161171,0.01522998,0.01440779,0.0001938847],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.005100215,0.00288421,0.9840333,0.004980076,0.001085078,0.001376093,0.000002741503,0.0002764528,0.0002617723],"genre_scores_gemma":[0.9301909,0.0001224957,0.06730878,0.0009604587,0.0001753364,0.0002433576,0.000004252017,0.00001711817,0.0009773289],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.9582285,"threshold_uncertainty_score":0.7268241,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02261994542786801,"score_gpt":0.2371888470241899,"score_spread":0.2145689015963219,"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."}}