From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Authentication-Results: plum.tunbury.org; dkim=pass (1024-bit key; unprotected) header.d=inria.fr header.i=@inria.fr header.a=rsa-sha256 header.s=dc header.b=TAWY/9Ji; dkim-atps=neutral Received-SPF: Pass (mailfrom) identity=mailfrom; client-ip=192.134.164.83; helo=mail2-relais-roc.national.inria.fr; envelope-from=caml-list-owner@inria.fr; receiver=tunbury.org Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by plum.tunbury.org (Postfix) with ESMTP id 505E5400A3 for ; Wed, 25 Feb 2026 16:47:35 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=inria.fr; s=dc; h=to:date:message-id:from:subject:reply-to:sender:list-id: list-help:list-subscribe:list-unsubscribe:list-post: list-owner:list-archive; bh=0CSWPMLCJqzQgl4vGBt9bzteVRczB6HwlHB9nT8sL0Y=; b=TAWY/9JiN55UmhJGaQ9FJIB1Kt2MrbLGmTixFhz5xQ3U/54qRPwLejIK NU8PuR/0CQhvsECBo741oDKuaZgWiKx4L10Lnxut8T1q9Ql81En4yG8DA fHE7vHQtVUvy0VWtp6acw3SOMIFkGEkFTyZO1qphmDX40CK0xJ99fCJ8k w=; X-CSE-ConnectionGUID: tgdj0gvzQp+WHs/S1YQ8IQ== X-CSE-MsgGUID: z2vpHmVYTNmsXxAwUHWDnA== Authentication-Results: mail2-relais-roc.national.inria.fr; dkim=none (message not signed) header.i=none; spf=SoftFail smtp.mailfrom=caml-list-owner@inria.fr; spf=None smtp.helo=postmaster@prod-sympa-app.inria.fr Received-SPF: SoftFail (mail2-relais-roc.national.inria.fr: domain of caml-list-owner@inria.fr is inclined to not designate 128.93.162.27 as permitted sender) identity=mailfrom; client-ip=128.93.162.27; receiver=mail2-relais-roc.national.inria.fr; envelope-from="caml-list-owner@inria.fr"; x-sender="caml-list-owner@inria.fr"; x-conformance=spf_only; x-record-type="v=spf1"; x-record-text="v=spf1 include:mailout.safebrands.com a:basic-mail.safebrands.com a:basic-mail01.safebrands.com a:basic-mail02.safebrands.com ip4:128.93.142.0/24 ip4:192.134.164.0/24 ip4:128.93.162.160 ip4:128.93.162.3 ip4:128.93.162.88 ip4:89.107.174.7 mx ~all" Received-SPF: None (mail2-relais-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@prod-sympa-app.inria.fr) identity=helo; client-ip=128.93.162.27; receiver=mail2-relais-roc.national.inria.fr; envelope-from="caml-list-owner@inria.fr"; x-sender="postmaster@prod-sympa-app.inria.fr"; x-conformance=spf_only X-IronPort-AV: E=Sophos;i="6.21,310,1763420400"; d="scan'";a="265162767" Received: from prod-sympa-app.inria.fr ([128.93.162.27]) by mail2-relais-roc.national.inria.fr with ESMTP; 25 Feb 2026 17:47:35 +0100 Received: by prod-sympa-app.inria.fr (Postfix, from userid 990) id 8955981E6B; Wed, 25 Feb 2026 17:47:35 +0100 (CET) Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by prod-sympa-app.inria.fr (Postfix) with ESMTP id 35A9881E64 for ; Wed, 25 Feb 2026 17:44:38 +0100 (CET) X-CSE-ConnectionGUID: ZbQ4DwWTRJ+Z2X+6C4Vxlg== X-CSE-MsgGUID: LybiXIl2TlyyUE9Q465NJg== IronPort-SDR: 699f26f5_kqniOwrHLrhM+T3AKOu0M8XgKP2dSbx182bftcoJAELVW7M NpEspxOV/JMp5eoPSJrI6GXouASoy9icivTKEiw== X-ThreatScanner-Verdict: Negative X-IPAS-Result: =?us-ascii?q?A0EjBQAxJp9p/wZZH8BahRqBB14xAwQLiHCFLIh5oBwGC?= =?us-ascii?q?QEDAQ03GgQBAQMBA5IjHwcBBDQTAQIEAQEBAQMCAwEBAQEBAQEBAQ0BAQUBA?= =?us-ascii?q?QECAQECBAYBAoEKE4ZPDYJFUYIWAQEBAQEBAQEBAQEBAQEBAQEZAg00KmQqB?= =?us-ascii?q?QdBMAIeMYMWgnMDEZhGkFuBAYMc2wwJJIFTBoFNjkmCS4Jxgg2EDoNQAoE3C?= =?us-ascii?q?2uDSIIvBIMwgXmRPYFmA1ksAVUTFwsHBYFmA4EGMjwyHYEjPheBCxsHBYZcD?= =?us-ascii?q?4h0gWaBHIF2AwttPTcUG49JP4F/FYE5IU8BK2kwY5J/kiqhDpBEglmSYQRJh?= =?us-ascii?q?ASNE5lUmQaOCZV3hUGBfyaBWXKDNk4DGQ9XlC6CL8AgKG4CBwEKAQEDCZFqN?= =?us-ascii?q?IFLAQE?= IronPort-PHdr: A9a23:ajOjuh199QFnMikEsmDOog4yDhhOgF0UFjAc5pdvsb9SaKPrp82kY BeDo601xwWVBtiLo9t/yMPo8InYEVQa5piAtH1QOLdtbDQizegwoUkLLfXBN3fGKuX3ZTcxB sVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizewb7x/I A+qoQnNucUan4RvJ6gxxxbKv3BFZ/lYyWR0KF2cmBrx+t2+94N5/SRKvPIh+c9AUaHkcKk9U LdVEjcoPX0r6cPyrRXNQhOB6XQFXmgInRRGHhDJ4x7mUJj/tCv6rfd91zKBPcLqV7A0WC+t4 LltRRT1lSoILT858GXQisxtkKJWpQ+qqhJjz4LIZoyeKf1xcL7AfdMBXWpOQNpeVzBPDIO7a osAFesBPeBFpIX5qFYDqR6yCA+xD+3t1zBInGf707Ak3esvHw/I3wwuEskSvHjIsNn5KLseX PqpwKTO0D7Nb+lW2TD46IXQfRAuv/aMXbx+ccfK1UYvDBnJjlCRqYP/OjOV1/4BvHaG4Op9U ++klmEopR1rrDe12scslpfGhpgTyl3c6Sl0w4Q4K9O5RUNlfdOoDphduiWEO4Z5Rs4vTW5lt ik6xLEbupO2YCcExpQpyhPRd/CKcIyF7xPnWeuSJTp0mXRoc6+xiRa19Eiv0Oz8Vs+s3VZFr ypFjtnMtm0W2BDJ68iHTeNx/kml2TaIyw/f9OBJLVozlarBJJ4sxKM7mJkLsUnbAyP7nFv6g LWYe0k54OSl6ODqbq/nq5KaKoR6kBvxMr40lcy6Gek4MhYBX2yc+emkzrLj50j5QLRRjv0qj KbWqo3VKd4HqaGlGA9ZyIMj6xelADej0dQUh2cII09YeB6fjojpPU/BIOzgAPuih1mgji1ny v7bMrH7AZjAKmLPnbb5cbZ48UFcyQ4zzd5F55JTD7EMOP3zVVH2tNzWAB80KBC7w/39BNV41 4MRQ2ePAq6DPKzMrFCI+/ojI/OQa48NpDb9N/8l6ubygnAjnF8debCl3Z8WaHCjAvRrOF6ZY HrpgtcZC2gGpAs+TOrwiF2DSzFffXiyX7gk6jE9E42pFZ3DSZy1gLydwCe7GYVban1eBlCDD 3jocIaKVe0UZS2cP8FtiiYEWqa/S4Eizx+jrBX1y6BiLurV4S0YqYzs28Jo6OHJiR4y7iZ4D 8Gc026XSmF0n3kESCEr06BiuUBy11SD0al9g/FADdJd6P1GXBkmO5PAyeJ2E839WgfbcdeTV FmrWs2oDygpQNw+29MOeF59G9u6gx7ZwyekHqIbm6SQBJws/KLTx3jxKNh5y3bBzKQvl0AoT NNAOz7uuqkqowPaAoqMl0SCi46rc74d1WjD7jHQ43CJuRRXXQl+X43ORjYaZ0LTrJL06l6RH PeVFb07P14Zmoa5IaxQZ4i13D2uJd/mMdXaOSeqnnuoQAyPzfWKZZbrfGMU2GPcDlIFmkYd5 yXOLhAwUwGmpW+WFzlyDRT3eUq5/uR5pn2TRVRyygCDakwn2raoqVYOnfLJc/oIxfofvTs57 TB9HVKzxdXTXtWNoARvVK5HJ9Y86VJGk2/Vql81JYSueoZlgFNWaAFrpwXu2hFwX51HitQvp Wg2wRBaILid0UhdejqUm5v7IfvSK2D3/VaiZ7O+Nkj29tGQ9+9P7f05rw+mpwS1Dg849H4h1 dBJ0nya75GMDQwIUJu3XFxlvx5976rXZCUw/ea2nTVlLLW0vzne2tkoGPptyxCueM1aOb+FE wm6GtMTBsynIugn01azaRdMMOdX/a8yd8SoEpnOkKGmO+hutDm9y2FG6YV8lE+A6ms0S+LF2 YoE3+DNxhGOBH/3iFastNyymJgRPGBIWDHmj3i1QtACA886NZwGAmqvPcCtk9B3hpq3HmVd6 EbmHVQNnsmgZRuVaVX5mwxWz0Ue53K9yk7ah3R5lS8kqq2H0WnA2ePnIVAIN2lFSkFplhHpI IGxjpYXUFXiPG1L3FO1oF33waRWvvE1IGTUT0lgdDOwKmBrV6r2u7afKZ0H+NYjtiNZV/65a FaRR+vmohcU5CjkGnNX2DExczzCVozRpxVhkyrdKX9yqCCcYsRs3VLF49eaQ/dN3z0ATS0+i D/NB1H6McP7tdmTkp7CtKi5WQfDHtVcfC7lw6uLr22+5GRvAFuyk+37ltD8EAc82DP2zJEzB H+O90+6MtitieyzKqp/c1NtBUPg5sYfeMk2iYY2iJwKmDAbipiT4XsbgDL2ONRf17j5aSlFT joKztjJpQn9jRQydDTSnsSpBzPDka4DL5Ggb2gb2zww9ZVPAaaQtvlfmDdt50C/pkTXaOR8m TEUzb0v7mQbiqcHollIrG3VD7YMEE1fJSGpmQ6P6oX0o6hQamiHeqP20Ut3mNHnAb2f6FI5O j6xatI5ECl8498qel3B13P9wor/PtzRZNcS8BCYjl2Tx/gQI5U3mP0QgCNhMm+opnwpxdkwi hl21I27toyKeAAPtOqpRwRVPTrva4YP6yng2OxAy92O0dnlTd1xXy8GV5zyQbe0HSIO4L75Y h2WHmRZyD/TGKKDT1bOsgE99jSfQtbzcCvLbHgBkYc7HkjbfRMGxltIGmxj1p8/HQS3yMGzR 1xh6HYe4Vn3rhYKweVtUnu3GnHWoAPiAtstYL6YKhcergRL5kOPdNeb8vo2BSZTuJuosA2KL GWfIQVOF2AAHEKeVRjlOfG16N/M/vL9ZKL2JubSYbiIte1VVuuZjZOp3Ix8+j+QN8KJdnB8B vw/00BHUDh3AcPc0zkITiUWkWrKYav57F+k/TZrq8mk7PnxcAv14IqUF7ZbPZNk8AvwhKaKM u/WiSpkaH5Z2p4K2X7U2e0f0VoV2EQMP3GmFbUNszKITbqFw/4NSUVCLXMicpUbisB0lhNAM sPalN7vg7txj/pvTkxASUSkgMaiI8oDP2C6MlrDQkeNLrWPYzPRkKSVKeuxT6NdiOJMuli+o zGeRgXsMzONmRHiTFaqMOhJjWeWMAEU6+TfOl59THPuSt7rcEjxKNhskTg/2qE5nFvDL2sdK iRxek8LpbaLqyZZi/B+XWFN8zA2SIvM0zbc5O7eJJEMtPJtCSkhjONW7kMxzL5N5T1FTvh48 MM9htV15VSnm+yOjDdrTUgXwt6qrIuRuER5JajQ+t9LUm2C+RME6GTWBhgX9YMN4jjHsLsWz 9nGkaO1JTtfoYq8wA== IronPort-Data: A9a23:0NmV9K5hJF9/ow/hGXB74wxRtEvDchMFZxGqfqrLsTDasY5as4F+v mcZWjuPOPuDZmPzKt5/YNiwp0IOuZeBz9BmHFQ/+HhjZn8b8sCt6faxfh6hZXvKRiHgZBs6t JtGMoGowOQcFCK0SsKFa+C5xZVE/fjVAOe6UaicZ30ZqTZMEE8JkQhkl/MynrlmiN24BxLlk d7pqqUzAnf8s9JPGjxSsfvrRC9H5qyo5mtC5AFmPJingXeH/5UrJMJHTU2OByCgKmVkNrbSb /rOyri/4lTY838FYvu5kqz2e1E9WbXbOw6DkBJ+A8BOVTAfzsCa+v9T2Ms0MS+7uR3R9zxC4 IklWaiLdOscFvakdNLx/PVvO3oW0aVuoNcrKJUk2CCZ5xWun3DEm52CAKyqVGGxFyke7Wxmr JQlxD4xgh+rteiPnJ6kddVWpIcRdvmoYqhDhGFkwmSMZRomacirr6Ti7MVd3Swsi8lCW/3Vf IwcaDNqbVLNbwAn1lU/UcNk2rzxwCmuNWMwRFG9/cLb50DcwQt/3pDmK5zQe9WPRINYklvwS mfupTqkW09AbIPHodaD2la9jO7/vCehZIYDBYCVp8c23gC15GNGXXX6UnPn+KPn1hDWt8hkA 0cd/y5rqakp6GSwX9zlVlu5pmSFt1gSQbJt//YS4RuIy7HI7g+VQGMfCDtAYdkn8sI6WFTGy 2NlgfvbDwUznKKqdUi/tYXOnXDsEnQrPWsNMHpsoRQ+3zX1nG0kYvvyojtLGbSwj8bpFDj8h TuR6i0/jrASy8MHys1XHGwrYRrw+/AlrSZvum07u15JCSsjOuaYi3SAswSz0Bq5BN/xo5nol CFsdzKiAB8y4WGlyHXXHrlTdF1Yz+uDMSPRm0VuA4hp8Drl/n+qeIE43QyT5S5BbK45RNMeS BKJ4VwBvcMKbBNHr8ZfOuqMNijj9oC4ffyNaxweRoMmjkFZJV7brhJ9L1WdxX7sm0UKmKQyc 8XTO8W1AHpQTewtwDOqTq1PmfUm1wIv91P1HJrb9hWA1abBRXi3TbxeDkCCQNpk54y5oSLU0 e1lCe209ztlXtfDPxbnqbwoEQhSLFwQJ4zHlMhMR+vSfitkAD4ADtHS85MAeqtkvaZeh7rU9 06TRkZjlV7NpUDGDS6oaXlTTqzlcrgijHA8PA0qZU2J3Vp6a6mRza4vTbkFVph5y/5SlttPU Ogjee+MJt9tWwb30W0RQrelpbMzaSnxoxyFOhSURQQWfrlidlTvwcDldA6+zxs+JHO7muVmq oLxyz6BZ4QIQjljK8PkaPiP6VeVllpFkcJQW3r4GPViSH/OwqNLdROo1uQWJvsSIyrt3jGZj gaaISkJrNn3/rMazoP7urCmnayITc1FAUtoL0vK5+2XNA7b3FaZ761ubeKqRQ3ZBUTIoPiMR OMN1PztEuw1rHATuapGLrtb56Yf5dzumrxk8jpZDEj7N1SFNp4wI12t/9V+ialW97oI5Sq0Q h2u//dZC5WoOeTkMl4aIVM9Zb+50cAroyTjt9InBECj/B5IpaKjVHtRMyKtkw1YFqN+a6k+8 NciuekXyg2xsQUrOdC4lRJp93yAA3gDcqc/vLcYC5/Ppitx738aer3aKCv9wK/XWuV2KkNwf wOl3vvTtYpT1m/pUiQVF0GU+cF/mJ5XmhRB7GFaFmSzgtCf28MGhkxAww8WEDZQ4A5Mid9oG 25RMEZwG6WC0hFoiOVHXEGuAwtxPwKYyGOg12o2kHDlcGfwWlzvNGEdPcO/zHId+U9YfRlZ+ +i840ThWjDIYsrw/3UTXWhIlv/dduFypzbywJ2fI8e4HpcBcWXEhI2qbjE2sBfJO546q3DGg uhIx9xOT5PHGxQemIABMLnC548sEEiFAEdgXcBe+Lg4GDCAWTOqhhmLBUODWuJMAP3o80SpV tBnGexTXi/j0BSukzE/LowPKo9Sg/QGyocjeLTqBGheqJqZjGNjn6zx/xjEpl0AYotRg/dmD 7jOZhSAOGC0rllFqV/n9cVrFDKxXogZWVfawuuwztQsK7sCl+NdKWcJzbq+uiSuAjtNph67k lvKWP7L8rZE149poorLF5dDDSWSLffYdryB0CK3guR0QeL/C+X8nCJLlQC/JCVTB6UbZPpvn 7fUsNLX4lLMjIxrb0/nwau+B4t7zuTsetFIM/DHDmhQxgqDf87O3yEt2U6FLb5xrdcMwfX/G iWZbpK8e+dADp0ZjDdQZjNFGhkQN7XvY+2y7WmhpvCLEV4G3RaBMNqj8mTzYHpGcjMTfafzE RLwp+3k8+UwQF6g3/PYL6oO715EzF7ftW8Ofsf0tCKEA2CkxFiJof3nlBMl6HfGBmTs/AMWJ 37abkCWSfhwkPigIBJlX0hatQZRCXd0hOh2c04AkzKzoy7vF3YIdIzxLr1fYqy5UUXOOFXQb yqLaWorDCS7UDhZGfk5DBIPQS/HbtEz1hzFyvDFMq9ah+paxG9NPVe5yhpd3g== IronPort-HdrOrdr: A9a23:YVoF3a3WUGdZWgC5CeInMQqjBJYkLtp133Aq2lEZdPUMSL39qy g39M5rryMc+wxhP03I/urwRZVoIEmsjqKdjrNwAV7PZmTbUS6TXeRfBOjZskHd8k/Fh41gPM 5bGsAUYuEYT2IK7/oSizPWLz9U+ri6GdeT69s2oU0AceggUdAH0+4wMHfjLqRZfng/OaYE X-Talos-CUID: 9a23:H+WjsW8ikhda4LPIisCVv3weI5wJbULh9lWTERWISjhCFIOFTVDFrQ== X-Talos-MUID: 9a23:PlqoOAX7niLR/Orq/Bv9jjBSFcMy36C/GX0gwKxa5ZSiFyMlbg== X-IronPort-Anti-Spam-Filtered: true X-IronPort-AV: E=Sophos;i="6.21,310,1763420400"; d="scan'208";a="265162070" X-MGA-submission: =?us-ascii?q?MDEG1G2PwnbWf+g7cViNQrFRdAvcw4hv1T1Tte?= =?us-ascii?q?cXwxrcAXAFYZcm0mcQAmJ5e0kabuwG9zZi0bWjltDAwVp0Psg7iSbIKT?= =?us-ascii?q?lN7BEc+Wa4+5L2/aPYpRU/PSk66ySsaR7jnQ4yFGRWJ2N/HvLSip+DSx?= =?us-ascii?q?38r5l/PN1kew5omU2+lUTOtQ=3D=3D?= Received: from armistead.cs.miami.edu (HELO armistead.ccs.miami.edu) ([192.31.89.6]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/ECDHE-RSA-AES256-GCM-SHA384; 25 Feb 2026 17:44:37 +0100 Received: by armistead.ccs.miami.edu (Postfix, from userid 3640) id EFEAAA018CC; Wed, 25 Feb 2026 11:44:24 -0500 (EST) To: User-Agent: mail (GNU Mailutils 3.14) Date: Wed, 25 Feb 2026 11:44:24 -0500 Message-Id: <20260225164424.EFEAAA018CC@armistead.ccs.miami.edu> From: geoff@cs.miami.edu X-Validation-by: geoff@cs.miami.edu Subject: [Caml-list] 2nd Workshop on Machine Learning for Solvers and Provers Reply-To: geoff@cs.miami.edu X-Loop: caml-list@inria.fr X-Sequence: 19460 Errors-To: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Help: , List-Subscribe: , List-Unsubscribe: , List-Post: List-Owner: List-Archive: Archived-At: CfP: 2nd Workshop on Machine Learning for Solvers and Provers - Lisbon - July 18 ========================================= We warmly invite you to submit your work to the 2nd Workshop on Machine Learning for Solvers and Provers (ML4SP), organised as part of the 2026 Federated Logic Conference (FLoC 2026) at Lisbon, Portugal. The workshop will run during the first block of the conference, on July 18, 2026. Workshop website: https://ml4sp.github.io/ Machine learning (ML) has had a substantial impact on SAT/SMT and CP solvers, as well as automated theorem provers. Recent advances have demonstrated the power of ML to inform solver heuristics, guide proof search, and optimize algorithm portfolios. Despite growing interest in this direction, work on ML for solvers and provers is often scattered across multiple research communities – SAT, SMT, CP, theorem proving, formal methods, and machine learning – with few opportunities for focused interaction. The ML4SP workshop aims to bring together researchers and practitioners working at the intersection of machine learning and formal reasoning systems. It provides a forum for the presentation of recent work, the exchange of ideas, and the fostering of collaboration between these communities. Topics of interest include, but are not limited to, ML-driven approaches for: + Heuristics (branching, restarts, ...) in CP, SAT, SMT, and MIP solvers + Tactic selection and proof guidance in automated and interactive theorem provers + Algorithm selection, parameter tuning and algorithm configuration, and portfolio solvers + End-to-end learning for solvers and provers + Benchmark generation and instance hardness prediction + Applications of ML-enhanced reasoning in verification, synthesis, planning, and related areas + Leveraging large language models (LLMs) for solver heuristics and proof guidance We welcome submissions describing previously published work, ongoing research, and position papers and early-stage ideas intended to stimulate discussion. Submission should be in PDF form, following the LIPIcs guidelines. They can be: + Extended abstracts (up to two pages, excluding references); or + Full papers (up to 15 pages, excluding references). All submissions will be reviewed by the PC members. A presentation time slot will be given to each accepted submission. Submission link: https://submissions.floc26.org/ml4sp/ Key dates: + Submission deadline: 15 May 2026 AoE + Result notification: 25 May 2026 + Camera ready: 2 July 2026 + Workshop day: 18 July 2026 Registration: please see FLoC’26 registration page