math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories Article Swipe
Hassen Saı̈di
,
Susmit Jha
,
Tuhin Sahai
·
YOU?
·
· 2023
· Open Access
·
· DOI: https://doi.org/10.48550/arxiv.2310.17064
YOU?
·
· 2023
· Open Access
·
· DOI: https://doi.org/10.48550/arxiv.2310.17064
As artificial intelligence (AI) gains greater adoption in a wide variety of applications, it has immense potential to contribute to mathematical discovery, by guiding conjecture generation, constructing counterexamples, assisting in formalizing mathematics, and discovering connections between different mathematical areas, to name a few. While prior work has leveraged computers for exhaustive mathematical proof search, recent efforts based on large language models (LLMs) aspire to position computing platforms as co-contributors in the mathematical research process. Despite their current limitations in logic and mathematical tasks, there is growing interest in melding theorem proving systems with foundation models. This work investigates the applicability of LLMs in formalizing advanced mathematical concepts and proposes a framework that can critically review and check mathematical reasoning in research papers. Given the noted reasoning shortcomings of LLMs, our approach synergizes the capabilities of proof assistants, specifically PVS, with LLMs, enabling a bridge between textual descriptions in academic papers and formal specifications in PVS. By harnessing the PVS environment, coupled with data ingestion and conversion mechanisms, we envision an automated process, called \emph{math-PVS}, to extract and formalize mathematical theorems from research papers, offering an innovative tool for academic review and discovery.
Related Topics
Concepts
Metadata
- Type
- preprint
- Language
- en
- Landing Page
- http://arxiv.org/abs/2310.17064
- https://arxiv.org/pdf/2310.17064
- OA Status
- green
- Related Works
- 10
- OpenAlex ID
- https://openalex.org/W4387995055
All OpenAlex metadata
Raw OpenAlex JSON
- OpenAlex ID
-
https://openalex.org/W4387995055Canonical identifier for this work in OpenAlex
- DOI
-
https://doi.org/10.48550/arxiv.2310.17064Digital Object Identifier
- Title
-
math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS TheoriesWork title
- Type
-
preprintOpenAlex work type
- Language
-
enPrimary language
- Publication year
-
2023Year of publication
- Publication date
-
2023-10-25Full publication date if available
- Authors
-
Hassen Saı̈di, Susmit Jha, Tuhin SahaiList of authors in order
- Landing page
-
https://arxiv.org/abs/2310.17064Publisher landing page
- PDF URL
-
https://arxiv.org/pdf/2310.17064Direct link to full text PDF
- Open access
-
YesWhether a free full text is available
- OA status
-
greenOpen access status per OpenAlex
- OA URL
-
https://arxiv.org/pdf/2310.17064Direct OA link when available
- Concepts
-
Computer science, Variety (cybernetics), Process (computing), Automated theorem proving, Conjecture, Counterexample, Management science, Artificial intelligence, Programming language, Mathematics, Engineering, Pure mathematics, Discrete mathematicsTop concepts (fields/topics) attached by OpenAlex
- Cited by
-
0Total citation count in OpenAlex
- Related works (count)
-
10Other works algorithmically related by OpenAlex
Full payload
| id | https://openalex.org/W4387995055 |
|---|---|
| doi | https://doi.org/10.48550/arxiv.2310.17064 |
| ids.doi | https://doi.org/10.48550/arxiv.2310.17064 |
| ids.openalex | https://openalex.org/W4387995055 |
| fwci | |
| type | preprint |
| title | math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories |
| biblio.issue | |
| biblio.volume | |
| biblio.last_page | |
| biblio.first_page | |
| topics[0].id | https://openalex.org/T13523 |
| topics[0].field.id | https://openalex.org/fields/17 |
| topics[0].field.display_name | Computer Science |
| topics[0].score | 0.9941999912261963 |
| topics[0].domain.id | https://openalex.org/domains/3 |
| topics[0].domain.display_name | Physical Sciences |
| topics[0].subfield.id | https://openalex.org/subfields/1703 |
| topics[0].subfield.display_name | Computational Theory and Mathematics |
| topics[0].display_name | Mathematics, Computing, and Information Processing |
| topics[1].id | https://openalex.org/T10181 |
| topics[1].field.id | https://openalex.org/fields/17 |
| topics[1].field.display_name | Computer Science |
| topics[1].score | 0.9408000111579895 |
| topics[1].domain.id | https://openalex.org/domains/3 |
| topics[1].domain.display_name | Physical Sciences |
| topics[1].subfield.id | https://openalex.org/subfields/1702 |
| topics[1].subfield.display_name | Artificial Intelligence |
| topics[1].display_name | Natural Language Processing Techniques |
| topics[2].id | https://openalex.org/T10215 |
| topics[2].field.id | https://openalex.org/fields/17 |
| topics[2].field.display_name | Computer Science |
| topics[2].score | 0.9010999798774719 |
| topics[2].domain.id | https://openalex.org/domains/3 |
| topics[2].domain.display_name | Physical Sciences |
| topics[2].subfield.id | https://openalex.org/subfields/1702 |
| topics[2].subfield.display_name | Artificial Intelligence |
| topics[2].display_name | Semantic Web and Ontologies |
| is_xpac | False |
| apc_list | |
| apc_paid | |
| concepts[0].id | https://openalex.org/C41008148 |
| concepts[0].level | 0 |
| concepts[0].score | 0.6083950400352478 |
| concepts[0].wikidata | https://www.wikidata.org/wiki/Q21198 |
| concepts[0].display_name | Computer science |
| concepts[1].id | https://openalex.org/C136197465 |
| concepts[1].level | 2 |
| concepts[1].score | 0.5559746623039246 |
| concepts[1].wikidata | https://www.wikidata.org/wiki/Q1729295 |
| concepts[1].display_name | Variety (cybernetics) |
| concepts[2].id | https://openalex.org/C98045186 |
| concepts[2].level | 2 |
| concepts[2].score | 0.45963698625564575 |
| concepts[2].wikidata | https://www.wikidata.org/wiki/Q205663 |
| concepts[2].display_name | Process (computing) |
| concepts[3].id | https://openalex.org/C206880738 |
| concepts[3].level | 2 |
| concepts[3].score | 0.44358018040657043 |
| concepts[3].wikidata | https://www.wikidata.org/wiki/Q431667 |
| concepts[3].display_name | Automated theorem proving |
| concepts[4].id | https://openalex.org/C2780990831 |
| concepts[4].level | 2 |
| concepts[4].score | 0.44107621908187866 |
| concepts[4].wikidata | https://www.wikidata.org/wiki/Q319141 |
| concepts[4].display_name | Conjecture |
| concepts[5].id | https://openalex.org/C162838799 |
| concepts[5].level | 2 |
| concepts[5].score | 0.426643967628479 |
| concepts[5].wikidata | https://www.wikidata.org/wiki/Q596077 |
| concepts[5].display_name | Counterexample |
| concepts[6].id | https://openalex.org/C539667460 |
| concepts[6].level | 1 |
| concepts[6].score | 0.41209203004837036 |
| concepts[6].wikidata | https://www.wikidata.org/wiki/Q2414942 |
| concepts[6].display_name | Management science |
| concepts[7].id | https://openalex.org/C154945302 |
| concepts[7].level | 1 |
| concepts[7].score | 0.3228261470794678 |
| concepts[7].wikidata | https://www.wikidata.org/wiki/Q11660 |
| concepts[7].display_name | Artificial intelligence |
| concepts[8].id | https://openalex.org/C199360897 |
| concepts[8].level | 1 |
| concepts[8].score | 0.3118790090084076 |
| concepts[8].wikidata | https://www.wikidata.org/wiki/Q9143 |
| concepts[8].display_name | Programming language |
| concepts[9].id | https://openalex.org/C33923547 |
| concepts[9].level | 0 |
| concepts[9].score | 0.17787334322929382 |
| concepts[9].wikidata | https://www.wikidata.org/wiki/Q395 |
| concepts[9].display_name | Mathematics |
| concepts[10].id | https://openalex.org/C127413603 |
| concepts[10].level | 0 |
| concepts[10].score | 0.10020685195922852 |
| concepts[10].wikidata | https://www.wikidata.org/wiki/Q11023 |
| concepts[10].display_name | Engineering |
| concepts[11].id | https://openalex.org/C202444582 |
| concepts[11].level | 1 |
| concepts[11].score | 0.0 |
| concepts[11].wikidata | https://www.wikidata.org/wiki/Q837863 |
| concepts[11].display_name | Pure mathematics |
| concepts[12].id | https://openalex.org/C118615104 |
| concepts[12].level | 1 |
| concepts[12].score | 0.0 |
| concepts[12].wikidata | https://www.wikidata.org/wiki/Q121416 |
| concepts[12].display_name | Discrete mathematics |
| keywords[0].id | https://openalex.org/keywords/computer-science |
| keywords[0].score | 0.6083950400352478 |
| keywords[0].display_name | Computer science |
| keywords[1].id | https://openalex.org/keywords/variety |
| keywords[1].score | 0.5559746623039246 |
| keywords[1].display_name | Variety (cybernetics) |
| keywords[2].id | https://openalex.org/keywords/process |
| keywords[2].score | 0.45963698625564575 |
| keywords[2].display_name | Process (computing) |
| keywords[3].id | https://openalex.org/keywords/automated-theorem-proving |
| keywords[3].score | 0.44358018040657043 |
| keywords[3].display_name | Automated theorem proving |
| keywords[4].id | https://openalex.org/keywords/conjecture |
| keywords[4].score | 0.44107621908187866 |
| keywords[4].display_name | Conjecture |
| keywords[5].id | https://openalex.org/keywords/counterexample |
| keywords[5].score | 0.426643967628479 |
| keywords[5].display_name | Counterexample |
| keywords[6].id | https://openalex.org/keywords/management-science |
| keywords[6].score | 0.41209203004837036 |
| keywords[6].display_name | Management science |
| keywords[7].id | https://openalex.org/keywords/artificial-intelligence |
| keywords[7].score | 0.3228261470794678 |
| keywords[7].display_name | Artificial intelligence |
| keywords[8].id | https://openalex.org/keywords/programming-language |
| keywords[8].score | 0.3118790090084076 |
| keywords[8].display_name | Programming language |
| keywords[9].id | https://openalex.org/keywords/mathematics |
| keywords[9].score | 0.17787334322929382 |
| keywords[9].display_name | Mathematics |
| keywords[10].id | https://openalex.org/keywords/engineering |
| keywords[10].score | 0.10020685195922852 |
| keywords[10].display_name | Engineering |
| language | en |
| locations[0].id | pmh:oai:arXiv.org:2310.17064 |
| locations[0].is_oa | True |
| locations[0].source.id | https://openalex.org/S4306400194 |
| locations[0].source.issn | |
| locations[0].source.type | repository |
| locations[0].source.is_oa | True |
| locations[0].source.issn_l | |
| locations[0].source.is_core | False |
| locations[0].source.is_in_doaj | False |
| locations[0].source.display_name | arXiv (Cornell University) |
| locations[0].source.host_organization | https://openalex.org/I205783295 |
| locations[0].source.host_organization_name | Cornell University |
| locations[0].source.host_organization_lineage | https://openalex.org/I205783295 |
| locations[0].license | |
| locations[0].pdf_url | https://arxiv.org/pdf/2310.17064 |
| locations[0].version | submittedVersion |
| locations[0].raw_type | text |
| locations[0].license_id | |
| locations[0].is_accepted | False |
| locations[0].is_published | False |
| locations[0].raw_source_name | |
| locations[0].landing_page_url | http://arxiv.org/abs/2310.17064 |
| locations[1].id | doi:10.48550/arxiv.2310.17064 |
| locations[1].is_oa | True |
| locations[1].source.id | https://openalex.org/S4306400194 |
| locations[1].source.issn | |
| locations[1].source.type | repository |
| locations[1].source.is_oa | True |
| locations[1].source.issn_l | |
| locations[1].source.is_core | False |
| locations[1].source.is_in_doaj | False |
| locations[1].source.display_name | arXiv (Cornell University) |
| locations[1].source.host_organization | https://openalex.org/I205783295 |
| locations[1].source.host_organization_name | Cornell University |
| locations[1].source.host_organization_lineage | https://openalex.org/I205783295 |
| locations[1].license | |
| locations[1].pdf_url | |
| locations[1].version | |
| locations[1].raw_type | article |
| locations[1].license_id | |
| locations[1].is_accepted | False |
| locations[1].is_published | |
| locations[1].raw_source_name | |
| locations[1].landing_page_url | https://doi.org/10.48550/arxiv.2310.17064 |
| indexed_in | arxiv, datacite |
| authorships[0].author.id | https://openalex.org/A5089858094 |
| authorships[0].author.orcid | |
| authorships[0].author.display_name | Hassen Saı̈di |
| authorships[0].author_position | first |
| authorships[0].raw_author_name | Saidi, Hassen |
| authorships[0].is_corresponding | False |
| authorships[1].author.id | https://openalex.org/A5035902535 |
| authorships[1].author.orcid | https://orcid.org/0000-0001-5983-9095 |
| authorships[1].author.display_name | Susmit Jha |
| authorships[1].author_position | middle |
| authorships[1].raw_author_name | Jha, Susmit |
| authorships[1].is_corresponding | False |
| authorships[2].author.id | https://openalex.org/A5057249914 |
| authorships[2].author.orcid | https://orcid.org/0000-0003-1896-8768 |
| authorships[2].author.display_name | Tuhin Sahai |
| authorships[2].author_position | last |
| authorships[2].raw_author_name | Sahai, Tuhin |
| authorships[2].is_corresponding | False |
| has_content.pdf | False |
| has_content.grobid_xml | False |
| is_paratext | False |
| open_access.is_oa | True |
| open_access.oa_url | https://arxiv.org/pdf/2310.17064 |
| open_access.oa_status | green |
| open_access.any_repository_has_fulltext | False |
| created_date | 2023-10-28T00:00:00 |
| display_name | math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories |
| has_fulltext | False |
| is_retracted | False |
| updated_date | 2025-11-06T06:51:31.235846 |
| primary_topic.id | https://openalex.org/T13523 |
| primary_topic.field.id | https://openalex.org/fields/17 |
| primary_topic.field.display_name | Computer Science |
| primary_topic.score | 0.9941999912261963 |
| primary_topic.domain.id | https://openalex.org/domains/3 |
| primary_topic.domain.display_name | Physical Sciences |
| primary_topic.subfield.id | https://openalex.org/subfields/1703 |
| primary_topic.subfield.display_name | Computational Theory and Mathematics |
| primary_topic.display_name | Mathematics, Computing, and Information Processing |
| related_works | https://openalex.org/W4240581084, https://openalex.org/W2012590989, https://openalex.org/W4385681624, https://openalex.org/W2049141591, https://openalex.org/W2952569802, https://openalex.org/W2950489642, https://openalex.org/W1734188852, https://openalex.org/W4297939726, https://openalex.org/W4299556667, https://openalex.org/W1588024081 |
| cited_by_count | 0 |
| locations_count | 2 |
| best_oa_location.id | pmh:oai:arXiv.org:2310.17064 |
| best_oa_location.is_oa | True |
| best_oa_location.source.id | https://openalex.org/S4306400194 |
| best_oa_location.source.issn | |
| best_oa_location.source.type | repository |
| best_oa_location.source.is_oa | True |
| best_oa_location.source.issn_l | |
| best_oa_location.source.is_core | False |
| best_oa_location.source.is_in_doaj | False |
| best_oa_location.source.display_name | arXiv (Cornell University) |
| best_oa_location.source.host_organization | https://openalex.org/I205783295 |
| best_oa_location.source.host_organization_name | Cornell University |
| best_oa_location.source.host_organization_lineage | https://openalex.org/I205783295 |
| best_oa_location.license | |
| best_oa_location.pdf_url | https://arxiv.org/pdf/2310.17064 |
| best_oa_location.version | submittedVersion |
| best_oa_location.raw_type | text |
| best_oa_location.license_id | |
| best_oa_location.is_accepted | False |
| best_oa_location.is_published | False |
| best_oa_location.raw_source_name | |
| best_oa_location.landing_page_url | http://arxiv.org/abs/2310.17064 |
| primary_location.id | pmh:oai:arXiv.org:2310.17064 |
| primary_location.is_oa | True |
| primary_location.source.id | https://openalex.org/S4306400194 |
| primary_location.source.issn | |
| primary_location.source.type | repository |
| primary_location.source.is_oa | True |
| primary_location.source.issn_l | |
| primary_location.source.is_core | False |
| primary_location.source.is_in_doaj | False |
| primary_location.source.display_name | arXiv (Cornell University) |
| primary_location.source.host_organization | https://openalex.org/I205783295 |
| primary_location.source.host_organization_name | Cornell University |
| primary_location.source.host_organization_lineage | https://openalex.org/I205783295 |
| primary_location.license | |
| primary_location.pdf_url | https://arxiv.org/pdf/2310.17064 |
| primary_location.version | submittedVersion |
| primary_location.raw_type | text |
| primary_location.license_id | |
| primary_location.is_accepted | False |
| primary_location.is_published | False |
| primary_location.raw_source_name | |
| primary_location.landing_page_url | http://arxiv.org/abs/2310.17064 |
| publication_date | 2023-10-25 |
| publication_year | 2023 |
| referenced_works_count | 0 |
| abstract_inverted_index.a | 8, 41, 109, 142 |
| abstract_inverted_index.As | 0 |
| abstract_inverted_index.By | 155 |
| abstract_inverted_index.an | 169, 184 |
| abstract_inverted_index.as | 67 |
| abstract_inverted_index.by | 22 |
| abstract_inverted_index.in | 7, 29, 69, 78, 87, 102, 119, 147, 153 |
| abstract_inverted_index.is | 84 |
| abstract_inverted_index.it | 13 |
| abstract_inverted_index.of | 11, 100, 127, 134 |
| abstract_inverted_index.on | 57 |
| abstract_inverted_index.to | 17, 19, 39, 63, 174 |
| abstract_inverted_index.we | 167 |
| abstract_inverted_index.PVS | 158 |
| abstract_inverted_index.and | 32, 80, 107, 115, 150, 164, 176, 190 |
| abstract_inverted_index.can | 112 |
| abstract_inverted_index.for | 49, 187 |
| abstract_inverted_index.has | 14, 46 |
| abstract_inverted_index.our | 129 |
| abstract_inverted_index.the | 70, 98, 123, 132, 157 |
| abstract_inverted_index.(AI) | 3 |
| abstract_inverted_index.LLMs | 101 |
| abstract_inverted_index.PVS, | 138 |
| abstract_inverted_index.PVS. | 154 |
| abstract_inverted_index.This | 95 |
| abstract_inverted_index.data | 162 |
| abstract_inverted_index.few. | 42 |
| abstract_inverted_index.from | 180 |
| abstract_inverted_index.name | 40 |
| abstract_inverted_index.that | 111 |
| abstract_inverted_index.tool | 186 |
| abstract_inverted_index.wide | 9 |
| abstract_inverted_index.with | 92, 139, 161 |
| abstract_inverted_index.work | 45, 96 |
| abstract_inverted_index.Given | 122 |
| abstract_inverted_index.LLMs, | 128, 140 |
| abstract_inverted_index.While | 43 |
| abstract_inverted_index.based | 56 |
| abstract_inverted_index.check | 116 |
| abstract_inverted_index.gains | 4 |
| abstract_inverted_index.large | 58 |
| abstract_inverted_index.logic | 79 |
| abstract_inverted_index.noted | 124 |
| abstract_inverted_index.prior | 44 |
| abstract_inverted_index.proof | 52, 135 |
| abstract_inverted_index.their | 75 |
| abstract_inverted_index.there | 83 |
| abstract_inverted_index.(LLMs) | 61 |
| abstract_inverted_index.areas, | 38 |
| abstract_inverted_index.aspire | 62 |
| abstract_inverted_index.bridge | 143 |
| abstract_inverted_index.called | 172 |
| abstract_inverted_index.formal | 151 |
| abstract_inverted_index.models | 60 |
| abstract_inverted_index.papers | 149 |
| abstract_inverted_index.recent | 54 |
| abstract_inverted_index.review | 114, 189 |
| abstract_inverted_index.tasks, | 82 |
| abstract_inverted_index.Despite | 74 |
| abstract_inverted_index.between | 35, 144 |
| abstract_inverted_index.coupled | 160 |
| abstract_inverted_index.current | 76 |
| abstract_inverted_index.efforts | 55 |
| abstract_inverted_index.extract | 175 |
| abstract_inverted_index.greater | 5 |
| abstract_inverted_index.growing | 85 |
| abstract_inverted_index.guiding | 23 |
| abstract_inverted_index.immense | 15 |
| abstract_inverted_index.melding | 88 |
| abstract_inverted_index.models. | 94 |
| abstract_inverted_index.papers, | 182 |
| abstract_inverted_index.papers. | 121 |
| abstract_inverted_index.proving | 90 |
| abstract_inverted_index.search, | 53 |
| abstract_inverted_index.systems | 91 |
| abstract_inverted_index.textual | 145 |
| abstract_inverted_index.theorem | 89 |
| abstract_inverted_index.variety | 10 |
| abstract_inverted_index.academic | 148, 188 |
| abstract_inverted_index.adoption | 6 |
| abstract_inverted_index.advanced | 104 |
| abstract_inverted_index.approach | 130 |
| abstract_inverted_index.concepts | 106 |
| abstract_inverted_index.enabling | 141 |
| abstract_inverted_index.envision | 168 |
| abstract_inverted_index.interest | 86 |
| abstract_inverted_index.language | 59 |
| abstract_inverted_index.offering | 183 |
| abstract_inverted_index.position | 64 |
| abstract_inverted_index.process, | 171 |
| abstract_inverted_index.process. | 73 |
| abstract_inverted_index.proposes | 108 |
| abstract_inverted_index.research | 72, 120, 181 |
| abstract_inverted_index.theorems | 179 |
| abstract_inverted_index.assisting | 28 |
| abstract_inverted_index.automated | 170 |
| abstract_inverted_index.computers | 48 |
| abstract_inverted_index.computing | 65 |
| abstract_inverted_index.different | 36 |
| abstract_inverted_index.formalize | 177 |
| abstract_inverted_index.framework | 110 |
| abstract_inverted_index.ingestion | 163 |
| abstract_inverted_index.leveraged | 47 |
| abstract_inverted_index.platforms | 66 |
| abstract_inverted_index.potential | 16 |
| abstract_inverted_index.reasoning | 118, 125 |
| abstract_inverted_index.artificial | 1 |
| abstract_inverted_index.conjecture | 24 |
| abstract_inverted_index.contribute | 18 |
| abstract_inverted_index.conversion | 165 |
| abstract_inverted_index.critically | 113 |
| abstract_inverted_index.discovery, | 21 |
| abstract_inverted_index.discovery. | 191 |
| abstract_inverted_index.exhaustive | 50 |
| abstract_inverted_index.foundation | 93 |
| abstract_inverted_index.harnessing | 156 |
| abstract_inverted_index.innovative | 185 |
| abstract_inverted_index.synergizes | 131 |
| abstract_inverted_index.assistants, | 136 |
| abstract_inverted_index.connections | 34 |
| abstract_inverted_index.discovering | 33 |
| abstract_inverted_index.formalizing | 30, 103 |
| abstract_inverted_index.generation, | 25 |
| abstract_inverted_index.limitations | 77 |
| abstract_inverted_index.mechanisms, | 166 |
| abstract_inverted_index.capabilities | 133 |
| abstract_inverted_index.constructing | 26 |
| abstract_inverted_index.descriptions | 146 |
| abstract_inverted_index.environment, | 159 |
| abstract_inverted_index.intelligence | 2 |
| abstract_inverted_index.investigates | 97 |
| abstract_inverted_index.mathematical | 20, 37, 51, 71, 81, 105, 117, 178 |
| abstract_inverted_index.mathematics, | 31 |
| abstract_inverted_index.shortcomings | 126 |
| abstract_inverted_index.specifically | 137 |
| abstract_inverted_index.applicability | 99 |
| abstract_inverted_index.applications, | 12 |
| abstract_inverted_index.specifications | 152 |
| abstract_inverted_index.co-contributors | 68 |
| abstract_inverted_index.\emph{math-PVS}, | 173 |
| abstract_inverted_index.counterexamples, | 27 |
| cited_by_percentile_year | |
| countries_distinct_count | 0 |
| institutions_distinct_count | 3 |
| sustainable_development_goals[0].id | https://metadata.un.org/sdg/4 |
| sustainable_development_goals[0].score | 0.6399999856948853 |
| sustainable_development_goals[0].display_name | Quality Education |
| citation_normalized_percentile |